BlanchetPointchevalCrypto06
Bruno Blanchet
Back to publications
Bruno Blanchet and David Pointcheval.
Automated Security Proofs with Sequences of Games.
In Cynthia Dwork, editor, CRYPTO'06, volume 4117 of
Lecture Notes in Computer Science, pages 537-554, Santa Barbara, CA, August
2006. Springer.
Copyright
© IACR.
Get the paper
.ps.gz, 194 Kb, .pdf, 190 Kb
Links
LNCS series home page.
This paper at Springer: http://dx.doi.org/10.1007/11818175_32.
Extended version available as ePrint Report 2006/069, http://eprint.iacr.org/2006/069.
Slides of the talk.
Abstract
This paper presents the first automatic technique for
proving not only protocols but also primitives in the exact security
computational model. Automatic proofs of cryptographic protocols were
up to now reserved to the Dolev-Yao model, which however makes quite
strong assumptions on the primitives. On the other hand, with the
proofs by reductions, in the complexity theoretic framework, more
subtle security assumptions can be considered, but security analyses
are manual. A process calculus is thus defined in order to take into
account the probabilistic semantics of the computational model. It is
already rich enough to describe all the usual security notions of both
symmetric and asymmetric cryptography, as well as the basic
computational assumptions. As an example, we illustrate the use of the
new tool with the proof of a quite famous asymmetric primitive:
unforgeability under chosen-message attacks (UF-CMA) of the
Full-Domain Hash signature scheme under the (trapdoor)-one-wayness of
some permutations.
Bibtex
@INPROCEEDINGS{BlanchetPointchevalCrypto06,
AUTHOR = {Bruno Blanchet and David Pointcheval},
TITLE = {Automated Security Proofs with Sequences of Games},
BOOKTITLE = {CRYPTO'06},
PAGES = {537--554},
YEAR = 2006,
EDITOR = {Cynthia Dwork},
VOLUME = 4117,
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Santa Barbara, CA},
MONTH = AUG,
PUBLISHER = {Springer}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)