Jan Jürjens and Tjark Weber. In Pierpaolo Degano and Luca Viganò, editors, Foundations and Applications of Security Analysis, Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPA-WITS 2009, York, UK, March 28-29, 2009, Revised Selected Papers, volume 5511 of Lecture Notes in Computer Science, pages 155-172. Springer, 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,
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 = {Foundations and Applications of Security Analysis, Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPA-WITS 2009, York, UK, March~28--29, 2009, Revised Selected Papers},
volume = {5511},
series = {Lecture Notes in Computer Science},
pages = {155--172},
publisher = {Springer},
year = {2009},
url = {http://dx.doi.org/10.1007/978-3-642-03459-6_11}
}