A -> B: {T, Kab}Ka-1 --> B sees {T, A <-Kab-> B}Ka-1
(A1) B bel Ka-> A
(A2) A bel A <-Kab-> B
(A3) B bel fresh(T)
(A4) B bel A controls A <-Kab-> B
B bel A said (T, A <-Kab-> B) A1, rule 1
B bel fresh(T, A <-Kab-> B) A3, rule 5
B bel A bel (T, A <-Kab-> B) rule 2
B bel A <-Kab-> B A4, rule 3
| Previous slide | Next slide | Back to first slide | View graphic version |