Sciweavers

Share
SP
2006
IEEE

A Computationally Sound Mechanized Prover for Security Protocols

10 years 5 months ago
A Computationally Sound Mechanized Prover for Security Protocols
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.
Bruno Blanchet
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where SP
Authors Bruno Blanchet
Comments (0)
books