Finite Models in FOL-Based Crypto-Protocol Verification

8 years 12 months ago
Finite Models in FOL-Based Crypto-Protocol Verification
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. We show that it can be used to deal with infinitely many principals (and thus sessions).
Jan Jürjens, Tjark Weber
Added 19 Feb 2011
Updated 19 Feb 2011
Type Journal
Year 2009
Where IFIP
Authors Jan Jürjens, Tjark Weber
Comments (0)