A computationally sound mechanized prover for security protocols

TLDR

In contrast to most previous provers, our tool does not rely on the Dolev‑Yao model but on the computational model. We present a new mechanized prover for secrecy properties of cryptographic protocols. The prover generates proofs as sequences of games formalized in a probabilistic polynomial‑time process calculus, providing a generic method to specify security properties for primitives such as encryption, signatures, MACs, and hash functions, and operates in the computational model rather than the Dolev‑Yao model. The tool produces proofs valid for a polynomial number of sessions in the security parameter against an active adversary, and has been implemented and tested on several literature protocols.

Abstract

We present a new mechanized prover for secrecy properties of cryptographic 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-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