Welcome to the resource topic for 2005/401
Title:
A Computationally Sound Mechanized Prover for Security Protocols
Authors: Bruno Blanchet
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.
ePrint: https://eprint.iacr.org/2005/401
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .