author | wenzelm |
Thu, 10 Dec 2015 21:39:33 +0100 | |
changeset 61830 | 4f5ab843cf5b |
parent 58889 | 5b7a9633cfa8 |
child 61956 | 38b73f7940af |
permissions | -rw-r--r-- |
41775 | 1 |
(* Title: HOL/Auth/Guard/P1.thy |
2 |
Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
|
3 |
Copyright 2002 University of Cambridge |
|
13508 | 4 |
|
41775 | 5 |
From G. Karjoth, N. Asokan and C. Gulcu |
6 |
"Protecting the computation results of free-roaming agents" |
|
7 |
Mobiles Agents 1998, LNCS 1477. |
|
8 |
*) |
|
13508 | 9 |
|
61830 | 10 |
section\<open>Protocol P1\<close> |
13508 | 11 |
|
39216 | 12 |
theory P1 imports "../Public" Guard_Public List_Msg begin |
13508 | 13 |
|
61830 | 14 |
subsection\<open>Protocol Definition\<close> |
13508 | 15 |
|
16 |
(****************************************************************************** |
|
17 |
||
18 |
the contents of the messages are not completely specified in the paper |
|
19 |
we assume that the user sends his request and his itinerary in the clear |
|
20 |
||
21 |
we will adopt the following format for messages: {|A,r,I,L|} |
|
22 |
A: originator (agent) |
|
23 |
r: request (number) |
|
24 |
I: next shops (agent list) |
|
25 |
L: collected offers (offer list) |
|
26 |
||
27 |
in the paper, the authors use nonces r_i to add redundancy in the offer |
|
28 |
in order to make it safer against dictionary attacks |
|
29 |
it is not necessary in our modelization since crypto is assumed to be strong |
|
30 |
(Crypt in injective) |
|
31 |
******************************************************************************) |
|
32 |
||
61830 | 33 |
subsubsection\<open>offer chaining: |
34 |
B chains his offer for A with the head offer of L for sending it to C\<close> |
|
13508 | 35 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
36 |
definition chain :: "agent => nat => agent => msg => agent => msg" where |
13508 | 37 |
"chain B ofr A L C == |
38 |
let m1= Crypt (pubK A) (Nonce ofr) in |
|
39 |
let m2= Hash {|head L, Agent C|} in |
|
40 |
sign B {|m1,m2|}" |
|
41 |
||
42 |
declare Let_def [simp] |
|
43 |
||
44 |
lemma chain_inj [iff]: "(chain B ofr A L C = chain B' ofr' A' L' C') |
|
45 |
= (B=B' & ofr=ofr' & A=A' & head L = head L' & C=C')" |
|
46 |
by (auto simp: chain_def Let_def) |
|
47 |
||
48 |
lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}" |
|
49 |
by (auto simp: chain_def sign_def) |
|
50 |
||
61830 | 51 |
subsubsection\<open>agent whose key is used to sign an offer\<close> |
13508 | 52 |
|
35418 | 53 |
fun shop :: "msg => msg" where |
13508 | 54 |
"shop {|B,X,Crypt K H|} = Agent (agt K)" |
55 |
||
56 |
lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B" |
|
57 |
by (simp add: chain_def sign_def) |
|
58 |
||
61830 | 59 |
subsubsection\<open>nonce used in an offer\<close> |
13508 | 60 |
|
35418 | 61 |
fun nonce :: "msg => msg" where |
13508 | 62 |
"nonce {|B,{|Crypt K ofr,m2|},CryptH|} = ofr" |
63 |
||
64 |
lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr" |
|
65 |
by (simp add: chain_def sign_def) |
|
66 |
||
61830 | 67 |
subsubsection\<open>next shop\<close> |
13508 | 68 |
|
35418 | 69 |
fun next_shop :: "msg => agent" where |
13508 | 70 |
"next_shop {|B,{|m1,Hash{|headL,Agent C|}|},CryptH|} = C" |
71 |
||
72 |
lemma next_shop_chain [iff]: "next_shop (chain B ofr A L C) = C" |
|
73 |
by (simp add: chain_def sign_def) |
|
74 |
||
61830 | 75 |
subsubsection\<open>anchor of the offer list\<close> |
13508 | 76 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
77 |
definition anchor :: "agent => nat => agent => msg" where |
13508 | 78 |
"anchor A n B == chain A n A (cons nil nil) B" |
79 |
||
80 |
lemma anchor_inj [iff]: "(anchor A n B = anchor A' n' B') |
|
81 |
= (A=A' & n=n' & B=B')" |
|
82 |
by (auto simp: anchor_def) |
|
83 |
||
84 |
lemma Nonce_in_anchor [iff]: "Nonce n:parts {anchor A n B}" |
|
85 |
by (auto simp: anchor_def) |
|
86 |
||
87 |
lemma shop_anchor [simp]: "shop (anchor A n B) = Agent A" |
|
88 |
by (simp add: anchor_def) |
|
89 |
||
90 |
lemma nonce_anchor [simp]: "nonce (anchor A n B) = Nonce n" |
|
91 |
by (simp add: anchor_def) |
|
92 |
||
93 |
lemma next_shop_anchor [iff]: "next_shop (anchor A n B) = B" |
|
94 |
by (simp add: anchor_def) |
|
95 |
||
61830 | 96 |
subsubsection\<open>request event\<close> |
13508 | 97 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
98 |
definition reqm :: "agent => nat => nat => msg => agent => msg" where |
13508 | 99 |
"reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I), |
100 |
cons (anchor A n B) nil|}" |
|
101 |
||
102 |
lemma reqm_inj [iff]: "(reqm A r n I B = reqm A' r' n' I' B') |
|
103 |
= (A=A' & r=r' & n=n' & I=I' & B=B')" |
|
104 |
by (auto simp: reqm_def) |
|
105 |
||
106 |
lemma Nonce_in_reqm [iff]: "Nonce n:parts {reqm A r n I B}" |
|
107 |
by (auto simp: reqm_def) |
|
108 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
109 |
definition req :: "agent => nat => nat => msg => agent => event" where |
13508 | 110 |
"req A r n I B == Says A B (reqm A r n I B)" |
111 |
||
112 |
lemma req_inj [iff]: "(req A r n I B = req A' r' n' I' B') |
|
113 |
= (A=A' & r=r' & n=n' & I=I' & B=B')" |
|
114 |
by (auto simp: req_def) |
|
115 |
||
61830 | 116 |
subsubsection\<open>propose event\<close> |
13508 | 117 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
118 |
definition prom :: "agent => nat => agent => nat => msg => msg => |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
119 |
msg => agent => msg" where |
13508 | 120 |
"prom B ofr A r I L J C == {|Agent A, Number r, |
121 |
app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}" |
|
122 |
||
123 |
lemma prom_inj [dest]: "prom B ofr A r I L J C |
|
124 |
= prom B' ofr' A' r' I' L' J' C' |
|
125 |
==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'" |
|
126 |
by (auto simp: prom_def) |
|
127 |
||
128 |
lemma Nonce_in_prom [iff]: "Nonce ofr:parts {prom B ofr A r I L J C}" |
|
129 |
by (auto simp: prom_def) |
|
130 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
131 |
definition pro :: "agent => nat => agent => nat => msg => msg => |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
132 |
msg => agent => event" where |
13508 | 133 |
"pro B ofr A r I L J C == Says B C (prom B ofr A r I L J C)" |
134 |
||
135 |
lemma pro_inj [dest]: "pro B ofr A r I L J C = pro B' ofr' A' r' I' L' J' C' |
|
136 |
==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'" |
|
137 |
by (auto simp: pro_def dest: prom_inj) |
|
138 |
||
61830 | 139 |
subsubsection\<open>protocol\<close> |
13508 | 140 |
|
23746 | 141 |
inductive_set p1 :: "event list set" |
142 |
where |
|
13508 | 143 |
|
23746 | 144 |
Nil: "[]:p1" |
13508 | 145 |
|
23746 | 146 |
| Fake: "[| evsf:p1; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p1" |
13508 | 147 |
|
23746 | 148 |
| Request: "[| evsr:p1; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p1" |
13508 | 149 |
|
23746 | 150 |
| Propose: "[| evsp:p1; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp; |
151 |
I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I))); |
|
152 |
Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p1" |
|
13508 | 153 |
|
61830 | 154 |
subsubsection\<open>Composition of Traces\<close> |
13508 | 155 |
|
156 |
lemma "evs':p1 ==> |
|
157 |
evs:p1 & (ALL n. Nonce n:used evs' --> Nonce n ~:used evs) --> |
|
158 |
evs'@evs : p1" |
|
159 |
apply (erule p1.induct, safe) |
|
160 |
apply (simp_all add: used_ConsI) |
|
161 |
apply (erule p1.Fake, erule synth_sub, rule analz_mono, rule knows_sub_app) |
|
162 |
apply (erule p1.Request, safe, simp_all add: req_def, force) |
|
163 |
apply (erule_tac A'=A' in p1.Propose, simp_all) |
|
164 |
apply (drule_tac x=ofr in spec, simp add: pro_def, blast) |
|
165 |
apply (erule_tac A'=A' in p1.Propose, auto simp: pro_def) |
|
166 |
done |
|
167 |
||
61830 | 168 |
subsubsection\<open>Valid Offer Lists\<close> |
13508 | 169 |
|
23746 | 170 |
inductive_set |
171 |
valid :: "agent => nat => agent => msg set" |
|
172 |
for A :: agent and n :: nat and B :: agent |
|
173 |
where |
|
174 |
Request [intro]: "cons (anchor A n B) nil:valid A n B" |
|
13508 | 175 |
|
23746 | 176 |
| Propose [intro]: "L:valid A n B |
13508 | 177 |
==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B" |
178 |
||
61830 | 179 |
subsubsection\<open>basic properties of valid\<close> |
13508 | 180 |
|
181 |
lemma valid_not_empty: "L:valid A n B ==> EX M L'. L = cons M L'" |
|
182 |
by (erule valid.cases, auto) |
|
183 |
||
184 |
lemma valid_pos_len: "L:valid A n B ==> 0 < len L" |
|
185 |
by (erule valid.induct, auto) |
|
186 |
||
61830 | 187 |
subsubsection\<open>offers of an offer list\<close> |
13508 | 188 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
189 |
definition offer_nonces :: "msg => msg set" where |
13508 | 190 |
"offer_nonces L == {X. X:parts {L} & (EX n. X = Nonce n)}" |
191 |
||
61830 | 192 |
subsubsection\<open>the originator can get the offers\<close> |
13508 | 193 |
|
194 |
lemma "L:valid A n B ==> offer_nonces L <= analz (insert L (initState A))" |
|
195 |
by (erule valid.induct, auto simp: anchor_def chain_def sign_def |
|
196 |
offer_nonces_def initState.simps) |
|
197 |
||
61830 | 198 |
subsubsection\<open>list of offers\<close> |
13508 | 199 |
|
35418 | 200 |
fun offers :: "msg => msg" where |
201 |
"offers (cons M L) = cons {|shop M, nonce M|} (offers L)" | |
|
13508 | 202 |
"offers other = nil" |
203 |
||
61830 | 204 |
subsubsection\<open>list of agents whose keys are used to sign a list of offers\<close> |
13508 | 205 |
|
35418 | 206 |
fun shops :: "msg => msg" where |
207 |
"shops (cons M L) = cons (shop M) (shops L)" | |
|
13508 | 208 |
"shops other = other" |
209 |
||
210 |
lemma shops_in_agl: "L:valid A n B ==> shops L:agl" |
|
211 |
by (erule valid.induct, auto simp: anchor_def chain_def sign_def) |
|
212 |
||
61830 | 213 |
subsubsection\<open>builds a trace from an itinerary\<close> |
13508 | 214 |
|
35418 | 215 |
fun offer_list :: "agent * nat * agent * msg * nat => msg" where |
216 |
"offer_list (A,n,B,nil,ofr) = cons (anchor A n B) nil" | |
|
13508 | 217 |
"offer_list (A,n,B,cons (Agent C) I,ofr) = ( |
218 |
let L = offer_list (A,n,B,I,Suc ofr) in |
|
219 |
cons (chain (next_shop (head L)) ofr A L C) L)" |
|
220 |
||
221 |
lemma "I:agl ==> ALL ofr. offer_list (A,n,B,I,ofr):valid A n B" |
|
222 |
by (erule agl.induct, auto) |
|
223 |
||
35418 | 224 |
fun trace :: "agent * nat * agent * nat * msg * msg * msg |
225 |
=> event list" where |
|
226 |
"trace (B,ofr,A,r,I,L,nil) = []" | |
|
13508 | 227 |
"trace (B,ofr,A,r,I,L,cons (Agent D) K) = ( |
228 |
let C = (if K=nil then B else agt_nb (head K)) in |
|
229 |
let I' = (if K=nil then cons (Agent A) (cons (Agent B) I) |
|
230 |
else cons (Agent A) (app (I, cons (head K) nil))) in |
|
231 |
let I'' = app (I, cons (head K) nil) in |
|
232 |
pro C (Suc ofr) A r I' L nil D |
|
233 |
# trace (B,Suc ofr,A,r,I'',tail L,K))" |
|
234 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
23746
diff
changeset
|
235 |
definition trace' :: "agent => nat => nat => msg => agent => nat => event list" where |
13508 | 236 |
"trace' A r n I B ofr == ( |
237 |
let AI = cons (Agent A) I in |
|
238 |
let L = offer_list (A,n,B,AI,ofr) in |
|
239 |
trace (B,ofr,A,r,nil,L,AI))" |
|
240 |
||
241 |
declare trace'_def [simp] |
|
242 |
||
61830 | 243 |
subsubsection\<open>there is a trace in which the originator receives a valid answer\<close> |
13508 | 244 |
|
245 |
lemma p1_not_empty: "evs:p1 ==> req A r n I B:set evs --> |
|
246 |
(EX evs'. evs'@evs:p1 & pro B' ofr A r I' L J A:set evs' & L:valid A n B)" |
|
247 |
oops |
|
248 |
||
249 |
||
61830 | 250 |
subsection\<open>properties of protocol P1\<close> |
13508 | 251 |
|
61830 | 252 |
text\<open>publicly verifiable forward integrity: |
253 |
anyone can verify the validity of an offer list\<close> |
|
13508 | 254 |
|
61830 | 255 |
subsubsection\<open>strong forward integrity: |
256 |
except the last one, no offer can be modified\<close> |
|
13508 | 257 |
|
258 |
lemma strong_forward_integrity: "ALL L. Suc i < len L |
|
259 |
--> L:valid A n B & repl (L,Suc i,M):valid A n B --> M = ith (L,Suc i)" |
|
260 |
apply (induct i) |
|
261 |
(* i = 0 *) |
|
262 |
apply clarify |
|
263 |
apply (frule len_not_empty, clarsimp) |
|
264 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 265 |
apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a) |
266 |
apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a) |
|
13508 | 267 |
apply (simp add: chain_def) |
268 |
(* i > 0 *) |
|
269 |
apply clarify |
|
270 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 271 |
apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na) |
13508 | 272 |
apply (frule len_not_empty, clarsimp) |
23746 | 273 |
apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
13508 | 274 |
by (drule_tac x=l' in spec, simp, blast) |
275 |
||
61830 | 276 |
subsubsection\<open>insertion resilience: |
277 |
except at the beginning, no offer can be inserted\<close> |
|
13508 | 278 |
|
279 |
lemma chain_isnt_head [simp]: "L:valid A n B ==> |
|
280 |
head L ~= chain (next_shop (head L)) ofr A L C" |
|
281 |
by (erule valid.induct, auto simp: chain_def sign_def anchor_def) |
|
282 |
||
283 |
lemma insertion_resilience: "ALL L. L:valid A n B --> Suc i < len L |
|
284 |
--> ins (L,Suc i,M) ~:valid A n B" |
|
285 |
apply (induct i) |
|
286 |
(* i = 0 *) |
|
287 |
apply clarify |
|
288 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 289 |
apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp) |
290 |
apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp) |
|
291 |
apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp) |
|
13508 | 292 |
(* i > 0 *) |
293 |
apply clarify |
|
294 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 295 |
apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
13508 | 296 |
apply (frule len_not_empty, clarsimp) |
23746 | 297 |
apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na) |
13508 | 298 |
apply (frule len_not_empty, clarsimp) |
299 |
by (drule_tac x=l' in spec, clarsimp) |
|
300 |
||
61830 | 301 |
subsubsection\<open>truncation resilience: |
302 |
only shop i can truncate at offer i\<close> |
|
13508 | 303 |
|
304 |
lemma truncation_resilience: "ALL L. L:valid A n B --> Suc i < len L |
|
305 |
--> cons M (trunc (L,Suc i)):valid A n B --> shop M = shop (ith (L,i))" |
|
306 |
apply (induct i) |
|
307 |
(* i = 0 *) |
|
308 |
apply clarify |
|
309 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 310 |
apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
13508 | 311 |
apply (frule len_not_empty, clarsimp) |
23746 | 312 |
apply (ind_cases "{|M,l'|}:valid A n B" for l') |
13508 | 313 |
apply (frule len_not_empty, clarsimp, simp) |
314 |
(* i > 0 *) |
|
315 |
apply clarify |
|
316 |
apply (frule len_not_empty, clarsimp) |
|
23746 | 317 |
apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
13508 | 318 |
apply (frule len_not_empty, clarsimp) |
319 |
by (drule_tac x=l' in spec, clarsimp) |
|
320 |
||
61830 | 321 |
subsubsection\<open>declarations for tactics\<close> |
13508 | 322 |
|
323 |
declare knows_Spy_partsEs [elim] |
|
324 |
declare Fake_parts_insert [THEN subsetD, dest] |
|
325 |
declare initState.simps [simp del] |
|
326 |
||
61830 | 327 |
subsubsection\<open>get components of a message\<close> |
13508 | 328 |
|
329 |
lemma get_ML [dest]: "Says A' B {|A,r,I,M,L|}:set evs ==> |
|
330 |
M:parts (spies evs) & L:parts (spies evs)" |
|
331 |
by blast |
|
332 |
||
61830 | 333 |
subsubsection\<open>general properties of p1\<close> |
13508 | 334 |
|
335 |
lemma reqm_neq_prom [iff]: |
|
336 |
"reqm A r n I B ~= prom B' ofr A' r' I' (cons M L) J C" |
|
337 |
by (auto simp: reqm_def prom_def) |
|
338 |
||
339 |
lemma prom_neq_reqm [iff]: |
|
340 |
"prom B' ofr A' r' I' (cons M L) J C ~= reqm A r n I B" |
|
341 |
by (auto simp: reqm_def prom_def) |
|
342 |
||
343 |
lemma req_neq_pro [iff]: "req A r n I B ~= pro B' ofr A' r' I' (cons M L) J C" |
|
344 |
by (auto simp: req_def pro_def) |
|
345 |
||
346 |
lemma pro_neq_req [iff]: "pro B' ofr A' r' I' (cons M L) J C ~= req A r n I B" |
|
347 |
by (auto simp: req_def pro_def) |
|
348 |
||
349 |
lemma p1_has_no_Gets: "evs:p1 ==> ALL A X. Gets A X ~:set evs" |
|
350 |
by (erule p1.induct, auto simp: req_def pro_def) |
|
351 |
||
352 |
lemma p1_is_Gets_correct [iff]: "Gets_correct p1" |
|
353 |
by (auto simp: Gets_correct_def dest: p1_has_no_Gets) |
|
354 |
||
355 |
lemma p1_is_one_step [iff]: "one_step p1" |
|
23746 | 356 |
by (unfold one_step_def, clarify, ind_cases "ev#evs:p1" for ev evs, auto) |
13508 | 357 |
|
358 |
lemma p1_has_only_Says' [rule_format]: "evs:p1 ==> |
|
359 |
ev:set evs --> (EX A B X. ev=Says A B X)" |
|
360 |
by (erule p1.induct, auto simp: req_def pro_def) |
|
361 |
||
362 |
lemma p1_has_only_Says [iff]: "has_only_Says p1" |
|
363 |
by (auto simp: has_only_Says_def dest: p1_has_only_Says') |
|
364 |
||
365 |
lemma p1_is_regular [iff]: "regular p1" |
|
366 |
apply (simp only: regular_def, clarify) |
|
367 |
apply (erule_tac p1.induct) |
|
368 |
apply (simp_all add: initState.simps knows.simps pro_def prom_def |
|
369 |
req_def reqm_def anchor_def chain_def sign_def) |
|
370 |
by (auto dest: no_Key_in_agl no_Key_in_appdel parts_trans) |
|
371 |
||
61830 | 372 |
subsubsection\<open>private keys are safe\<close> |
13508 | 373 |
|
374 |
lemma priK_parts_Friend_imp_bad [rule_format,dest]: |
|
375 |
"[| evs:p1; Friend B ~= A |] |
|
376 |
==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)" |
|
377 |
apply (erule p1.induct) |
|
378 |
apply (simp_all add: initState.simps knows.simps pro_def prom_def |
|
17778 | 379 |
req_def reqm_def anchor_def chain_def sign_def) |
13508 | 380 |
apply (blast dest: no_Key_in_agl) |
381 |
apply (auto del: parts_invKey disjE dest: parts_trans |
|
382 |
simp add: no_Key_in_appdel) |
|
383 |
done |
|
384 |
||
385 |
lemma priK_analz_Friend_imp_bad [rule_format,dest]: |
|
386 |
"[| evs:p1; Friend B ~= A |] |
|
387 |
==> (Key (priK A):analz (knows (Friend B) evs)) --> (A:bad)" |
|
388 |
by auto |
|
389 |
||
390 |
lemma priK_notin_knows_max_Friend: "[| evs:p1; A ~:bad; A ~= Friend C |] |
|
391 |
==> Key (priK A) ~:analz (knows_max (Friend C) evs)" |
|
392 |
apply (rule not_parts_not_analz, simp add: knows_max_def, safe) |
|
393 |
apply (drule_tac H="spies' evs" in parts_sub) |
|
394 |
apply (rule_tac p=p1 in knows_max'_sub_spies', simp+) |
|
395 |
apply (drule_tac H="spies evs" in parts_sub) |
|
396 |
by (auto dest: knows'_sub_knows [THEN subsetD] priK_notin_initState_Friend) |
|
397 |
||
61830 | 398 |
subsubsection\<open>general guardedness properties\<close> |
13508 | 399 |
|
400 |
lemma agl_guard [intro]: "I:agl ==> I:guard n Ks" |
|
401 |
by (erule agl.induct, auto) |
|
402 |
||
403 |
lemma Says_to_knows_max'_guard: "[| Says A' C {|A'',r,I,L|}:set evs; |
|
404 |
Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks" |
|
405 |
by (auto dest: Says_to_knows_max') |
|
406 |
||
407 |
lemma Says_from_knows_max'_guard: "[| Says C A' {|A'',r,I,L|}:set evs; |
|
408 |
Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks" |
|
409 |
by (auto dest: Says_from_knows_max') |
|
410 |
||
411 |
lemma Says_Nonce_not_used_guard: "[| Says A' B {|A'',r,I,L|}:set evs; |
|
412 |
Nonce n ~:used evs |] ==> L:guard n Ks" |
|
413 |
by (drule not_used_not_parts, auto) |
|
414 |
||
61830 | 415 |
subsubsection\<open>guardedness of messages\<close> |
13508 | 416 |
|
417 |
lemma chain_guard [iff]: "chain B ofr A L C:guard n {priK A}" |
|
418 |
by (case_tac "ofr=n", auto simp: chain_def sign_def) |
|
419 |
||
420 |
lemma chain_guard_Nonce_neq [intro]: "n ~= ofr |
|
421 |
==> chain B ofr A' L C:guard n {priK A}" |
|
422 |
by (auto simp: chain_def sign_def) |
|
423 |
||
424 |
lemma anchor_guard [iff]: "anchor A n' B:guard n {priK A}" |
|
425 |
by (case_tac "n'=n", auto simp: anchor_def) |
|
426 |
||
427 |
lemma anchor_guard_Nonce_neq [intro]: "n ~= n' |
|
428 |
==> anchor A' n' B:guard n {priK A}" |
|
429 |
by (auto simp: anchor_def) |
|
430 |
||
431 |
lemma reqm_guard [intro]: "I:agl ==> reqm A r n' I B:guard n {priK A}" |
|
432 |
by (case_tac "n'=n", auto simp: reqm_def) |
|
433 |
||
434 |
lemma reqm_guard_Nonce_neq [intro]: "[| n ~= n'; I:agl |] |
|
435 |
==> reqm A' r n' I B:guard n {priK A}" |
|
436 |
by (auto simp: reqm_def) |
|
437 |
||
438 |
lemma prom_guard [intro]: "[| I:agl; J:agl; L:guard n {priK A} |] |
|
439 |
==> prom B ofr A r I L J C:guard n {priK A}" |
|
440 |
by (auto simp: prom_def) |
|
441 |
||
442 |
lemma prom_guard_Nonce_neq [intro]: "[| n ~= ofr; I:agl; J:agl; |
|
443 |
L:guard n {priK A} |] ==> prom B ofr A' r I L J C:guard n {priK A}" |
|
444 |
by (auto simp: prom_def) |
|
445 |
||
61830 | 446 |
subsubsection\<open>Nonce uniqueness\<close> |
13508 | 447 |
|
448 |
lemma uniq_Nonce_in_chain [dest]: "Nonce k:parts {chain B ofr A L C} ==> k=ofr" |
|
449 |
by (auto simp: chain_def sign_def) |
|
450 |
||
451 |
lemma uniq_Nonce_in_anchor [dest]: "Nonce k:parts {anchor A n B} ==> k=n" |
|
452 |
by (auto simp: anchor_def chain_def sign_def) |
|
453 |
||
454 |
lemma uniq_Nonce_in_reqm [dest]: "[| Nonce k:parts {reqm A r n I B}; |
|
455 |
I:agl |] ==> k=n" |
|
456 |
by (auto simp: reqm_def dest: no_Nonce_in_agl) |
|
457 |
||
458 |
lemma uniq_Nonce_in_prom [dest]: "[| Nonce k:parts {prom B ofr A r I L J C}; |
|
459 |
I:agl; J:agl; Nonce k ~:parts {L} |] ==> k=ofr" |
|
460 |
by (auto simp: prom_def dest: no_Nonce_in_agl no_Nonce_in_appdel) |
|
461 |
||
61830 | 462 |
subsubsection\<open>requests are guarded\<close> |
13508 | 463 |
|
464 |
lemma req_imp_Guard [rule_format]: "[| evs:p1; A ~:bad |] ==> |
|
465 |
req A r n I B:set evs --> Guard n {priK A} (spies evs)" |
|
466 |
apply (erule p1.induct, simp) |
|
467 |
apply (simp add: req_def knows.simps, safe) |
|
468 |
apply (erule in_synth_Guard, erule Guard_analz, simp) |
|
469 |
by (auto simp: req_def pro_def dest: Says_imp_knows_Spy) |
|
470 |
||
471 |
lemma req_imp_Guard_Friend: "[| evs:p1; A ~:bad; req A r n I B:set evs |] |
|
472 |
==> Guard n {priK A} (knows_max (Friend C) evs)" |
|
473 |
apply (rule Guard_knows_max') |
|
474 |
apply (rule_tac H="spies evs" in Guard_mono) |
|
475 |
apply (rule req_imp_Guard, simp+) |
|
476 |
apply (rule_tac B="spies' evs" in subset_trans) |
|
477 |
apply (rule_tac p=p1 in knows_max'_sub_spies', simp+) |
|
478 |
by (rule knows'_sub_knows) |
|
479 |
||
61830 | 480 |
subsubsection\<open>propositions are guarded\<close> |
13508 | 481 |
|
482 |
lemma pro_imp_Guard [rule_format]: "[| evs:p1; B ~:bad; A ~:bad |] ==> |
|
483 |
pro B ofr A r I (cons M L) J C:set evs --> Guard ofr {priK A} (spies evs)" |
|
484 |
apply (erule p1.induct) (* +3 subgoals *) |
|
485 |
(* Nil *) |
|
486 |
apply simp |
|
487 |
(* Fake *) |
|
488 |
apply (simp add: pro_def, safe) (* +4 subgoals *) |
|
489 |
(* 1 *) |
|
490 |
apply (erule in_synth_Guard, drule Guard_analz, simp, simp) |
|
491 |
(* 2 *) |
|
492 |
apply simp |
|
493 |
(* 3 *) |
|
494 |
apply (simp, simp add: req_def pro_def, blast) |
|
495 |
(* 4 *) |
|
496 |
apply (simp add: pro_def) |
|
497 |
apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard) |
|
498 |
(* 5 *) |
|
499 |
apply simp |
|
500 |
apply safe (* +1 subgoal *) |
|
501 |
apply (simp add: pro_def) |
|
502 |
apply (blast dest: prom_inj Says_Nonce_not_used_guard) |
|
503 |
(* 6 *) |
|
504 |
apply (simp add: pro_def) |
|
505 |
apply (blast dest: Says_imp_knows_Spy) |
|
506 |
(* Request *) |
|
507 |
apply (simp add: pro_def) |
|
508 |
apply (blast dest: prom_inj Says_Nonce_not_used_guard Nonce_not_used_Guard) |
|
509 |
(* Propose *) |
|
510 |
apply simp |
|
511 |
apply safe (* +1 subgoal *) |
|
512 |
(* 1 *) |
|
513 |
apply (simp add: pro_def) |
|
514 |
apply (blast dest: prom_inj Says_Nonce_not_used_guard) |
|
515 |
(* 2 *) |
|
516 |
apply (simp add: pro_def) |
|
517 |
by (blast dest: Says_imp_knows_Spy) |
|
518 |
||
519 |
lemma pro_imp_Guard_Friend: "[| evs:p1; B ~:bad; A ~:bad; |
|
520 |
pro B ofr A r I (cons M L) J C:set evs |] |
|
521 |
==> Guard ofr {priK A} (knows_max (Friend D) evs)" |
|
522 |
apply (rule Guard_knows_max') |
|
523 |
apply (rule_tac H="spies evs" in Guard_mono) |
|
524 |
apply (rule pro_imp_Guard, simp+) |
|
525 |
apply (rule_tac B="spies' evs" in subset_trans) |
|
526 |
apply (rule_tac p=p1 in knows_max'_sub_spies', simp+) |
|
527 |
by (rule knows'_sub_knows) |
|
528 |
||
61830 | 529 |
subsubsection\<open>data confidentiality: |
530 |
no one other than the originator can decrypt the offers\<close> |
|
13508 | 531 |
|
532 |
lemma Nonce_req_notin_spies: "[| evs:p1; req A r n I B:set evs; A ~:bad |] |
|
533 |
==> Nonce n ~:analz (spies evs)" |
|
534 |
by (frule req_imp_Guard, simp+, erule Guard_Nonce_analz, simp+) |
|
535 |
||
536 |
lemma Nonce_req_notin_knows_max_Friend: "[| evs:p1; req A r n I B:set evs; |
|
537 |
A ~:bad; A ~= Friend C |] ==> Nonce n ~:analz (knows_max (Friend C) evs)" |
|
538 |
apply (clarify, frule_tac C=C in req_imp_Guard_Friend, simp+) |
|
539 |
apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+) |
|
540 |
by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def) |
|
541 |
||
542 |
lemma Nonce_pro_notin_spies: "[| evs:p1; B ~:bad; A ~:bad; |
|
543 |
pro B ofr A r I (cons M L) J C:set evs |] ==> Nonce ofr ~:analz (spies evs)" |
|
544 |
by (frule pro_imp_Guard, simp+, erule Guard_Nonce_analz, simp+) |
|
545 |
||
546 |
lemma Nonce_pro_notin_knows_max_Friend: "[| evs:p1; B ~:bad; A ~:bad; |
|
547 |
A ~= Friend D; pro B ofr A r I (cons M L) J C:set evs |] |
|
548 |
==> Nonce ofr ~:analz (knows_max (Friend D) evs)" |
|
549 |
apply (clarify, frule_tac A=A in pro_imp_Guard_Friend, simp+) |
|
550 |
apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+) |
|
551 |
by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def) |
|
552 |
||
61830 | 553 |
subsubsection\<open>non repudiability: |
554 |
an offer signed by B has been sent by B\<close> |
|
13508 | 555 |
|
556 |
lemma Crypt_reqm: "[| Crypt (priK A) X:parts {reqm A' r n I B}; I:agl |] ==> A=A'" |
|
557 |
by (auto simp: reqm_def anchor_def chain_def sign_def dest: no_Crypt_in_agl) |
|
558 |
||
559 |
lemma Crypt_prom: "[| Crypt (priK A) X:parts {prom B ofr A' r I L J C}; |
|
560 |
I:agl; J:agl |] ==> A=B | Crypt (priK A) X:parts {L}" |
|
561 |
apply (simp add: prom_def anchor_def chain_def sign_def) |
|
562 |
by (blast dest: no_Crypt_in_agl no_Crypt_in_appdel) |
|
563 |
||
564 |
lemma Crypt_safeness: "[| evs:p1; A ~:bad |] ==> Crypt (priK A) X:parts (spies evs) |
|
565 |
--> (EX B Y. Says A B Y:set evs & Crypt (priK A) X:parts {Y})" |
|
566 |
apply (erule p1.induct) |
|
567 |
(* Nil *) |
|
568 |
apply simp |
|
569 |
(* Fake *) |
|
570 |
apply clarsimp |
|
571 |
apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) |
|
572 |
apply (erule disjE) |
|
573 |
apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast) |
|
574 |
(* Request *) |
|
575 |
apply (simp add: req_def, clarify) |
|
576 |
apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) |
|
577 |
apply (erule disjE) |
|
578 |
apply (frule Crypt_reqm, simp, clarify) |
|
579 |
apply (rule_tac x=B in exI, rule_tac x="reqm A r n I B" in exI, simp, blast) |
|
580 |
(* Propose *) |
|
581 |
apply (simp add: pro_def, clarify) |
|
582 |
apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp) |
|
583 |
apply (rotate_tac -1, erule disjE) |
|
584 |
apply (frule Crypt_prom, simp, simp) |
|
585 |
apply (rotate_tac -1, erule disjE) |
|
586 |
apply (rule_tac x=C in exI) |
|
587 |
apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI, blast) |
|
588 |
apply (subgoal_tac "cons M L:parts (spies evsp)") |
|
589 |
apply (drule_tac G="{cons M L}" and H="spies evsp" in parts_trans, blast, blast) |
|
590 |
apply (drule Says_imp_spies, rotate_tac -1, drule parts.Inj) |
|
591 |
apply (drule parts.Snd, drule parts.Snd, drule parts.Snd) |
|
592 |
by auto |
|
593 |
||
594 |
lemma Crypt_Hash_imp_sign: "[| evs:p1; A ~:bad |] ==> |
|
595 |
Crypt (priK A) (Hash X):parts (spies evs) |
|
596 |
--> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})" |
|
597 |
apply (erule p1.induct) |
|
598 |
(* Nil *) |
|
599 |
apply simp |
|
600 |
(* Fake *) |
|
601 |
apply clarsimp |
|
602 |
apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) |
|
603 |
apply simp |
|
604 |
apply (erule disjE) |
|
605 |
apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast) |
|
606 |
(* Request *) |
|
607 |
apply (simp add: req_def, clarify) |
|
608 |
apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) |
|
609 |
apply simp |
|
610 |
apply (erule disjE) |
|
611 |
apply (frule Crypt_reqm, simp+) |
|
612 |
apply (rule_tac x=B in exI, rule_tac x="reqm Aa r n I B" in exI) |
|
613 |
apply (simp add: reqm_def sign_def anchor_def no_Crypt_in_agl) |
|
614 |
apply (simp add: chain_def sign_def, blast) |
|
615 |
(* Propose *) |
|
616 |
apply (simp add: pro_def, clarify) |
|
617 |
apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD) |
|
618 |
apply simp |
|
619 |
apply (rotate_tac -1, erule disjE) |
|
620 |
apply (simp add: prom_def sign_def no_Crypt_in_agl no_Crypt_in_appdel) |
|
621 |
apply (simp add: chain_def sign_def) |
|
622 |
apply (rotate_tac -1, erule disjE) |
|
623 |
apply (rule_tac x=C in exI) |
|
624 |
apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI) |
|
625 |
apply (simp add: prom_def chain_def sign_def) |
|
626 |
apply (erule impE) |
|
627 |
apply (blast dest: get_ML parts_sub) |
|
628 |
apply (blast del: MPair_parts)+ |
|
629 |
done |
|
630 |
||
631 |
lemma sign_safeness: "[| evs:p1; A ~:bad |] ==> sign A X:parts (spies evs) |
|
632 |
--> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})" |
|
633 |
apply (clarify, simp add: sign_def, frule parts.Snd) |
|
634 |
apply (blast dest: Crypt_Hash_imp_sign [unfolded sign_def]) |
|
635 |
done |
|
636 |
||
637 |
end |