Welcome to the resource topic for 2006/069
Title:
Automated Security Proofs with Sequences of Games
Authors: Bruno Blanchet, David Pointcheval
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.
ePrint: https://eprint.iacr.org/2006/069
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 .