author | wenzelm |
Thu, 15 Feb 2018 12:11:00 +0100 | |
changeset 67613 | ce654b0e6d69 |
parent 62390 | 842917225d56 |
child 71989 | bad75618fb82 |
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 |
||
61956 | 21 |
we will adopt the following format for messages: \<lbrace>A,r,I,L\<rbrace> |
13508 | 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 |
|
61956 | 39 |
let m2= Hash \<lbrace>head L, Agent C\<rbrace> in |
40 |
sign B \<lbrace>m1,m2\<rbrace>" |
|
13508 | 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 |
||
67613 | 48 |
lemma Nonce_in_chain [iff]: "Nonce ofr \<in> parts {chain B ofr A L C}" |
13508 | 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 |
61956 | 54 |
"shop \<lbrace>B,X,Crypt K H\<rbrace> = Agent (agt K)" |
13508 | 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 |
61956 | 62 |
"nonce \<lbrace>B,\<lbrace>Crypt K ofr,m2\<rbrace>,CryptH\<rbrace> = ofr" |
13508 | 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 |
61956 | 70 |
"next_shop \<lbrace>B,\<lbrace>m1,Hash\<lbrace>headL,Agent C\<rbrace>\<rbrace>,CryptH\<rbrace> = C" |
13508 | 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 |
||
67613 | 84 |
lemma Nonce_in_anchor [iff]: "Nonce n \<in> parts {anchor A n B}" |
13508 | 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 |
61956 | 99 |
"reqm A r n I B == \<lbrace>Agent A, Number r, cons (Agent A) (cons (Agent B) I), |
100 |
cons (anchor A n B) nil\<rbrace>" |
|
13508 | 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 |
||
67613 | 106 |
lemma Nonce_in_reqm [iff]: "Nonce n \<in> parts {reqm A r n I B}" |
13508 | 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 |
61956 | 120 |
"prom B ofr A r I L J C == \<lbrace>Agent A, Number r, |
121 |
app (J, del (Agent B, I)), cons (chain B ofr A L C) L\<rbrace>" |
|
13508 | 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 |
||
67613 | 128 |
lemma Nonce_in_prom [iff]: "Nonce ofr \<in> parts {prom B ofr A r I L J C}" |
13508 | 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 |
|
67613 | 144 |
Nil: "[] \<in> p1" |
13508 | 145 |
|
67613 | 146 |
| Fake: "[| evsf \<in> p1; X \<in> synth (analz (spies evsf)) |] ==> Says Spy B X # evsf \<in> p1" |
13508 | 147 |
|
67613 | 148 |
| Request: "[| evsr \<in> p1; Nonce n \<notin> used evsr; I \<in> agl |] ==> req A r n I B # evsr \<in> p1" |
13508 | 149 |
|
67613 | 150 |
| Propose: "[| evsp \<in> p1; Says A' B \<lbrace>Agent A,Number r,I,cons M L\<rbrace> \<in> set evsp; |
151 |
I \<in> agl; J \<in> agl; isin (Agent C, app (J, del (Agent B, I))); |
|
152 |
Nonce ofr \<notin> used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp \<in> p1" |
|
13508 | 153 |
|
61830 | 154 |
subsubsection\<open>Composition of Traces\<close> |
13508 | 155 |
|
67613 | 156 |
lemma "evs' \<in> p1 \<Longrightarrow> |
157 |
evs \<in> p1 \<and> (\<forall>n. Nonce n \<in> used evs' \<longrightarrow> Nonce n \<notin> used evs) \<longrightarrow> |
|
158 |
evs' @ evs \<in> p1" |
|
13508 | 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 |
67613 | 171 |
valid :: "agent \<Rightarrow> nat \<Rightarrow> agent \<Rightarrow> msg set" |
23746 | 172 |
for A :: agent and n :: nat and B :: agent |
173 |
where |
|
67613 | 174 |
Request [intro]: "cons (anchor A n B) nil \<in> valid A n B" |
13508 | 175 |
|
67613 | 176 |
| Propose [intro]: "L \<in> valid A n B |
177 |
\<Longrightarrow> cons (chain (next_shop (head L)) ofr A L C) L \<in> valid A n B" |
|
13508 | 178 |
|
61830 | 179 |
subsubsection\<open>basic properties of valid\<close> |
13508 | 180 |
|
67613 | 181 |
lemma valid_not_empty: "L \<in> valid A n B \<Longrightarrow> \<exists>M L'. L = cons M L'" |
13508 | 182 |
by (erule valid.cases, auto) |
183 |
||
67613 | 184 |
lemma valid_pos_len: "L \<in> valid A n B \<Longrightarrow> 0 < len L" |
13508 | 185 |
by (erule valid.induct, auto) |
186 |
||
61830 | 187 |
subsubsection\<open>offers of an offer list\<close> |
13508 | 188 |
|
67613 | 189 |
definition offer_nonces :: "msg \<Rightarrow> msg set" where |
190 |
"offer_nonces L \<equiv> {X. X \<in> parts {L} \<and> (\<exists>n. X = Nonce n)}" |
|
13508 | 191 |
|
61830 | 192 |
subsubsection\<open>the originator can get the offers\<close> |
13508 | 193 |
|
67613 | 194 |
lemma "L \<in> valid A n B \<Longrightarrow> offer_nonces L \<subseteq> analz (insert L (initState A))" |
13508 | 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 |
61956 | 201 |
"offers (cons M L) = cons \<lbrace>shop M, nonce M\<rbrace> (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 |
||
67613 | 210 |
lemma shops_in_agl: "L \<in> valid A n B \<Longrightarrow> shops L \<in> agl" |
13508 | 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 |
|
67613 | 215 |
fun offer_list :: "agent \<times> nat \<times> agent \<times> msg \<times> nat \<Rightarrow> msg" where |
35418 | 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 |
||
67613 | 221 |
lemma "I \<in> agl \<Longrightarrow> \<forall>ofr. offer_list (A,n,B,I,ofr) \<in> valid A n B" |
13508 | 222 |
by (erule agl.induct, auto) |
223 |
||
67613 | 224 |
fun trace :: "agent \<times> nat \<times> agent \<times> nat \<times> msg \<times> msg \<times> msg |
225 |
\<Rightarrow> event list" where |
|
35418 | 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 |
||
67613 | 235 |
definition trace' :: "agent \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> msg \<Rightarrow> agent \<Rightarrow> nat \<Rightarrow> event list" where |
236 |
"trace' A r n I B ofr \<equiv> ( |
|
13508 | 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 |
|
67613 | 245 |
lemma p1_not_empty: "evs \<in> p1 \<Longrightarrow> req A r n I B \<in> set evs \<longrightarrow> |
246 |
(\<exists>evs'. evs' @ evs \<in> p1 \<and> pro B' ofr A r I' L J A \<in> set evs' \<and> L \<in> valid A n B)" |
|
13508 | 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 |
|
67613 | 258 |
lemma strong_forward_integrity: "\<forall>L. Suc i < len L |
259 |
\<longrightarrow> L \<in> valid A n B \<and> repl (L,Suc i,M) \<in> valid A n B \<longrightarrow> M = ith (L,Suc i)" |
|
13508 | 260 |
apply (induct i) |
261 |
(* i = 0 *) |
|
262 |
apply clarify |
|
263 |
apply (frule len_not_empty, clarsimp) |
|
264 |
apply (frule len_not_empty, clarsimp) |
|
67613 | 265 |
apply (ind_cases "\<lbrace>x,xa,l'a\<rbrace> \<in> valid A n B" for x xa l'a) |
266 |
apply (ind_cases "\<lbrace>x,M,l'a\<rbrace> \<in> 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) |
|
67613 | 271 |
apply (ind_cases "\<lbrace>x,repl(l',Suc na,M)\<rbrace> \<in> valid A n B" for x l' na) |
13508 | 272 |
apply (frule len_not_empty, clarsimp) |
67613 | 273 |
apply (ind_cases "\<lbrace>x,l'\<rbrace> \<in> 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 |
|
67613 | 279 |
lemma chain_isnt_head [simp]: "L \<in> valid A n B \<Longrightarrow> |
280 |
head L \<noteq> chain (next_shop (head L)) ofr A L C" |
|
13508 | 281 |
by (erule valid.induct, auto simp: chain_def sign_def anchor_def) |
282 |
||
67613 | 283 |
lemma insertion_resilience: "\<forall>L. L \<in> valid A n B \<longrightarrow> Suc i < len L |
284 |
\<longrightarrow> ins (L,Suc i,M) \<notin> valid A n B" |
|
13508 | 285 |
apply (induct i) |
286 |
(* i = 0 *) |
|
287 |
apply clarify |
|
288 |
apply (frule len_not_empty, clarsimp) |
|
67613 | 289 |
apply (ind_cases "\<lbrace>x,l'\<rbrace> \<in> valid A n B" for x l', simp) |
290 |
apply (ind_cases "\<lbrace>x,M,l'\<rbrace> \<in> valid A n B" for x l', clarsimp) |
|
291 |
apply (ind_cases "\<lbrace>head l',l'\<rbrace> \<in> valid A n B" for l', simp, simp) |
|
13508 | 292 |
(* i > 0 *) |
293 |
apply clarify |
|
294 |
apply (frule len_not_empty, clarsimp) |
|
67613 | 295 |
apply (ind_cases "\<lbrace>x,l'\<rbrace> \<in> valid A n B" for x l') |
13508 | 296 |
apply (frule len_not_empty, clarsimp) |
67613 | 297 |
apply (ind_cases "\<lbrace>x,ins(l',Suc na,M)\<rbrace> \<in> 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 |
|
67613 | 304 |
lemma truncation_resilience: "\<forall>L. L \<in> valid A n B \<longrightarrow> Suc i < len L |
305 |
\<longrightarrow> cons M (trunc (L,Suc i)) \<in> valid A n B \<longrightarrow> shop M = shop (ith (L,i))" |
|
13508 | 306 |
apply (induct i) |
307 |
(* i = 0 *) |
|
308 |
apply clarify |
|
309 |
apply (frule len_not_empty, clarsimp) |
|
67613 | 310 |
apply (ind_cases "\<lbrace>x,l'\<rbrace> \<in> valid A n B" for x l') |
13508 | 311 |
apply (frule len_not_empty, clarsimp) |
67613 | 312 |
apply (ind_cases "\<lbrace>M,l'\<rbrace> \<in> 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) |
|
67613 | 317 |
apply (ind_cases "\<lbrace>x,l'\<rbrace> \<in> 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 |
|
67613 | 329 |
lemma get_ML [dest]: "Says A' B \<lbrace>A,r,I,M,L\<rbrace> \<in> set evs \<Longrightarrow> |
330 |
M \<in> parts (spies evs) \<and> L \<in> parts (spies evs)" |
|
13508 | 331 |
by blast |
332 |
||
61830 | 333 |
subsubsection\<open>general properties of p1\<close> |
13508 | 334 |
|
335 |
lemma reqm_neq_prom [iff]: |
|
67613 | 336 |
"reqm A r n I B \<noteq> prom B' ofr A' r' I' (cons M L) J C" |
13508 | 337 |
by (auto simp: reqm_def prom_def) |
338 |
||
339 |
lemma prom_neq_reqm [iff]: |
|
67613 | 340 |
"prom B' ofr A' r' I' (cons M L) J C \<noteq> reqm A r n I B" |
13508 | 341 |
by (auto simp: reqm_def prom_def) |
342 |
||
67613 | 343 |
lemma req_neq_pro [iff]: "req A r n I B \<noteq> pro B' ofr A' r' I' (cons M L) J C" |
13508 | 344 |
by (auto simp: req_def pro_def) |
345 |
||
67613 | 346 |
lemma pro_neq_req [iff]: "pro B' ofr A' r' I' (cons M L) J C \<noteq> req A r n I B" |
13508 | 347 |
by (auto simp: req_def pro_def) |
348 |
||
67613 | 349 |
lemma p1_has_no_Gets: "evs \<in> p1 \<Longrightarrow> \<forall>A X. Gets A X \<notin> set evs" |
13508 | 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" |
|
67613 | 356 |
by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> p1" for ev evs, auto) |
13508 | 357 |
|
67613 | 358 |
lemma p1_has_only_Says' [rule_format]: "evs \<in> p1 \<Longrightarrow> |
359 |
ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)" |
|
13508 | 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]: |
|
67613 | 375 |
"[| evs \<in> p1; Friend B \<noteq> A |] |
376 |
==> (Key (priK A) \<in> parts (knows (Friend B) evs)) \<longrightarrow> (A \<in> bad)" |
|
13508 | 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]: |
|
67613 | 386 |
"[| evs \<in> p1; Friend B \<noteq> A |] |
387 |
==> (Key (priK A) \<in> analz (knows (Friend B) evs)) \<longrightarrow> (A \<in> bad)" |
|
13508 | 388 |
by auto |
389 |
||
67613 | 390 |
lemma priK_notin_knows_max_Friend: "[| evs \<in> p1; A \<notin> bad; A \<noteq> Friend C |] |
391 |
==> Key (priK A) \<notin> analz (knows_max (Friend C) evs)" |
|
13508 | 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 |
|
67613 | 400 |
lemma agl_guard [intro]: "I \<in> agl \<Longrightarrow> I \<in> guard n Ks" |
13508 | 401 |
by (erule agl.induct, auto) |
402 |
||
67613 | 403 |
lemma Says_to_knows_max'_guard: "[| Says A' C \<lbrace>A'',r,I,L\<rbrace> \<in> set evs; |
404 |
Guard n Ks (knows_max' C evs) |] ==> L \<in> guard n Ks" |
|
13508 | 405 |
by (auto dest: Says_to_knows_max') |
406 |
||
67613 | 407 |
lemma Says_from_knows_max'_guard: "[| Says C A' \<lbrace>A'',r,I,L\<rbrace> \<in> set evs; |
408 |
Guard n Ks (knows_max' C evs) |] ==> L \<in> guard n Ks" |
|
13508 | 409 |
by (auto dest: Says_from_knows_max') |
410 |
||
67613 | 411 |
lemma Says_Nonce_not_used_guard: "[| Says A' B \<lbrace>A'',r,I,L\<rbrace> \<in> set evs; |
412 |
Nonce n \<notin> used evs |] ==> L \<in> guard n Ks" |
|
13508 | 413 |
by (drule not_used_not_parts, auto) |
414 |
||
61830 | 415 |
subsubsection\<open>guardedness of messages\<close> |
13508 | 416 |
|
67613 | 417 |
lemma chain_guard [iff]: "chain B ofr A L C \<in> guard n {priK A}" |
13508 | 418 |
by (case_tac "ofr=n", auto simp: chain_def sign_def) |
419 |
||
67613 | 420 |
lemma chain_guard_Nonce_neq [intro]: "n \<noteq> ofr |
421 |
\<Longrightarrow> chain B ofr A' L C \<in> guard n {priK A}" |
|
13508 | 422 |
by (auto simp: chain_def sign_def) |
423 |
||
67613 | 424 |
lemma anchor_guard [iff]: "anchor A n' B \<in> guard n {priK A}" |
13508 | 425 |
by (case_tac "n'=n", auto simp: anchor_def) |
426 |
||
67613 | 427 |
lemma anchor_guard_Nonce_neq [intro]: "n \<noteq> n' |
428 |
\<Longrightarrow> anchor A' n' B \<in> guard n {priK A}" |
|
13508 | 429 |
by (auto simp: anchor_def) |
430 |
||
67613 | 431 |
lemma reqm_guard [intro]: "I \<in> agl \<Longrightarrow> reqm A r n' I B \<in> guard n {priK A}" |
13508 | 432 |
by (case_tac "n'=n", auto simp: reqm_def) |
433 |
||
67613 | 434 |
lemma reqm_guard_Nonce_neq [intro]: "[| n \<noteq> n'; I \<in> agl |] |
435 |
==> reqm A' r n' I B \<in> guard n {priK A}" |
|
13508 | 436 |
by (auto simp: reqm_def) |
437 |
||
67613 | 438 |
lemma prom_guard [intro]: "[| I \<in> agl; J \<in> agl; L \<in> guard n {priK A} |] |
439 |
==> prom B ofr A r I L J C \<in> guard n {priK A}" |
|
13508 | 440 |
by (auto simp: prom_def) |
441 |
||
67613 | 442 |
lemma prom_guard_Nonce_neq [intro]: "[| n \<noteq> ofr; I \<in> agl; J \<in> agl; |
443 |
L \<in> guard n {priK A} |] ==> prom B ofr A' r I L J C \<in> guard n {priK A}" |
|
13508 | 444 |
by (auto simp: prom_def) |
445 |
||
61830 | 446 |
subsubsection\<open>Nonce uniqueness\<close> |
13508 | 447 |
|
67613 | 448 |
lemma uniq_Nonce_in_chain [dest]: "Nonce k \<in> parts {chain B ofr A L C} \<Longrightarrow> k=ofr" |
13508 | 449 |
by (auto simp: chain_def sign_def) |
450 |
||
67613 | 451 |
lemma uniq_Nonce_in_anchor [dest]: "Nonce k \<in> parts {anchor A n B} \<Longrightarrow> k=n" |
13508 | 452 |
by (auto simp: anchor_def chain_def sign_def) |
453 |
||
67613 | 454 |
lemma uniq_Nonce_in_reqm [dest]: "[| Nonce k \<in> parts {reqm A r n I B}; |
455 |
I \<in> agl |] ==> k=n" |
|
13508 | 456 |
by (auto simp: reqm_def dest: no_Nonce_in_agl) |
457 |
||
67613 | 458 |
lemma uniq_Nonce_in_prom [dest]: "[| Nonce k \<in> parts {prom B ofr A r I L J C}; |
459 |
I \<in> agl; J \<in> agl; Nonce k \<notin> parts {L} |] ==> k=ofr" |
|
13508 | 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 |
|
67613 | 464 |
lemma req_imp_Guard [rule_format]: "[| evs \<in> p1; A \<notin> bad |] ==> |
465 |
req A r n I B \<in> set evs \<longrightarrow> Guard n {priK A} (spies evs)" |
|
13508 | 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 |
||
67613 | 471 |
lemma req_imp_Guard_Friend: "[| evs \<in> p1; A \<notin> bad; req A r n I B \<in> set evs |] |
13508 | 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 |
|
67613 | 482 |
lemma pro_imp_Guard [rule_format]: "[| evs \<in> p1; B \<notin> bad; A \<notin> bad |] ==> |
483 |
pro B ofr A r I (cons M L) J C \<in> set evs \<longrightarrow> Guard ofr {priK A} (spies evs)" |
|
13508 | 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 |
||
67613 | 519 |
lemma pro_imp_Guard_Friend: "[| evs \<in> p1; B \<notin> bad; A \<notin> bad; |
520 |
pro B ofr A r I (cons M L) J C \<in> set evs |] |
|
13508 | 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 |
|
67613 | 532 |
lemma Nonce_req_notin_spies: "[| evs \<in> p1; req A r n I B \<in> set evs; A \<notin> bad |] |
533 |
==> Nonce n \<notin> analz (spies evs)" |
|
13508 | 534 |
by (frule req_imp_Guard, simp+, erule Guard_Nonce_analz, simp+) |
535 |
||
67613 | 536 |
lemma Nonce_req_notin_knows_max_Friend: "[| evs \<in> p1; req A r n I B \<in> set evs; |
537 |
A \<notin> bad; A \<noteq> Friend C |] ==> Nonce n \<notin> analz (knows_max (Friend C) evs)" |
|
13508 | 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 |
||
67613 | 542 |
lemma Nonce_pro_notin_spies: "[| evs \<in> p1; B \<notin> bad; A \<notin> bad; |
543 |
pro B ofr A r I (cons M L) J C \<in> set evs |] ==> Nonce ofr \<notin> analz (spies evs)" |
|
13508 | 544 |
by (frule pro_imp_Guard, simp+, erule Guard_Nonce_analz, simp+) |
545 |
||
67613 | 546 |
lemma Nonce_pro_notin_knows_max_Friend: "[| evs \<in> p1; B \<notin> bad; A \<notin> bad; |
547 |
A \<noteq> Friend D; pro B ofr A r I (cons M L) J C \<in> set evs |] |
|
548 |
==> Nonce ofr \<notin> analz (knows_max (Friend D) evs)" |
|
13508 | 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 |
|
67613 | 556 |
lemma Crypt_reqm: "[| Crypt (priK A) X \<in> parts {reqm A' r n I B}; I \<in> agl |] ==> A=A'" |
13508 | 557 |
by (auto simp: reqm_def anchor_def chain_def sign_def dest: no_Crypt_in_agl) |
558 |
||
67613 | 559 |
lemma Crypt_prom: "[| Crypt (priK A) X \<in> parts {prom B ofr A' r I L J C}; |
560 |
I \<in> agl; J \<in> agl |] ==> A=B \<or> Crypt (priK A) X \<in> parts {L}" |
|
13508 | 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 |
||
67613 | 564 |
lemma Crypt_safeness: "[| evs \<in> p1; A \<notin> bad |] ==> Crypt (priK A) X \<in> parts (spies evs) |
565 |
\<longrightarrow> (\<exists>B Y. Says A B Y \<in> set evs \<and> Crypt (priK A) X \<in> parts {Y})" |
|
13508 | 566 |
apply (erule p1.induct) |
567 |
(* Nil *) |
|
568 |
apply simp |
|
569 |
(* Fake *) |
|
570 |
apply clarsimp |
|
67613 | 571 |
apply (drule_tac P="\<lambda>G. Crypt (priK A) X \<in> G" in parts_insert_substD, simp) |
13508 | 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) |
|
67613 | 576 |
apply (drule_tac P="\<lambda>G. Crypt (priK A) X \<in> G" in parts_insert_substD, simp) |
13508 | 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) |
|
67613 | 582 |
apply (drule_tac P="\<lambda>G. Crypt (priK A) X \<in> G" in parts_insert_substD, simp) |
13508 | 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) |
|
67613 | 588 |
apply (subgoal_tac "cons M L \<in> parts (spies evsp)") |
13508 | 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 |
||
67613 | 594 |
lemma Crypt_Hash_imp_sign: "[| evs \<in> p1; A \<notin> bad |] ==> |
595 |
Crypt (priK A) (Hash X) \<in> parts (spies evs) |
|
596 |
\<longrightarrow> (\<exists>B Y. Says A B Y \<in> set evs \<and> sign A X \<in> parts {Y})" |
|
13508 | 597 |
apply (erule p1.induct) |
598 |
(* Nil *) |
|
599 |
apply simp |
|
600 |
(* Fake *) |
|
601 |
apply clarsimp |
|
67613 | 602 |
apply (drule_tac P="\<lambda>G. Crypt (priK A) (Hash X) \<in> G" in parts_insert_substD) |
13508 | 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) |
|
67613 | 608 |
apply (drule_tac P="\<lambda>G. Crypt (priK A) (Hash X) \<in> G" in parts_insert_substD) |
13508 | 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) |
|
67613 | 617 |
apply (drule_tac P="\<lambda>G. Crypt (priK A) (Hash X) \<in> G" in parts_insert_substD) |
13508 | 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 |
||
67613 | 631 |
lemma sign_safeness: "[| evs \<in> p1; A \<notin> bad |] ==> sign A X \<in> parts (spies evs) |
632 |
\<longrightarrow> (\<exists>B Y. Says A B Y \<in> set evs \<and> sign A X \<in> parts {Y})" |
|
13508 | 633 |
apply (clarify, simp add: sign_def, frule parts.Snd) |
634 |
apply (blast dest: Crypt_Hash_imp_sign [unfolded sign_def]) |
|
635 |
done |
|
636 |
||
62390 | 637 |
end |