title = { Pattern-based abstraction for verifying secrecy in protocols },
    author = {Bozga, Liana and Lakhnech, Yassine and P\'erin, Micha\"el},
    month = {Feb},
    year = {2006},
    journal = {International Journal on Software Tools for Technology Transfer (STTT)},
    key = {Cryptographic protocols - Security - Verification - Abstract interpretation - Widening},
    pages = {57-76},
    volume = {8},
    team = {DCS},
    abstract = {We present a method based on abstract interpretation for verifying secrecy properties of cryptographic protocols. Our method allows one 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 subterm. 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 s), Yahalom (12.67 s), Otway-Rees (0.01 s), and Kao-Chow (0.78 s).},


Publication Sections

Contact | Site Map | Site created with SPIP 2.1.26 + AHUNTSIC [CC License]

Logged in visitors: 10 ; visits: 449470