Sala Riunioni 1 - Dipartimento di Scienze dell'Informazione - at 9.00 am

Title
"CryptoVerif: A Computationally Sound Mechanized Prover for Security Protocols"


Abstract

We present the prover CryptoVerif: it is the first mechanized prover for security protocols sound in the computational model. It produces proofs presented as sequences of games, like the manual proofs of cryptographers; these games are formalized in a probabilistic polynomial-time process calculus. CryptoVerif provides a generic method for specifying security assumptions on cryptographic primitives, which can handle shared-key and public-key encryption, signatures, message authentication codes, and hash functions. It can prove secrecy and correspondence properties (including authentication). It produces proofs valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary.