14 Computer Security Foundations Workshop, 1996. |
14 Computer Security Foundations Workshop, 1996. |
15 *) |
15 *) |
16 |
16 |
17 WooLam = Shared + |
17 WooLam = Shared + |
18 |
18 |
19 consts woolam :: "agent set => event list set" |
19 consts lost :: agent set (*No need for it to be a variable*) |
20 inductive "woolam lost" |
20 woolam :: event list set |
|
21 inductive woolam |
21 intrs |
22 intrs |
22 (*Initial trace is empty*) |
23 (*Initial trace is empty*) |
23 Nil "[]: woolam lost" |
24 Nil "[]: woolam" |
24 |
25 |
25 (*The spy MAY say anything he CAN say. We do not expect him to |
26 (*The spy MAY say anything he CAN say. We do not expect him to |
26 invent new nonces here, but he can also use NS1. Common to |
27 invent new nonces here, but he can also use NS1. Common to |
27 all similar protocols.*) |
28 all similar protocols.*) |
28 Fake "[| evs: woolam lost; B ~= Spy; |
29 Fake "[| evs: woolam; B ~= Spy; |
29 X: synth (analz (sees lost Spy evs)) |] |
30 X: synth (analz (sees lost Spy evs)) |] |
30 ==> Says Spy B X # evs : woolam lost" |
31 ==> Says Spy B X # evs : woolam" |
31 |
32 |
32 (*Alice initiates a protocol run*) |
33 (*Alice initiates a protocol run*) |
33 WL1 "[| evs: woolam lost; A ~= B |] |
34 WL1 "[| evs: woolam; A ~= B |] |
34 ==> Says A B (Agent A) # evs : woolam lost" |
35 ==> Says A B (Agent A) # evs : woolam" |
35 |
36 |
36 (*Bob responds to Alice's message with a challenge.*) |
37 (*Bob responds to Alice's message with a challenge.*) |
37 WL2 "[| evs: woolam lost; A ~= B; |
38 WL2 "[| evs: woolam; A ~= B; |
38 Says A' B (Agent A) : set_of_list evs |] |
39 Says A' B (Agent A) : set_of_list evs |] |
39 ==> Says B A (Nonce (newN evs)) # evs : woolam lost" |
40 ==> Says B A (Nonce (newN evs)) # evs : woolam" |
40 |
41 |
41 (*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. |
42 B is *not* properly determined -- Alice essentially broadcasts |
43 B is *not* properly determined -- Alice essentially broadcasts |
43 her reply.*) |
44 her reply.*) |
44 WL3 "[| evs: woolam lost; A ~= B; |
45 WL3 "[| evs: woolam; A ~= B; |
45 Says B' A (Nonce NB) : set_of_list evs; |
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 A B (Crypt (Nonce NB) (shrK A)) # evs : woolam lost" |
48 ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam" |
48 |
49 |
49 (*Bob forwards Alice's response to the Server.*) |
50 (*Bob forwards Alice's response to the Server.*) |
50 WL4 "[| evs: woolam lost; B ~= Server; |
51 WL4 "[| evs: woolam; B ~= Server; |
51 Says A' B X : set_of_list evs; |
52 Says A' B X : set_of_list evs; |
52 Says A'' B (Agent A) : set_of_list evs |] |
53 Says A'' B (Agent A) : set_of_list evs |] |
53 ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam lost" |
54 ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam" |
54 |
55 |
55 (*Server decrypts Alice's response for Bob.*) |
56 (*Server decrypts Alice's response for Bob.*) |
56 WL5 "[| evs: woolam lost; B ~= Server; |
57 WL5 "[| evs: woolam; B ~= Server; |
57 Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|} |
58 Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} |
58 : set_of_list evs |] |
59 : set_of_list evs |] |
59 ==> Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B)) |
60 ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) |
60 # evs : woolam lost" |
61 # evs : woolam" |
61 |
62 |
62 end |
63 end |