Finiteness Limitation

• How many sessions must be simulated to ensure coverage?

  • Lowe attack needed two sessions
  • Example 1.3 in Dolev-Yao [DY83] needed three sessions

    A -> B: {{M}PKb, A}PKb
    
    B -> A: {{M}Pka, B}Pka

• No algorithmically determined bound is possible for all cases

  Because of undecidability for the model
  

• Possible bounds for limited classes of protocols

  • Lowe “small system” result [Low98b]: one honest agent per role, one time, if certain restrictions are satisfied:

    Encrypted fields are distinguishable
    
    Principal identities in every encrypted field
    No temporary secrets
    No forwarding of encrypted fields

Previous slide

Next slide

Back to first slide

View graphic version