Verimag

Technical Reports

L. Bozga, Y. Lakhnech and M. Perin
Pattern-based Abstraction for Verifying Secrecy in Protocols (2004)

TR-2004-1.pdf
TR-2004-1.ps

Keywords: Security, Cryptographic Protocols, Abstract Interpretation, Verification

Abstract: We present a method based on abstract interpretation for verifying secrecy properties of cryptographic protocols. Our method allows to verify secrecy properties in a general model allowing an unbounded number of sessions, an unbounded number of principals and an unbounded size of messages. As abstract domain we use sets of so-called super terms. Super terms are obtained by allowing an interpreted constructor, which we denote by Sup, where the meaning of a term $\Sup(t)$ is the set of terms that contain $t$ as sub-term. For these terms, we solve a generalized form of the unification problem and introduce a widening operator. We implemented a prototype and were able to verify well-known protocols such as for instance Needham-Schroeder-Lowe (0.03 sec), Yahalom (12.67 sec), Otway-Rees (0.01 sec) and Kao-Chow (0.78 sec).

Contact | Site Map | Site powered by SPIP 3.0.25 + AHUNTSIC [CC License]

info visites 777787