Dolev-Yao Model

• Dolev-Yao model [DY83]

• Decidability of cascade, name-stamp (“ping-pong”) protocols

  • Start with a secret M
  • Each party in turn applies a combination of operators:

    Public-key encryption Ej for any party j: M -> {M}Kj
    
    Public-key decryption for self, Di
    Append an identifier Ij for any party j: M -> {M, j}
    Remove an appended identifier j: Rj
    Remove any appended identifier: R

  • Example:

    A -> B: Eb(Ia(Eb(M))) = a1(M) = M’ = {{M}Kb, A}Kb
    
    B -> A: Ea(Ib(Ea(Db(Ra(Db(M’)))))) = b1(M’) = Ea(Ib(Ea(M))) = M”
    A -> B: a2(M”) ...

Previous slide

Next slide

Back to first slide

View graphic version