@article{BLP06,
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,PACSS},
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).},
}
