Introduction Using ProVerif Horn clauses Applications Conclusion

Bruno Blanchet

Description

Introduction Using ProVerif Horn clauses Applications Conclusion The automatic security protocol verifier ProVerif Bruno Blanchet CNRS, Ecole Normale Superieure, INRIA, Paris June 2010 Bruno Blanchet (CNRS, ENS, INRIA) ProVerif June 2010 1 / 43

• distribution protocol


• proverif horn


• clauses applications


• secret key


• dolev-yao model


• security protocol verifier


• yao

Sujets

• Needham
• Blanchet
• Key (cryptography)
• Dolev-Yao model

Informations

• Publié par: pefav
• Nombre de lectures: 44
• Langue: English

Extrait

IntroductionUsignrPVorefioHnrlcseauppsAcaliontinoCssulcnoi alBoehcnnurB,INSIANRCNt(,ERS2e10JfnueVirP)or

Bruno Blanchet

June 2010

3

The automatic security protocol verifier ProVerif

´ CNRS, Ecole Normale Superieure, INRIA, Paris ´

01/4

nUioctdurontIualcAsesilppitacngsioVPriferrnHoonsConclusion 102enuJfireVorP)

Introduction

Many techniques exist for the verification of cryptographic protocols (theorem proving, model checking, typing, . . . ) We present a technique based on an abstract representation of the protocol by aset of Horn clauses. This technique yieldsfully automaticproofs of protocols for an unbounded number of runs(many clients connecting to a server, for instance) and anunbounded message space.

3/402cnehBoalrBnuNRIANS,IRS,Et(CN

InUiongsirontctduusioonclnilppAsesCsnoitaciferoVPrauclrnHo S,EN(CNRchetBlanuronB433/

Active attacker: the attacker canintercept all messages sent on the network he cancompute messages he cansend messages on the network

Model of protocols

neJu1020VorPfireNI,S)AIR

nUsingPrroductionrlcuaesVorefioHontionsCppsAcalisulcnoi noBlBruet(Canch

Theformal modelor “Dolev-Yao model” is due to Needham and Schroeder (1978) and Dolev and Yao (1983). The cryptographic primitives areblackboxes. The messages aretermson these primitives. The attacker is restricted to compute only using these primitives. ⇒perfect cryptography assumption One can add equations between primitives, but in any case, one makes the hypothesis that the only equalities are those given by these equations.

The formal model facilitates automatic proofs.

Model of protocols: the formal model

43A)PrINRIENS,NRS,01/4en02fiuJVore Int