author | berghofe |
Wed, 11 Jul 2007 11:14:51 +0200 | |
changeset 23746 | a455e69c31cc |
parent 22426 | 1c38ca2496c4 |
child 35416 | d8d7d1b785af |
permissions | -rw-r--r-- |
13508 | 1 |
(****************************************************************************** |
2 |
date: april 2002 |
|
3 |
author: Frederic Blanqui |
|
4 |
email: blanqui@lri.fr |
|
5 |
webpage: http://www.lri.fr/~blanqui/ |
|
6 |
||
7 |
University of Cambridge, Computer Laboratory |
|
8 |
William Gates Building, JJ Thomson Avenue |
|
9 |
Cambridge CB3 0FD, United Kingdom |
|
10 |
******************************************************************************) |
|
11 |
||
12 |
header{*Other Protocol-Independent Results*} |
|
13 |
||
16417 | 14 |
theory Proto imports Guard_Public begin |
13508 | 15 |
|
16 |
subsection{*protocols*} |
|
17 |
||
18 |
types rule = "event set * event" |
|
19 |
||
20768 | 20 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
21 |
msg' :: "rule => msg" where |
20768 | 22 |
"msg' R == msg (snd R)" |
13508 | 23 |
|
24 |
types proto = "rule set" |
|
25 |
||
26 |
constdefs wdef :: "proto => bool" |
|
27 |
"wdef p == ALL R k. R:p --> Number k:parts {msg' R} |
|
28 |
--> Number k:parts (msg`(fst R))" |
|
29 |
||
30 |
subsection{*substitutions*} |
|
31 |
||
32 |
record subs = |
|
33 |
agent :: "agent => agent" |
|
34 |
nonce :: "nat => nat" |
|
35 |
nb :: "nat => msg" |
|
36 |
key :: "key => key" |
|
37 |
||
38 |
consts apm :: "subs => msg => msg" |
|
39 |
||
40 |
primrec |
|
41 |
"apm s (Agent A) = Agent (agent s A)" |
|
42 |
"apm s (Nonce n) = Nonce (nonce s n)" |
|
43 |
"apm s (Number n) = nb s n" |
|
44 |
"apm s (Key K) = Key (key s K)" |
|
45 |
"apm s (Hash X) = Hash (apm s X)" |
|
46 |
"apm s (Crypt K X) = ( |
|
47 |
if (EX A. K = pubK A) then Crypt (pubK (agent s (agt K))) (apm s X) |
|
48 |
else if (EX A. K = priK A) then Crypt (priK (agent s (agt K))) (apm s X) |
|
49 |
else Crypt (key s K) (apm s X))" |
|
50 |
"apm s {|X,Y|} = {|apm s X, apm s Y|}" |
|
51 |
||
52 |
lemma apm_parts: "X:parts {Y} ==> apm s X:parts {apm s Y}" |
|
53 |
apply (erule parts.induct, simp_all, blast) |
|
54 |
apply (erule parts.Fst) |
|
55 |
apply (erule parts.Snd) |
|
56 |
by (erule parts.Body)+ |
|
57 |
||
58 |
lemma Nonce_apm [rule_format]: "Nonce n:parts {apm s X} ==> |
|
59 |
(ALL k. Number k:parts {X} --> Nonce n ~:parts {nb s k}) --> |
|
60 |
(EX k. Nonce k:parts {X} & nonce s k = n)" |
|
61 |
by (induct X, simp_all, blast) |
|
62 |
||
63 |
lemma wdef_Nonce: "[| Nonce n:parts {apm s X}; R:p; msg' R = X; wdef p; |
|
64 |
Nonce n ~:parts (apm s `(msg `(fst R))) |] ==> |
|
65 |
(EX k. Nonce k:parts {X} & nonce s k = n)" |
|
66 |
apply (erule Nonce_apm, unfold wdef_def) |
|
67 |
apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp) |
|
68 |
apply (drule_tac x=x in bspec, simp) |
|
69 |
apply (drule_tac Y="msg x" and s=s in apm_parts, simp) |
|
70 |
by (blast dest: parts_parts) |
|
71 |
||
72 |
consts ap :: "subs => event => event" |
|
73 |
||
74 |
primrec |
|
75 |
"ap s (Says A B X) = Says (agent s A) (agent s B) (apm s X)" |
|
76 |
"ap s (Gets A X) = Gets (agent s A) (apm s X)" |
|
77 |
"ap s (Notes A X) = Notes (agent s A) (apm s X)" |
|
78 |
||
20768 | 79 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
80 |
ap' :: "subs => rule => event" where |
20768 | 81 |
"ap' s R == ap s (snd R)" |
13508 | 82 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
83 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
84 |
apm' :: "subs => rule => msg" where |
20768 | 85 |
"apm' s R == apm s (msg' R)" |
86 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
87 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
88 |
priK' :: "subs => agent => key" where |
20768 | 89 |
"priK' s A == priK (agent s A)" |
90 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
91 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
92 |
pubK' :: "subs => agent => key" where |
20768 | 93 |
"pubK' s A == pubK (agent s A)" |
13508 | 94 |
|
95 |
subsection{*nonces generated by a rule*} |
|
96 |
||
97 |
constdefs newn :: "rule => nat set" |
|
98 |
"newn R == {n. Nonce n:parts {msg (snd R)} & Nonce n ~:parts (msg`(fst R))}" |
|
99 |
||
100 |
lemma newn_parts: "n:newn R ==> Nonce (nonce s n):parts {apm' s R}" |
|
101 |
by (auto simp: newn_def dest: apm_parts) |
|
102 |
||
103 |
subsection{*traces generated by a protocol*} |
|
104 |
||
105 |
constdefs ok :: "event list => rule => subs => bool" |
|
106 |
"ok evs R s == ((ALL x. x:fst R --> ap s x:set evs) |
|
107 |
& (ALL n. n:newn R --> Nonce (nonce s n) ~:used evs))" |
|
108 |
||
23746 | 109 |
inductive_set |
110 |
tr :: "proto => event list set" |
|
111 |
for p :: proto |
|
112 |
where |
|
13508 | 113 |
|
23746 | 114 |
Nil [intro]: "[]:tr p" |
13508 | 115 |
|
23746 | 116 |
| Fake [intro]: "[| evsf:tr p; X:synth (analz (spies evsf)) |] |
117 |
==> Says Spy B X # evsf:tr p" |
|
13508 | 118 |
|
23746 | 119 |
| Proto [intro]: "[| evs:tr p; R:p; ok evs R s |] ==> ap' s R # evs:tr p" |
13508 | 120 |
|
121 |
subsection{*general properties*} |
|
122 |
||
123 |
lemma one_step_tr [iff]: "one_step (tr p)" |
|
124 |
apply (unfold one_step_def, clarify) |
|
23746 | 125 |
by (ind_cases "ev # evs:tr p" for ev evs, auto) |
13508 | 126 |
|
127 |
constdefs has_only_Says' :: "proto => bool" |
|
128 |
"has_only_Says' p == ALL R. R:p --> is_Says (snd R)" |
|
129 |
||
130 |
lemma has_only_Says'D: "[| R:p; has_only_Says' p |] |
|
131 |
==> (EX A B X. snd R = Says A B X)" |
|
132 |
by (unfold has_only_Says'_def is_Says_def, blast) |
|
133 |
||
134 |
lemma has_only_Says_tr [simp]: "has_only_Says' p ==> has_only_Says (tr p)" |
|
135 |
apply (unfold has_only_Says_def) |
|
136 |
apply (rule allI, rule allI, rule impI) |
|
137 |
apply (erule tr.induct) |
|
138 |
apply (auto simp: has_only_Says'_def ok_def) |
|
139 |
by (drule_tac x=a in spec, auto simp: is_Says_def) |
|
140 |
||
141 |
lemma has_only_Says'_in_trD: "[| has_only_Says' p; list @ ev # evs1 \<in> tr p |] |
|
142 |
==> (EX A B X. ev = Says A B X)" |
|
143 |
by (drule has_only_Says_tr, auto) |
|
144 |
||
145 |
lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s; |
|
146 |
ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))" |
|
147 |
apply (unfold ok_def, clarsimp) |
|
148 |
apply (drule_tac x=x in spec, drule_tac x=x in spec) |
|
149 |
by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts) |
|
150 |
||
151 |
lemma ok_is_Says: "[| evs' @ ev # evs:tr p; ok evs R s; has_only_Says' p; |
|
152 |
R:p; x:fst R |] ==> is_Says x" |
|
153 |
apply (unfold ok_def is_Says_def, clarify) |
|
154 |
apply (drule_tac x=x in spec, simp) |
|
155 |
apply (subgoal_tac "one_step (tr p)") |
|
156 |
apply (drule trunc, simp, drule one_step_Cons, simp) |
|
157 |
apply (drule has_only_SaysD, simp+) |
|
158 |
by (clarify, case_tac x, auto) |
|
159 |
||
160 |
subsection{*types*} |
|
161 |
||
162 |
types keyfun = "rule => subs => nat => event list => key set" |
|
163 |
||
164 |
types secfun = "rule => nat => subs => key set => msg" |
|
165 |
||
166 |
subsection{*introduction of a fresh guarded nonce*} |
|
167 |
||
168 |
constdefs fresh :: "proto => rule => subs => nat => key set => event list |
|
169 |
=> bool" |
|
170 |
"fresh p R s n Ks evs == (EX evs1 evs2. evs = evs2 @ ap' s R # evs1 |
|
171 |
& Nonce n ~:used evs1 & R:p & ok evs1 R s & Nonce n:parts {apm' s R} |
|
172 |
& apm' s R:guard n Ks)" |
|
173 |
||
174 |
lemma freshD: "fresh p R s n Ks evs ==> (EX evs1 evs2. |
|
175 |
evs = evs2 @ ap' s R # evs1 & Nonce n ~:used evs1 & R:p & ok evs1 R s |
|
176 |
& Nonce n:parts {apm' s R} & apm' s R:guard n Ks)" |
|
177 |
by (unfold fresh_def, blast) |
|
178 |
||
179 |
lemma freshI [intro]: "[| Nonce n ~:used evs1; R:p; Nonce n:parts {apm' s R}; |
|
180 |
ok evs1 R s; apm' s R:guard n Ks |] |
|
181 |
==> fresh p R s n Ks (list @ ap' s R # evs1)" |
|
182 |
by (unfold fresh_def, blast) |
|
183 |
||
184 |
lemma freshI': "[| Nonce n ~:used evs1; (l,r):p; |
|
185 |
Nonce n:parts {apm s (msg r)}; ok evs1 (l,r) s; apm s (msg r):guard n Ks |] |
|
186 |
==> fresh p (l,r) s n Ks (evs2 @ ap s r # evs1)" |
|
187 |
by (drule freshI, simp+) |
|
188 |
||
189 |
lemma fresh_used: "[| fresh p R' s' n Ks evs; has_only_Says' p |] |
|
190 |
==> Nonce n:used evs" |
|
191 |
apply (unfold fresh_def, clarify) |
|
192 |
apply (drule has_only_Says'D) |
|
193 |
by (auto intro: parts_used_app) |
|
194 |
||
195 |
lemma fresh_newn: "[| evs' @ ap' s R # evs:tr p; wdef p; has_only_Says' p; |
|
196 |
Nonce n ~:used evs; R:p; ok evs R s; Nonce n:parts {apm' s R} |] |
|
197 |
==> EX k. k:newn R & nonce s k = n" |
|
198 |
apply (drule wdef_Nonce, simp+) |
|
199 |
apply (frule ok_not_used, simp+) |
|
200 |
apply (clarify, erule ok_is_Says, simp+) |
|
201 |
apply (clarify, rule_tac x=k in exI, simp add: newn_def) |
|
202 |
apply (clarify, drule_tac Y="msg x" and s=s in apm_parts) |
|
203 |
apply (drule ok_not_used, simp+) |
|
13601 | 204 |
by (clarify, erule ok_is_Says, simp+) |
13508 | 205 |
|
206 |
lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs; |
|
207 |
Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev" |
|
208 |
apply (drule trunc, simp, ind_cases "ev # evs:tr p", simp) |
|
209 |
by (drule_tac x=X in in_sub, drule parts_sub, simp, simp, blast+) |
|
210 |
||
211 |
lemma fresh_ruleD: "[| fresh p R' s' n Ks evs; keys R' s' n evs <= Ks; wdef p; |
|
212 |
has_only_Says' p; evs:tr p; ALL R k s. nonce s k = n --> Nonce n:used evs --> |
|
213 |
R:p --> k:newn R --> Nonce n:parts {apm' s R} --> apm' s R:guard n Ks --> |
|
214 |
apm' s R:parts (spies evs) --> keys R s n evs <= Ks --> P |] ==> P" |
|
215 |
apply (frule fresh_used, simp) |
|
216 |
apply (unfold fresh_def, clarify) |
|
217 |
apply (drule_tac x=R' in spec) |
|
218 |
apply (drule fresh_newn, simp+, clarify) |
|
219 |
apply (drule_tac x=k in spec) |
|
220 |
apply (drule_tac x=s' in spec) |
|
221 |
apply (subgoal_tac "apm' s' R':parts (spies (evs2 @ ap' s' R' # evs1))") |
|
222 |
apply (case_tac R', drule has_only_Says'D, simp, clarsimp) |
|
223 |
apply (case_tac R', drule has_only_Says'D, simp, clarsimp) |
|
224 |
apply (rule_tac Y="apm s' X" in parts_parts, blast) |
|
225 |
by (rule parts.Inj, rule Says_imp_spies, simp, blast) |
|
226 |
||
227 |
subsection{*safe keys*} |
|
228 |
||
229 |
constdefs safe :: "key set => msg set => bool" |
|
230 |
"safe Ks G == ALL K. K:Ks --> Key K ~:analz G" |
|
231 |
||
232 |
lemma safeD [dest]: "[| safe Ks G; K:Ks |] ==> Key K ~:analz G" |
|
233 |
by (unfold safe_def, blast) |
|
234 |
||
235 |
lemma safe_insert: "safe Ks (insert X G) ==> safe Ks G" |
|
236 |
by (unfold safe_def, blast) |
|
237 |
||
238 |
lemma Guard_safe: "[| Guard n Ks G; safe Ks G |] ==> Nonce n ~:analz G" |
|
239 |
by (blast dest: Guard_invKey) |
|
240 |
||
241 |
subsection{*guardedness preservation*} |
|
242 |
||
243 |
constdefs preserv :: "proto => keyfun => nat => key set => bool" |
|
244 |
"preserv p keys n Ks == (ALL evs R' s' R s. evs:tr p --> |
|
245 |
Guard n Ks (spies evs) --> safe Ks (spies evs) --> fresh p R' s' n Ks evs --> |
|
246 |
keys R' s' n evs <= Ks --> R:p --> ok evs R s --> apm' s R:guard n Ks)" |
|
247 |
||
248 |
lemma preservD: "[| preserv p keys n Ks; evs:tr p; Guard n Ks (spies evs); |
|
249 |
safe Ks (spies evs); fresh p R' s' n Ks evs; R:p; ok evs R s; |
|
250 |
keys R' s' n evs <= Ks |] ==> apm' s R:guard n Ks" |
|
251 |
by (unfold preserv_def, blast) |
|
252 |
||
253 |
lemma preservD': "[| preserv p keys n Ks; evs:tr p; Guard n Ks (spies evs); |
|
254 |
safe Ks (spies evs); fresh p R' s' n Ks evs; (l,Says A B X):p; |
|
255 |
ok evs (l,Says A B X) s; keys R' s' n evs <= Ks |] ==> apm s X:guard n Ks" |
|
256 |
by (drule preservD, simp+) |
|
257 |
||
258 |
subsection{*monotonic keyfun*} |
|
259 |
||
260 |
constdefs monoton :: "proto => keyfun => bool" |
|
261 |
"monoton p keys == ALL R' s' n ev evs. ev # evs:tr p --> |
|
262 |
keys R' s' n evs <= keys R' s' n (ev # evs)" |
|
263 |
||
264 |
lemma monotonD [dest]: "[| keys R' s' n (ev # evs) <= Ks; monoton p keys; |
|
265 |
ev # evs:tr p |] ==> keys R' s' n evs <= Ks" |
|
266 |
by (unfold monoton_def, blast) |
|
267 |
||
268 |
subsection{*guardedness theorem*} |
|
269 |
||
270 |
lemma Guard_tr [rule_format]: "[| evs:tr p; has_only_Says' p; |
|
271 |
preserv p keys n Ks; monoton p keys; Guard n Ks (initState Spy) |] ==> |
|
272 |
safe Ks (spies evs) --> fresh p R' s' n Ks evs --> keys R' s' n evs <= Ks --> |
|
273 |
Guard n Ks (spies evs)" |
|
274 |
apply (erule tr.induct) |
|
275 |
(* Nil *) |
|
276 |
apply simp |
|
277 |
(* Fake *) |
|
278 |
apply (clarify, drule freshD, clarsimp) |
|
279 |
apply (case_tac evs2) |
|
280 |
(* evs2 = [] *) |
|
281 |
apply (frule has_only_Says'D, simp) |
|
282 |
apply (clarsimp, blast) |
|
283 |
(* evs2 = aa # list *) |
|
284 |
apply (clarsimp, rule conjI) |
|
285 |
apply (blast dest: safe_insert) |
|
286 |
(* X:guard n Ks *) |
|
287 |
apply (rule in_synth_Guard, simp, rule Guard_analz) |
|
288 |
apply (blast dest: safe_insert) |
|
289 |
apply (drule safe_insert, simp add: safe_def) |
|
290 |
(* Proto *) |
|
291 |
apply (clarify, drule freshD, clarify) |
|
292 |
apply (case_tac evs2) |
|
293 |
(* evs2 = [] *) |
|
294 |
apply (frule has_only_Says'D, simp) |
|
295 |
apply (frule_tac R=R' in has_only_Says'D, simp) |
|
296 |
apply (case_tac R', clarsimp, blast) |
|
297 |
(* evs2 = ab # list *) |
|
298 |
apply (frule has_only_Says'D, simp) |
|
299 |
apply (clarsimp, rule conjI) |
|
300 |
apply (drule Proto, simp+, blast dest: safe_insert) |
|
301 |
(* apm s X:guard n Ks *) |
|
302 |
apply (frule Proto, simp+) |
|
303 |
apply (erule preservD', simp+) |
|
304 |
apply (blast dest: safe_insert) |
|
305 |
apply (blast dest: safe_insert) |
|
306 |
by (blast, simp, simp, blast) |
|
307 |
||
308 |
subsection{*useful properties for guardedness*} |
|
309 |
||
310 |
lemma newn_neq_used: "[| Nonce n:used evs; ok evs R s; k:newn R |] |
|
311 |
==> n ~= nonce s k" |
|
312 |
by (auto simp: ok_def) |
|
313 |
||
314 |
lemma ok_Guard: "[| ok evs R s; Guard n Ks (spies evs); x:fst R; is_Says x |] |
|
315 |
==> apm s (msg x):parts (spies evs) & apm s (msg x):guard n Ks" |
|
316 |
apply (unfold ok_def is_Says_def, clarify) |
|
317 |
apply (drule_tac x="Says A B X" in spec, simp) |
|
318 |
by (drule Says_imp_spies, auto intro: parts_parts) |
|
319 |
||
320 |
lemma ok_parts_not_new: "[| Y:parts (spies evs); Nonce (nonce s n):parts {Y}; |
|
321 |
ok evs R s |] ==> n ~:newn R" |
|
322 |
by (auto simp: ok_def dest: not_used_not_spied parts_parts) |
|
323 |
||
324 |
subsection{*unicity*} |
|
325 |
||
326 |
constdefs uniq :: "proto => secfun => bool" |
|
327 |
"uniq p secret == ALL evs R R' n n' Ks s s'. R:p --> R':p --> |
|
328 |
n:newn R --> n':newn R' --> nonce s n = nonce s' n' --> |
|
329 |
Nonce (nonce s n):parts {apm' s R} --> Nonce (nonce s n):parts {apm' s' R'} --> |
|
330 |
apm' s R:guard (nonce s n) Ks --> apm' s' R':guard (nonce s n) Ks --> |
|
331 |
evs:tr p --> Nonce (nonce s n) ~:analz (spies evs) --> |
|
332 |
secret R n s Ks:parts (spies evs) --> secret R' n' s' Ks:parts (spies evs) --> |
|
333 |
secret R n s Ks = secret R' n' s' Ks" |
|
334 |
||
335 |
lemma uniqD: "[| uniq p secret; evs: tr p; R:p; R':p; n:newn R; n':newn R'; |
|
336 |
nonce s n = nonce s' n'; Nonce (nonce s n) ~:analz (spies evs); |
|
337 |
Nonce (nonce s n):parts {apm' s R}; Nonce (nonce s n):parts {apm' s' R'}; |
|
338 |
secret R n s Ks:parts (spies evs); secret R' n' s' Ks:parts (spies evs); |
|
339 |
apm' s R:guard (nonce s n) Ks; apm' s' R':guard (nonce s n) Ks |] ==> |
|
340 |
secret R n s Ks = secret R' n' s' Ks" |
|
341 |
by (unfold uniq_def, blast) |
|
342 |
||
343 |
constdefs ord :: "proto => (rule => rule => bool) => bool" |
|
22426 | 344 |
"ord p inff == ALL R R'. R:p --> R':p --> ~ inff R R' --> inff R' R" |
13508 | 345 |
|
22426 | 346 |
lemma ordD: "[| ord p inff; ~ inff R R'; R:p; R':p |] ==> inff R' R" |
13508 | 347 |
by (unfold ord_def, blast) |
348 |
||
349 |
constdefs uniq' :: "proto => (rule => rule => bool) => secfun => bool" |
|
22426 | 350 |
"uniq' p inff secret == ALL evs R R' n n' Ks s s'. R:p --> R':p --> |
351 |
inff R R' --> n:newn R --> n':newn R' --> nonce s n = nonce s' n' --> |
|
13508 | 352 |
Nonce (nonce s n):parts {apm' s R} --> Nonce (nonce s n):parts {apm' s' R'} --> |
353 |
apm' s R:guard (nonce s n) Ks --> apm' s' R':guard (nonce s n) Ks --> |
|
354 |
evs:tr p --> Nonce (nonce s n) ~:analz (spies evs) --> |
|
355 |
secret R n s Ks:parts (spies evs) --> secret R' n' s' Ks:parts (spies evs) --> |
|
356 |
secret R n s Ks = secret R' n' s' Ks" |
|
357 |
||
22426 | 358 |
lemma uniq'D: "[| uniq' p inff secret; evs: tr p; inff R R'; R:p; R':p; n:newn R; |
13508 | 359 |
n':newn R'; nonce s n = nonce s' n'; Nonce (nonce s n) ~:analz (spies evs); |
360 |
Nonce (nonce s n):parts {apm' s R}; Nonce (nonce s n):parts {apm' s' R'}; |
|
361 |
secret R n s Ks:parts (spies evs); secret R' n' s' Ks:parts (spies evs); |
|
362 |
apm' s R:guard (nonce s n) Ks; apm' s' R':guard (nonce s n) Ks |] ==> |
|
363 |
secret R n s Ks = secret R' n' s' Ks" |
|
364 |
by (unfold uniq'_def, blast) |
|
365 |
||
22426 | 366 |
lemma uniq'_imp_uniq: "[| uniq' p inff secret; ord p inff |] ==> uniq p secret" |
13508 | 367 |
apply (unfold uniq_def) |
368 |
apply (rule allI)+ |
|
22426 | 369 |
apply (case_tac "inff R R'") |
13508 | 370 |
apply (blast dest: uniq'D) |
371 |
by (auto dest: ordD uniq'D intro: sym) |
|
372 |
||
373 |
subsection{*Needham-Schroeder-Lowe*} |
|
374 |
||
375 |
constdefs |
|
376 |
a :: agent "a == Friend 0" |
|
377 |
b :: agent "b == Friend 1" |
|
378 |
a' :: agent "a' == Friend 2" |
|
379 |
b' :: agent "b' == Friend 3" |
|
380 |
Na :: nat "Na == 0" |
|
381 |
Nb :: nat "Nb == 1" |
|
382 |
||
20768 | 383 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
384 |
ns1 :: rule where |
20768 | 385 |
"ns1 == ({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))" |
13508 | 386 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
387 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
388 |
ns2 :: rule where |
20768 | 389 |
"ns2 == ({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})}, |
390 |
Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))" |
|
13508 | 391 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
392 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
393 |
ns3 :: rule where |
20768 | 394 |
"ns3 == ({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}), |
395 |
Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})}, |
|
396 |
Says a b (Crypt (pubK b) (Nonce Nb)))" |
|
13508 | 397 |
|
23746 | 398 |
inductive_set ns :: proto where |
399 |
[iff]: "ns1:ns" |
|
400 |
| [iff]: "ns2:ns" |
|
401 |
| [iff]: "ns3:ns" |
|
13508 | 402 |
|
20768 | 403 |
abbreviation (input) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
404 |
ns3a :: event where |
20768 | 405 |
"ns3a == Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})" |
13508 | 406 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
407 |
abbreviation (input) |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
408 |
ns3b :: event where |
20768 | 409 |
"ns3b == Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})" |
13508 | 410 |
|
411 |
constdefs keys :: "keyfun" |
|
412 |
"keys R' s' n evs == {priK' s' a, priK' s' b}" |
|
413 |
||
414 |
lemma "monoton ns keys" |
|
415 |
by (simp add: keys_def monoton_def) |
|
416 |
||
417 |
constdefs secret :: "secfun" |
|
418 |
"secret R n s Ks == |
|
419 |
(if R=ns1 then apm s (Crypt (pubK b) {|Nonce Na, Agent a|}) |
|
420 |
else if R=ns2 then apm s (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}) |
|
421 |
else Number 0)" |
|
422 |
||
423 |
constdefs inf :: "rule => rule => bool" |
|
424 |
"inf R R' == (R=ns1 | (R=ns2 & R'~=ns1) | (R=ns3 & R'=ns3))" |
|
425 |
||
426 |
lemma inf_is_ord [iff]: "ord ns inf" |
|
427 |
apply (unfold ord_def inf_def) |
|
428 |
apply (rule allI)+ |
|
23746 | 429 |
apply (rule impI) |
430 |
apply (simp add: split_paired_all) |
|
13508 | 431 |
by (rule impI, erule ns.cases, simp_all)+ |
432 |
||
433 |
subsection{*general properties*} |
|
434 |
||
435 |
lemma ns_has_only_Says' [iff]: "has_only_Says' ns" |
|
436 |
apply (unfold has_only_Says'_def) |
|
437 |
apply (rule allI, rule impI) |
|
23746 | 438 |
apply (simp add: split_paired_all) |
13508 | 439 |
by (erule ns.cases, auto) |
440 |
||
441 |
lemma newn_ns1 [iff]: "newn ns1 = {Na}" |
|
442 |
by (simp add: newn_def) |
|
443 |
||
444 |
lemma newn_ns2 [iff]: "newn ns2 = {Nb}" |
|
445 |
by (auto simp: newn_def Na_def Nb_def) |
|
446 |
||
447 |
lemma newn_ns3 [iff]: "newn ns3 = {}" |
|
448 |
by (auto simp: newn_def) |
|
449 |
||
450 |
lemma ns_wdef [iff]: "wdef ns" |
|
451 |
by (auto simp: wdef_def elim: ns.cases) |
|
452 |
||
453 |
subsection{*guardedness for NSL*} |
|
454 |
||
455 |
lemma "uniq ns secret ==> preserv ns keys n Ks" |
|
456 |
apply (unfold preserv_def) |
|
457 |
apply (rule allI)+ |
|
458 |
apply (rule impI, rule impI, rule impI, rule impI, rule impI) |
|
459 |
apply (erule fresh_ruleD, simp, simp, simp, simp) |
|
460 |
apply (rule allI)+ |
|
461 |
apply (rule impI, rule impI, rule impI) |
|
23746 | 462 |
apply (simp add: split_paired_all) |
13508 | 463 |
apply (erule ns.cases) |
464 |
(* fresh with NS1 *) |
|
465 |
apply (rule impI, rule impI, rule impI, rule impI, rule impI, rule impI) |
|
466 |
apply (erule ns.cases) |
|
467 |
(* NS1 *) |
|
468 |
apply clarsimp |
|
469 |
apply (frule newn_neq_used, simp, simp) |
|
470 |
apply (rule No_Nonce, simp) |
|
471 |
(* NS2 *) |
|
472 |
apply clarsimp |
|
473 |
apply (frule newn_neq_used, simp, simp) |
|
474 |
apply (case_tac "nonce sa Na = nonce s Na") |
|
475 |
apply (frule Guard_safe, simp) |
|
476 |
apply (frule Crypt_guard_invKey, simp) |
|
477 |
apply (frule ok_Guard, simp, simp, simp, clarsimp) |
|
478 |
apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp) |
|
479 |
apply (frule_tac R=ns1 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+) |
|
480 |
apply (simp add: secret_def, simp add: secret_def, force, force) |
|
481 |
apply (simp add: secret_def keys_def, blast) |
|
482 |
apply (rule No_Nonce, simp) |
|
483 |
(* NS3 *) |
|
484 |
apply clarsimp |
|
485 |
apply (case_tac "nonce sa Na = nonce s Nb") |
|
486 |
apply (frule Guard_safe, simp) |
|
487 |
apply (frule Crypt_guard_invKey, simp) |
|
488 |
apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp) |
|
489 |
apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp) |
|
490 |
apply (frule_tac R=ns1 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+) |
|
491 |
apply (simp add: secret_def, simp add: secret_def, force, force) |
|
492 |
apply (simp add: secret_def, rule No_Nonce, simp) |
|
493 |
(* fresh with NS2 *) |
|
494 |
apply (rule impI, rule impI, rule impI, rule impI, rule impI, rule impI) |
|
495 |
apply (erule ns.cases) |
|
496 |
(* NS1 *) |
|
497 |
apply clarsimp |
|
498 |
apply (frule newn_neq_used, simp, simp) |
|
499 |
apply (rule No_Nonce, simp) |
|
500 |
(* NS2 *) |
|
501 |
apply clarsimp |
|
502 |
apply (frule newn_neq_used, simp, simp) |
|
503 |
apply (case_tac "nonce sa Nb = nonce s Na") |
|
504 |
apply (frule Guard_safe, simp) |
|
505 |
apply (frule Crypt_guard_invKey, simp) |
|
506 |
apply (frule ok_Guard, simp, simp, simp, clarsimp) |
|
507 |
apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp) |
|
508 |
apply (frule_tac R=ns2 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+) |
|
509 |
apply (simp add: secret_def, simp add: secret_def, force, force) |
|
510 |
apply (simp add: secret_def, rule No_Nonce, simp) |
|
511 |
(* NS3 *) |
|
512 |
apply clarsimp |
|
513 |
apply (case_tac "nonce sa Nb = nonce s Nb") |
|
514 |
apply (frule Guard_safe, simp) |
|
515 |
apply (frule Crypt_guard_invKey, simp) |
|
516 |
apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp) |
|
517 |
apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp) |
|
518 |
apply (frule_tac R=ns2 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+) |
|
519 |
apply (simp add: secret_def, simp add: secret_def, force, force) |
|
520 |
apply (simp add: secret_def keys_def, blast) |
|
521 |
apply (rule No_Nonce, simp) |
|
522 |
(* fresh with NS3 *) |
|
523 |
by simp |
|
524 |
||
525 |
subsection{*unicity for NSL*} |
|
526 |
||
527 |
lemma "uniq' ns inf secret" |
|
528 |
apply (unfold uniq'_def) |
|
529 |
apply (rule allI)+ |
|
23746 | 530 |
apply (simp add: split_paired_all) |
13508 | 531 |
apply (rule impI, erule ns.cases) |
532 |
(* R = ns1 *) |
|
533 |
apply (rule impI, erule ns.cases) |
|
534 |
(* R' = ns1 *) |
|
535 |
apply (rule impI, rule impI, rule impI, rule impI) |
|
536 |
apply (rule impI, rule impI, rule impI, rule impI) |
|
537 |
apply (rule impI, erule tr.induct) |
|
538 |
(* Nil *) |
|
539 |
apply (simp add: secret_def) |
|
540 |
(* Fake *) |
|
541 |
apply (clarify, simp add: secret_def) |
|
542 |
apply (drule notin_analz_insert) |
|
543 |
apply (drule Crypt_insert_synth, simp, simp, simp) |
|
544 |
apply (drule Crypt_insert_synth, simp, simp, simp, simp) |
|
545 |
(* Proto *) |
|
23746 | 546 |
apply (erule_tac P="ok evsa R sa" in rev_mp) |
547 |
apply (simp add: split_paired_all) |
|
13508 | 548 |
apply (erule ns.cases) |
549 |
(* ns1 *) |
|
550 |
apply (clarify, simp add: secret_def) |
|
551 |
apply (erule disjE, erule disjE, clarsimp) |
|
552 |
apply (drule ok_parts_not_new, simp, simp, simp) |
|
553 |
apply (clarify, drule ok_parts_not_new, simp, simp, simp) |
|
554 |
(* ns2 *) |
|
555 |
apply (simp add: secret_def) |
|
556 |
(* ns3 *) |
|
557 |
apply (simp add: secret_def) |
|
558 |
(* R' = ns2 *) |
|
559 |
apply (rule impI, rule impI, rule impI, rule impI) |
|
560 |
apply (rule impI, rule impI, rule impI, rule impI) |
|
561 |
apply (rule impI, erule tr.induct) |
|
562 |
(* Nil *) |
|
563 |
apply (simp add: secret_def) |
|
564 |
(* Fake *) |
|
565 |
apply (clarify, simp add: secret_def) |
|
566 |
apply (drule notin_analz_insert) |
|
567 |
apply (drule Crypt_insert_synth, simp, simp, simp) |
|
568 |
apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp) |
|
569 |
(* Proto *) |
|
23746 | 570 |
apply (erule_tac P="ok evsa R sa" in rev_mp) |
571 |
apply (simp add: split_paired_all) |
|
13508 | 572 |
apply (erule ns.cases) |
573 |
(* ns1 *) |
|
574 |
apply (clarify, simp add: secret_def) |
|
575 |
apply (drule_tac s=sa and n=Na in ok_parts_not_new, simp, simp, simp) |
|
576 |
(* ns2 *) |
|
577 |
apply (clarify, simp add: secret_def) |
|
578 |
apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp) |
|
579 |
(* ns3 *) |
|
580 |
apply (simp add: secret_def) |
|
581 |
(* R' = ns3 *) |
|
582 |
apply simp |
|
583 |
(* R = ns2 *) |
|
584 |
apply (rule impI, erule ns.cases) |
|
585 |
(* R' = ns1 *) |
|
586 |
apply (simp only: inf_def, blast) |
|
587 |
(* R' = ns2 *) |
|
588 |
apply (rule impI, rule impI, rule impI, rule impI) |
|
589 |
apply (rule impI, rule impI, rule impI, rule impI) |
|
590 |
apply (rule impI, erule tr.induct) |
|
591 |
(* Nil *) |
|
592 |
apply (simp add: secret_def) |
|
593 |
(* Fake *) |
|
594 |
apply (clarify, simp add: secret_def) |
|
595 |
apply (drule notin_analz_insert) |
|
596 |
apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp) |
|
597 |
apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp) |
|
598 |
(* Proto *) |
|
23746 | 599 |
apply (erule_tac P="ok evsa R sa" in rev_mp) |
600 |
apply (simp add: split_paired_all) |
|
13508 | 601 |
apply (erule ns.cases) |
602 |
(* ns1 *) |
|
603 |
apply (simp add: secret_def) |
|
604 |
(* ns2 *) |
|
605 |
apply (clarify, simp add: secret_def) |
|
606 |
apply (erule disjE, erule disjE, clarsimp, clarsimp) |
|
607 |
apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp) |
|
608 |
apply (erule disjE, clarsimp) |
|
609 |
apply (drule_tac s=sa and n=Nb in ok_parts_not_new, simp, simp, simp) |
|
610 |
by (simp_all add: secret_def) |
|
611 |
||
612 |
end |