Jan Jürjens and Tjark Weber. In Pierpaolo Degano and Luca Viganò, editors, ARSPA-WITS'09 - Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, Informal Proceedings, pages 211-227, York, UK, March 2009.
Cryptographic protocols can only be secure under certain inequality assumptions. Axiomatizing these inequalities explicitly is problematic: stating too many inequalities may impair soundness of the verification approach. To address this issue, we investigate an alternative approach (based on first-order logic) that does not require inequalities to be axiomatized. A derivation of the negated security property exhibits a protocol attack, and absence of a derivation amounts to absence of the investigated kind of attack.
We establish a fragment of FOL strictly greater than Horn formulas in which the approach is sound. We then show how to use finite model generation in this context to prove the absence of attacks. To demonstrate its practicality, the approach is applied to several well-known protocols, including ones relying on non-trivial algebraic properties.
@inproceedings{juerjens09finite-pre,
author = {Jan J{\"u}rjens and Tjark Weber},
title = {Finite Models in {FOL}-based Crypto-Protocol Verification},
editor = {Pierpaolo Degano and Luca Vigan{\`o}},
booktitle = {ARSPA-WITS'09~-- Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, Informal Proceedings},
pages = {211--227},
address = {York, UK},
month = mar,
year = {2009}
}