Introduction Symbolic Model Computational Model Implementations Conclusion

De
Publié par

Introduction Symbolic Model Computational Model Implementations Conclusion Security Protocol Verification: Symbolic and Computational Models Bruno Blanchet INRIA, Ecole Normale Superieure, CNRS March 2012 Bruno Blanchet (INRIA, ENS, CNRS) ETAPS March 2012 1 / 48

  • cryptographic primitives

  • computational models

  • verifying protocol

  • security protocols

  • model computational

  • basic cryptographic

  • model implementations

  • ecole normale


Publié le : mardi 19 juin 2012
Lecture(s) : 28
Source : di.ens.fr
Nombre de pages : 53
Voir plus Voir moins
Introduction
Bruno Blanchet
Symbolic Model
Security mbolic a
Sy
Computational Model
Implementations
Protocol Verification: nd Computational Mod
Bruno Blanchet
els
´ INRIA,EcoleNormaleSupe´rieure,CNRS Bruno.Blanchet@ens.fr
(INRIA, ENS, CNRS)
March 2012
ETAPS
March 2012
Conclusion
1 / 48
Introduction
Outline
1
2
3
4
5
Symbolic Model
Computational Model
Implementations
Introduction to security protocols Verifying protocols in the symbolic model Verifying protocols in the computational model Verifying protocol implementations Conclusion and future challenges
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
March 2012
Conclusion
2 / 48
Introduction
Symbolic Model
Communications
A(Alice)
Bruno Blanchet
over
(INRIA, ENS, CNRS)
a
Computational Model
secure
network
secure network
ETAPS
Implementations
B
(Bob)
March 2012
Conclusion
3 / 48
Introduction
Symbolic Model
Computational Model
Implementations
Communications over anniesrecukortwne
A(Alice)
insecure network
B(Bob)
C(attacker) Atalks toBon an insecure network need for cryptography in order to make communications secure for instance, encrypt messages to preserve secrets.
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
March 2012
Conclusion
4 / 48
Introduction
Symbolic Model
Cryptographic primitives
Computational Model
Implementations
Conclusion
Definition (Cryptographic primitives) Basic cryptographic algorithms, used as building blocks for protocols, e.g.encryptionandsignatures.
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
March 2012
5 / 48
Introduction
Symbolic Model
Cryptographic primitives
Computational Model
Implementations
Conclusion
Definition (Cryptographic primitives) Basic cryptographic algorithms, used as building blocks for protocols, e.g.encryptionandsignatures.
Shared-key encryption
encryption
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
decryption
March 2012
5 / 48
Introduction
Symbolic Model
Cryptographic primitives
Computational Model
Implementations
Conclusion
Definition (Cryptographic primitives) Basic cryptographic algorithms, used as building blocks for protocols, e.g.encryptionandsignatures.
Public-key encryption
encryption
public key
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
decryption
private key
March 2012
5 / 48
Introduction
Symbolic Model
Cryptographic primitives
Computational Model
Implementations
Conclusion
Definition (Cryptographic primitives) Basic cryptographic algorithms, used as building blocks for protocols, e.g.encryptionandsignatures.
Signatures
signature
private key
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
verification
signature ok?
public key
March 2012
5 / 48
Introduction
Example
Symbolic Model
Computational Model
Implementations
Denning-Sacco key distribution protocol [Denning, Sacco, 1981] (simplified)
kfresh
A(Alice)
{{k}skA}pkB
{s}k
The goal of the protocol is that the keykshould b betweenAandB. Sosshould remain secret.
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
B(Bob)
Conclusion
e a secret key, shared
March 2012
6 / 48
Introduction
The attack
Symbolic Model
Computational Model
The (well-known) attack against this protocol. kfresh{{k}skA}pkC
A(Alice)
The attackerC
C
Implementations
{{k}skA}pkB
(attacker) asA(Alice)
{s}k
impersonatesAand obtains the secrets.
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
Conclusion
B(Bob)
March 2012
7 / 48
Introduction
Symbolic Model
The corrected protocol
kfresh
A(Alice)
Computational Model
{{ABk}skA}pkB
{s}k
Implementations
B(Bob)
Conclusion
NowCcannot impersonateAbecause in the previous attack, the first message is{{ACk}skA}pkB, which is not accepted byB.
Bruno Blanchet (INRIA, ENS, CNRS)
ETAPS
March 2012
8 / 48
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.