15 Proc. Royal Soc. 426 (1989). |
15 Proc. Royal Soc. 426 (1989). |
16 *} |
16 *} |
17 |
17 |
18 types state = "event list" |
18 types state = "event list" |
19 |
19 |
20 constdefs |
|
21 |
|
22 (*The spy MAY say anything he CAN say. We do not expect him to |
20 (*The spy MAY say anything he CAN say. We do not expect him to |
23 invent new nonces here, but he can also use NS1. Common to |
21 invent new nonces here, but he can also use NS1. Common to |
24 all similar protocols.*) |
22 all similar protocols.*) |
|
23 definition |
25 Fake :: "(state*state) set" |
24 Fake :: "(state*state) set" |
26 "Fake == {(s,s'). |
25 where "Fake = {(s,s'). |
27 \<exists>B X. s' = Says Spy B X # s |
26 \<exists>B X. s' = Says Spy B X # s |
28 & X \<in> synth (analz (spies s))}" |
27 & X \<in> synth (analz (spies s))}" |
29 |
28 |
30 (*The numeric suffixes on A identify the rule*) |
29 (*The numeric suffixes on A identify the rule*) |
31 |
30 |
32 (*Alice initiates a protocol run, sending a nonce to Bob*) |
31 (*Alice initiates a protocol run, sending a nonce to Bob*) |
|
32 definition |
33 NS1 :: "(state*state) set" |
33 NS1 :: "(state*state) set" |
34 "NS1 == {(s1,s'). |
34 where "NS1 = {(s1,s'). |
35 \<exists>A1 B NA. |
35 \<exists>A1 B NA. |
36 s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1 |
36 s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1 |
37 & Nonce NA \<notin> used s1}" |
37 & Nonce NA \<notin> used s1}" |
38 |
38 |
39 (*Bob responds to Alice's message with a further nonce*) |
39 (*Bob responds to Alice's message with a further nonce*) |
|
40 definition |
40 NS2 :: "(state*state) set" |
41 NS2 :: "(state*state) set" |
41 "NS2 == {(s2,s'). |
42 where "NS2 = {(s2,s'). |
42 \<exists>A' A2 B NA NB. |
43 \<exists>A' A2 B NA NB. |
43 s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2 |
44 s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2 |
44 & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) \<in> set s2 |
45 & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) \<in> set s2 |
45 & Nonce NB \<notin> used s2}" |
46 & Nonce NB \<notin> used s2}" |
46 |
47 |
47 (*Alice proves her existence by sending NB back to Bob.*) |
48 (*Alice proves her existence by sending NB back to Bob.*) |
|
49 definition |
48 NS3 :: "(state*state) set" |
50 NS3 :: "(state*state) set" |
49 "NS3 == {(s3,s'). |
51 where "NS3 = {(s3,s'). |
50 \<exists>A3 B' B NA NB. |
52 \<exists>A3 B' B NA NB. |
51 s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3 |
53 s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3 |
52 & Says A3 B (Crypt (pubK B) {|Nonce NA, Agent A3|}) \<in> set s3 |
54 & Says A3 B (Crypt (pubK B) {|Nonce NA, Agent A3|}) \<in> set s3 |
53 & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) \<in> set s3}" |
55 & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) \<in> set s3}" |
54 |
56 |
55 |
57 |
56 definition Nprg :: "state program" where |
58 definition Nprg :: "state program" where |
57 (*Initial trace is empty*) |
59 (*Initial trace is empty*) |
58 "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)" |
60 "Nprg = mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)" |
59 |
61 |
60 declare spies_partsEs [elim] |
62 declare spies_partsEs [elim] |
61 declare analz_into_parts [dest] |
63 declare analz_into_parts [dest] |
62 declare Fake_parts_insert_in_Un [dest] |
64 declare Fake_parts_insert_in_Un [dest] |
63 |
65 |