Introduction Calculus Proof technique Example proof Conclusion

icon

39

pages

icon

Français

icon

Documents

Écrit par

Publié par

Lire un extrait
Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe et accède à tout notre catalogue !

Je m'inscris

Découvre YouScribe et accède à tout notre catalogue !

Je m'inscris
icon

39

pages

icon

Français

icon

Documents

Lire un extrait
Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Introduction Calculus Proof technique Example proof Conclusion CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols Bruno Blanchet CNRS, Ecole Normale Superieure, INRIA, Paris June 2009 Bruno Blanchet (CNRS, ENS, INRIA) CryptoVerif June 2009 1 / 38

  • cryptographic primitives

  • proofs can

  • proof technique

  • bitstrings cryptographic primitives

  • approach allows

  • direct approach

  • dolev-yao model

  • automatic proof


Voir icon arrow

Publié par

Langue

Français

IntroductionCaluculPsorfoethcineEqumpxaprlefCoolcnooisunteC(nahconlBBurA)CrINRIENS,NRS,002enuJfireVotpy
Bruno Blanchet
June 2009
CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols
´ CNRS,EcoleNormaleSupe´rieure,INRIA,Paris
8/391
IortntcudethcinuqEeaxpmelionCalculusProofonfCooprniousclnu2e00293/8
Two models for security protocols: Computational model: messages are bitstrings cryptographic primitives are functions from bitstrings to bitstrings the adversary is a probabilistic polynomial-time Turing machine Proofs are done manually. Formal model(so-called “Dolev-Yao model”): cryptographic primitives are ideal blackboxes messages are terms built from the cryptographic primitives the adversary is restricted to use only the primitives Proofs can be done automatically. Our goal: achieveautomatic provabilityunder the realisticcomputational assumptions.
Introduction
RIA)CryptoVerifJtehcRNC(NE,SNI,SBnoruanBl
C(RNhctelBnauronBVetofJrie2un9300NE,SNI,S)AIRpyrC3/8
Two approaches for the automatic proof of cryptographic protocols in a computational model: Indirect approach: 1) Make a Dolev-Yao proof. 2) Use a theorem that shows the soundness of the Dolev-Yao approach with respect to the computational model. Pioneered by Abadi and Rogaway; pursued by many others. Direct approach: Design automatic tools for proving protocols in a computational model. Approach pioneered by Laud.
Introduction
clusionproofConEeaxpmelethcinuqsPluofronCiocualortntcudI
Voir icon more
Alternate Text