Issue No. 04 - October-December (2008 vol. 5)
We present a new mechanized prover for secrecy properties of security protocols. In contrast to most previous provers, our tool does not rely on the Dolev-Yao model, but on the computational model. It produces proofs presented as sequences of games; these games are formalized in a probabilistic polynomial-time process calculus. Our tool provides a generic method for specifying security properties of the cryptographic primitives, which can handle shared-key and public-key encryption, signatures, message authentication codes, and hash functions. Our tool produces proofs valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. We have implemented our tool and tested it on a number of examples of protocols from the literature.
C.2.2.c Protocol verification, F.3.1.d Mechanical verification, D.2.4.d Formal methods
B. Blanchet, "A Computationally Sound Mechanized Prover for Security Protocols," in IEEE Transactions on Dependable and Secure Computing, vol. 5, no. , pp. 193-207, 2007.