Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Introduction Calculus Proof technique Example proof Conclusion

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

  • cryptographic primitives

  • proofs can

  • proof technique

  • bitstrings cryptographic primitives

  • approach allows

  • direct approach

  • dolev-yao model

  • automatic proof


Voir plus Voir moins
IntroductionCaluculPsorfoethcineEqumpxaprlefCoolcnooisuneh(talcnnuBorBIA)C,INR,ENSCNRS2lirpAfireVotpyr
Bruno Blanchet
April 2009
CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols
´ CNRS,EcoleNormaleSupe´rieure,INRIA,Paris
8/39100
tnIudorfoethcinuqEeaxpmctionCalculusPronfCooprleiousclonAfrpli0290/283
Introduction
INRIA)CryptoVerihcnaC(te,SRN,SNEruBBlno
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.
oneh(talcnnuBorBptryeroVApifl2riSRNCSNE,RNI,C)AI00393/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
ConclusipleproofqieuxEmaootfcenhullcPrustiucCaonnIdort
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin