Pattern-based abstraction for verifying secrecy in protocols

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).