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

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-)