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