33 (*Alice initiates a protocol run*) |
33 (*Alice initiates a protocol run*) |
34 WL1 "[| evs: woolam; A ~= B |] |
34 WL1 "[| evs: woolam; A ~= B |] |
35 ==> Says A B (Agent A) # evs : woolam" |
35 ==> Says A B (Agent A) # evs : woolam" |
36 |
36 |
37 (*Bob responds to Alice's message with a challenge.*) |
37 (*Bob responds to Alice's message with a challenge.*) |
38 WL2 "[| evs: woolam; A ~= B; |
38 WL2 "[| evs: woolam; A ~= B; |
39 Says A' B (Agent A) : set_of_list evs |] |
39 Says A' B (Agent A) : set_of_list evs |] |
40 ==> Says B A (Nonce (newN(length evs))) # evs : woolam" |
40 ==> Says B A (Nonce NB) # evs : woolam" |
41 |
41 |
42 (*Alice responds to Bob's challenge by encrypting NB with her key. |
42 (*Alice responds to Bob's challenge by encrypting NB with her key. |
43 B is *not* properly determined -- Alice essentially broadcasts |
43 B is *not* properly determined -- Alice essentially broadcasts |
44 her reply.*) |
44 her reply.*) |
45 WL3 "[| evs: woolam; A ~= B; |
45 WL3 "[| evs: woolam; A ~= B; |
46 Says B' A (Nonce NB) : set_of_list evs; |
46 Says A B (Agent A) : set_of_list evs; |
47 Says A B (Agent A) : set_of_list evs |] |
47 Says B' A (Nonce NB) : set_of_list evs |] |
48 ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam" |
48 ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam" |
49 |
49 |
50 (*Bob forwards Alice's response to the Server.*) |
50 (*Bob forwards Alice's response to the Server.*) |
51 WL4 "[| evs: woolam; B ~= Server; |
51 WL4 "[| evs: woolam; B ~= Server; |
52 Says A' B X : set_of_list evs; |
52 Says A' B X : set_of_list evs; |