L. Bozga, Y. Lakhnech and M. Perin
Pattern-based Abstraction for Verifying Secrecy in Protocols (2004)
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).
