A
S
B
A -> S: A, {T, B, Kab}Kas --> (M1) S sees {T, A <-Kab-> B}Kas
S -> B: {T, A, Kab}Kbs --> (M2) B sees {T, A bel A <-Kab-> B}Kbs
(A1) P bel fresh(T), for P = A, B, S
(A2) B bel A controls A <-Kab-> B
(A3) S bel A <-Kas-> S, B bel B <-Kbs-> S
(A4) B bel S controls A bel A <-Kab-> B
(A5) A bel A <-Kab-> B
T is a timestamp
A generates Kab
Kas, Kbs are shared with S
S should check this
Justifies A said A <-Kab-> B
| Previous slide | Next slide | Back to first slide | View graphic version |