Analysis

• Goal: prove that B bel A <-Kab-> B.

• Proof:

  B sees {T, A bel A <-Kab-> B}Kbs M2
  
  B bel S said (T, A bel A <-Kab-> B) A3, rule 1
  B bel fresh(T, A bel A <-Kab-> B) A1, rule 5
  B bel S bel (T, A bel A <-Kab-> B) rule 2
  B bel S bel A bel A <-Kab-> B conjunction
  B bel A bel A <-Kab-> B A4, rule 3
  B bel A <-Kab-> B A2, Rule 3

• Exercises:

  • Prove that S bel A bel A <-Kab-> B
  • Add the message B -> A: {T}Kab (M3) and show that

    A bel B bel A <-Kab-> B
    

Previous slide

Next slide

Back to first slide

View graphic version