|
1 theory Needham_Schroeder_No_Attacker_Example |
|
2 imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" |
|
3 begin |
|
4 |
|
5 datatype agent = Alice | Bob | Spy |
|
6 |
|
7 definition agents :: "agent set" |
|
8 where |
|
9 "agents = {Spy, Alice, Bob}" |
|
10 |
|
11 definition bad :: "agent set" |
|
12 where |
|
13 "bad = {Spy}" |
|
14 |
|
15 datatype key = pubEK agent | priEK agent |
|
16 |
|
17 fun invKey |
|
18 where |
|
19 "invKey (pubEK A) = priEK A" |
|
20 | "invKey (priEK A) = pubEK A" |
|
21 |
|
22 datatype |
|
23 msg = Agent agent --{*Agent names*} |
|
24 | Key key |
|
25 | Nonce nat --{*Unguessable nonces*} |
|
26 | MPair msg msg --{*Compound messages*} |
|
27 | Crypt key msg --{*Encryption, public- or shared-key*} |
|
28 |
|
29 text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*} |
|
30 syntax |
|
31 "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
|
32 |
|
33 syntax (xsymbols) |
|
34 "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") |
|
35 |
|
36 translations |
|
37 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
|
38 "{|x, y|}" == "CONST MPair x y" |
|
39 |
|
40 inductive_set |
|
41 parts :: "msg set => msg set" |
|
42 for H :: "msg set" |
|
43 where |
|
44 Inj [intro]: "X \<in> H ==> X \<in> parts H" |
|
45 | Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H" |
|
46 | Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H" |
|
47 | Body: "Crypt K X \<in> parts H ==> X \<in> parts H" |
|
48 |
|
49 inductive_set |
|
50 analz :: "msg set => msg set" |
|
51 for H :: "msg set" |
|
52 where |
|
53 Inj [intro,simp] : "X \<in> H ==> X \<in> analz H" |
|
54 | Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H" |
|
55 | Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H" |
|
56 | Decrypt [dest]: |
|
57 "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H" |
|
58 |
|
59 inductive_set |
|
60 synth :: "msg set => msg set" |
|
61 for H :: "msg set" |
|
62 where |
|
63 Inj [intro]: "X \<in> H ==> X \<in> synth H" |
|
64 | Agent [intro]: "Agent agt \<in> synth H" |
|
65 | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H" |
|
66 | Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H" |
|
67 |
|
68 primrec initState |
|
69 where |
|
70 initState_Alice: |
|
71 "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)" |
|
72 | initState_Bob: |
|
73 "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)" |
|
74 |
|
75 | initState_Spy: |
|
76 "initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)" |
|
77 |
|
78 datatype |
|
79 event = Says agent agent msg |
|
80 | Gets agent msg |
|
81 | Notes agent msg |
|
82 |
|
83 |
|
84 primrec knows :: "agent => event list => msg set" |
|
85 where |
|
86 knows_Nil: "knows A [] = initState A" |
|
87 | knows_Cons: |
|
88 "knows A (ev # evs) = |
|
89 (if A = Spy then |
|
90 (case ev of |
|
91 Says A' B X => insert X (knows Spy evs) |
|
92 | Gets A' X => knows Spy evs |
|
93 | Notes A' X => |
|
94 if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs) |
|
95 else |
|
96 (case ev of |
|
97 Says A' B X => |
|
98 if A'=A then insert X (knows A evs) else knows A evs |
|
99 | Gets A' X => |
|
100 if A'=A then insert X (knows A evs) else knows A evs |
|
101 | Notes A' X => |
|
102 if A'=A then insert X (knows A evs) else knows A evs))" |
|
103 |
|
104 abbreviation (input) |
|
105 spies :: "event list => msg set" where |
|
106 "spies == knows Spy" |
|
107 |
|
108 primrec used :: "event list => msg set" |
|
109 where |
|
110 used_Nil: "used [] = Union (parts ` initState ` agents)" |
|
111 | used_Cons: "used (ev # evs) = |
|
112 (case ev of |
|
113 Says A B X => parts {X} \<union> used evs |
|
114 | Gets A X => used evs |
|
115 | Notes A X => parts {X} \<union> used evs)" |
|
116 (* --{*The case for @{term Gets} seems anomalous, but @{term Gets} always |
|
117 follows @{term Says} in real protocols. Seems difficult to change. |
|
118 See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *}*) |
|
119 |
|
120 inductive_set ns_public :: "event list set" |
|
121 where |
|
122 (*Initial trace is empty*) |
|
123 Nil: "[] \<in> ns_public" |
|
124 (*Alice initiates a protocol run, sending a nonce to Bob*) |
|
125 | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> |
|
126 \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) |
|
127 # evs1 \<in> ns_public" |
|
128 (*Bob responds to Alice's message with a further nonce*) |
|
129 | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; |
|
130 Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> |
|
131 \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) |
|
132 # evs2 \<in> ns_public" |
|
133 |
|
134 (*Alice proves her existence by sending NB back to Bob.*) |
|
135 | NS3: "\<lbrakk>evs3 \<in> ns_public; |
|
136 Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
|
137 Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk> |
|
138 \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public" |
|
139 |
|
140 |
|
141 subsection {* Preparations for sets *} |
|
142 |
|
143 fun find_first :: "('a => 'b option) => 'a list => 'b option" |
|
144 where |
|
145 "find_first f [] = None" |
|
146 | "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)" |
|
147 |
|
148 consts cps_of_set :: "'a set => ('a => term list option) => term list option" |
|
149 |
|
150 lemma |
|
151 [code]: "cps_of_set (set xs) f = find_first f xs" |
|
152 sorry |
|
153 |
|
154 consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option" |
|
155 consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => code_numeral => term list Quickcheck_Exhaustive.three_valued" |
|
156 |
|
157 lemma |
|
158 [code]: "pos_cps_of_set (set xs) f i = find_first f xs" |
|
159 sorry |
|
160 |
|
161 consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued) |
|
162 => 'b list => 'a Quickcheck_Exhaustive.three_valued" |
|
163 |
|
164 lemma [code]: |
|
165 "find_first' f [] = Quickcheck_Exhaustive.No_value" |
|
166 "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))" |
|
167 sorry |
|
168 |
|
169 lemma |
|
170 [code]: "neg_cps_of_set (set xs) f i = find_first' f xs" |
|
171 sorry |
|
172 |
|
173 setup {* |
|
174 let |
|
175 val Fun = Predicate_Compile_Aux.Fun |
|
176 val Input = Predicate_Compile_Aux.Input |
|
177 val Output = Predicate_Compile_Aux.Output |
|
178 val Bool = Predicate_Compile_Aux.Bool |
|
179 val oi = Fun (Output, Fun (Input, Bool)) |
|
180 val ii = Fun (Input, Fun (Input, Bool)) |
|
181 fun of_set compfuns (Type ("fun", [T, _])) = |
|
182 case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of |
|
183 Type ("Quickcheck_Exhaustive.three_valued", _) => |
|
184 Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T)) |
|
185 | Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T) |
|
186 | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T)) |
|
187 fun member compfuns (U as Type ("fun", [T, _])) = |
|
188 (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns |
|
189 (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0)))) |
|
190 |
|
191 in |
|
192 Core_Data.force_modes_and_compilations @{const_name Set.member} |
|
193 [(oi, (of_set, false)), (ii, (member, false))] |
|
194 end |
|
195 *} |
|
196 |
|
197 subsection {* Derived equations for analz, parts and synth *} |
|
198 |
|
199 lemma [code]: |
|
200 "analz H = (let |
|
201 H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H)) |
|
202 in if H' = H then H else analz H')" |
|
203 sorry |
|
204 |
|
205 lemma [code]: |
|
206 "parts H = (let |
|
207 H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H)) |
|
208 in if H' = H then H else parts H')" |
|
209 sorry |
|
210 |
|
211 code_pred [skip_proof] ns_publicp . |
|
212 thm ns_publicp.equation |
|
213 |
|
214 code_pred [generator_cps] ns_publicp . |
|
215 thm ns_publicp.generator_cps_equation |
|
216 |
|
217 setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *} |
|
218 declare ListMem_iff[symmetric, code_pred_inline] |
|
219 |
|
220 declare [[quickcheck_timing]] |
|
221 setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} |
|
222 declare [[quickcheck_full_support = false]] |
|
223 |
|
224 lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" |
|
225 (*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose] |
|
226 quickcheck[exhaustive, size = 8, timeout = 3600, verbose] |
|
227 quickcheck[narrowing, size = 7, timeout = 3600, verbose]*) |
|
228 quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample] |
|
229 oops |
|
230 |
|
231 lemma |
|
232 "\<lbrakk>ns_publicp evs\<rbrakk> |
|
233 \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs |
|
234 \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B |
|
235 \<Longrightarrow> Nonce NB \<notin> analz (spies evs)" |
|
236 quickcheck[smart_exhaustive, depth = 6, timeout = 30] |
|
237 quickcheck[narrowing, size = 6, timeout = 30, verbose] |
|
238 oops |
|
239 |
|
240 end |