author | paulson <lp15@cam.ac.uk> |
Wed, 26 Apr 2017 15:53:35 +0100 | |
changeset 65583 | 8d53b3bebab4 |
parent 63648 | f9f3006a5579 |
child 67443 | 3abf6a722518 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/Auth/Shared.thy |
1934 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1996 University of Cambridge |
|
4 |
||
5 |
Theory of Shared Keys (common to all symmetric-key protocols) |
|
6 |
||
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3472
diff
changeset
|
7 |
Shared, long-term keys; initial states of agents |
1934 | 8 |
*) |
9 |
||
32631 | 10 |
theory Shared |
11 |
imports Event All_Symmetric |
|
12 |
begin |
|
1934 | 13 |
|
14 |
consts |
|
39216 | 15 |
shrK :: "agent => key" (*symmetric keys*) |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
16 |
|
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
17 |
specification (shrK) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
18 |
inj_shrK: "inj shrK" |
61830 | 19 |
\<comment>\<open>No two agents have the same long-term key\<close> |
55416 | 20 |
apply (rule exI [of _ "case_agent 0 (\<lambda>n. n + 2) 1"]) |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
21 |
apply (simp add: inj_on_def split: agent.split) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
22 |
done |
1967 | 23 |
|
61830 | 24 |
text\<open>Server knows all long-term keys; other agents know only their own\<close> |
39246 | 25 |
|
26 |
overloading |
|
27 |
initState \<equiv> initState |
|
28 |
begin |
|
29 |
||
30 |
primrec initState where |
|
11104 | 31 |
initState_Server: "initState Server = Key ` range shrK" |
39246 | 32 |
| initState_Friend: "initState (Friend i) = {Key (shrK (Friend i))}" |
33 |
| initState_Spy: "initState Spy = Key`shrK`bad" |
|
34 |
||
35 |
end |
|
2032 | 36 |
|
1934 | 37 |
|
61830 | 38 |
subsection\<open>Basic properties of shrK\<close> |
13926 | 39 |
|
40 |
(*Injectiveness: Agents' long-term keys are distinct.*) |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
17744
diff
changeset
|
41 |
lemmas shrK_injective = inj_shrK [THEN inj_eq] |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
17744
diff
changeset
|
42 |
declare shrK_injective [iff] |
13926 | 43 |
|
44 |
lemma invKey_K [simp]: "invKey K = K" |
|
45 |
apply (insert isSym_keys) |
|
46 |
apply (simp add: symKeys_def) |
|
47 |
done |
|
48 |
||
49 |
||
50 |
lemma analz_Decrypt' [dest]: |
|
51 |
"[| Crypt K X \<in> analz H; Key K \<in> analz H |] ==> X \<in> analz H" |
|
52 |
by auto |
|
53 |
||
61830 | 54 |
text\<open>Now cancel the \<open>dest\<close> attribute given to |
55 |
\<open>analz.Decrypt\<close> in its declaration.\<close> |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
56 |
declare analz.Decrypt [rule del] |
13926 | 57 |
|
61830 | 58 |
text\<open>Rewrites should not refer to @{term "initState(Friend i)"} because |
59 |
that expression is not in normal form.\<close> |
|
13926 | 60 |
|
61 |
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" |
|
62 |
apply (unfold keysFor_def) |
|
63 |
apply (induct_tac "C", auto) |
|
64 |
done |
|
65 |
||
66 |
(*Specialized to shared-key model: no @{term invKey}*) |
|
67 |
lemma keysFor_parts_insert: |
|
14983 | 68 |
"[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |] |
39216 | 69 |
==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H" |
41693
47532fe9e075
Introduction of metis calls and other cosmetic modifications.
paulson
parents:
39247
diff
changeset
|
70 |
by (metis invKey_K keysFor_parts_insert) |
13926 | 71 |
|
72 |
lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H" |
|
41693
47532fe9e075
Introduction of metis calls and other cosmetic modifications.
paulson
parents:
39247
diff
changeset
|
73 |
by (metis Crypt_imp_invKey_keysFor invKey_K) |
13926 | 74 |
|
75 |
||
61830 | 76 |
subsection\<open>Function "knows"\<close> |
13926 | 77 |
|
78 |
(*Spy sees shared keys of agents!*) |
|
79 |
lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) \<in> knows Spy evs" |
|
80 |
apply (induct_tac "evs") |
|
63648 | 81 |
apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split) |
13926 | 82 |
done |
83 |
||
84 |
(*For case analysis on whether or not an agent is compromised*) |
|
85 |
lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X \<in> analz (knows Spy evs); A: bad |] |
|
86 |
==> X \<in> analz (knows Spy evs)" |
|
41693
47532fe9e075
Introduction of metis calls and other cosmetic modifications.
paulson
parents:
39247
diff
changeset
|
87 |
by (metis Spy_knows_Spy_bad analz.Inj analz_Decrypt') |
13926 | 88 |
|
89 |
||
90 |
(** Fresh keys never clash with long-term shared keys **) |
|
91 |
||
92 |
(*Agents see their own shared keys!*) |
|
93 |
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A" |
|
94 |
by (induct_tac "A", auto) |
|
95 |
||
96 |
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs" |
|
97 |
by (rule initState_into_used, blast) |
|
98 |
||
99 |
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys |
|
100 |
from long-term shared keys*) |
|
101 |
lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK" |
|
102 |
by blast |
|
103 |
||
104 |
lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K" |
|
105 |
by blast |
|
106 |
||
17744 | 107 |
lemmas shrK_sym_neq = shrK_neq [THEN not_sym] |
108 |
declare shrK_sym_neq [simp] |
|
13926 | 109 |
|
110 |
||
61830 | 111 |
subsection\<open>Fresh nonces\<close> |
13926 | 112 |
|
113 |
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)" |
|
114 |
by (induct_tac "B", auto) |
|
115 |
||
116 |
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []" |
|
41693
47532fe9e075
Introduction of metis calls and other cosmetic modifications.
paulson
parents:
39247
diff
changeset
|
117 |
by (simp add: used_Nil) |
13926 | 118 |
|
119 |
||
61830 | 120 |
subsection\<open>Supply fresh nonces for possibility theorems.\<close> |
13926 | 121 |
|
122 |
(*In any trace, there is an upper bound N on the greatest nonce in use.*) |
|
123 |
lemma Nonce_supply_lemma: "\<exists>N. ALL n. N<=n --> Nonce n \<notin> used evs" |
|
124 |
apply (induct_tac "evs") |
|
125 |
apply (rule_tac x = 0 in exI) |
|
63648 | 126 |
apply (simp_all (no_asm_simp) add: used_Cons split: event.split) |
41693
47532fe9e075
Introduction of metis calls and other cosmetic modifications.
paulson
parents:
39247
diff
changeset
|
127 |
apply (metis le_sup_iff msg_Nonce_supply) |
13926 | 128 |
done |
129 |
||
130 |
lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs" |
|
41693
47532fe9e075
Introduction of metis calls and other cosmetic modifications.
paulson
parents:
39247
diff
changeset
|
131 |
by (metis Nonce_supply_lemma order_eq_iff) |
13926 | 132 |
|
133 |
lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'" |
|
134 |
apply (cut_tac evs = evs in Nonce_supply_lemma) |
|
135 |
apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify) |
|
41693
47532fe9e075
Introduction of metis calls and other cosmetic modifications.
paulson
parents:
39247
diff
changeset
|
136 |
apply (metis Suc_n_not_le_n nat_le_linear) |
13926 | 137 |
done |
138 |
||
139 |
lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & |
|
140 |
Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''" |
|
141 |
apply (cut_tac evs = evs in Nonce_supply_lemma) |
|
142 |
apply (cut_tac evs = "evs'" in Nonce_supply_lemma) |
|
143 |
apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify) |
|
144 |
apply (rule_tac x = N in exI) |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
145 |
apply (rule_tac x = "Suc (N+Na)" in exI) |
13926 | 146 |
apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI) |
147 |
apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le) |
|
148 |
done |
|
149 |
||
150 |
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs" |
|
151 |
apply (rule Nonce_supply_lemma [THEN exE]) |
|
152 |
apply (rule someI, blast) |
|
153 |
done |
|
154 |
||
61830 | 155 |
text\<open>Unlike the corresponding property of nonces, we cannot prove |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
156 |
@{term "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"}. |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
157 |
We have infinitely many agents and there is nothing to stop their |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14181
diff
changeset
|
158 |
long-term keys from exhausting all the natural numbers. Instead, |
61830 | 159 |
possibility theorems must assume the existence of a few keys.\<close> |
13926 | 160 |
|
161 |
||
61830 | 162 |
subsection\<open>Specialized Rewriting for Theorems About @{term analz} and Image\<close> |
13926 | 163 |
|
164 |
lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \<notin> A" |
|
165 |
by blast |
|
166 |
||
167 |
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H" |
|
168 |
by blast |
|
169 |
||
13956 | 170 |
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key`(insert K KK) \<union> C" |
13926 | 171 |
by blast |
172 |
||
173 |
(** Reverse the normal simplification of "image" to build up (not break down) |
|
174 |
the set of keys. Use analz_insert_eq with (Un_upper2 RS analz_mono) to |
|
175 |
erase occurrences of forwarded message components (X). **) |
|
176 |
||
177 |
lemmas analz_image_freshK_simps = |
|
61830 | 178 |
simp_thms mem_simps \<comment>\<open>these two allow its use with \<open>only:\<close>\<close> |
13926 | 179 |
disj_comms |
180 |
image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset |
|
181 |
analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD] |
|
182 |
insert_Key_singleton subset_Compl_range |
|
183 |
Key_not_used insert_Key_image Un_assoc [THEN sym] |
|
184 |
||
185 |
(*Lemma for the trivial direction of the if-and-only-if*) |
|
186 |
lemma analz_image_freshK_lemma: |
|
187 |
"(Key K \<in> analz (Key`nE \<union> H)) --> (K \<in> nE | Key K \<in> analz H) ==> |
|
188 |
(Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)" |
|
189 |
by (blast intro: analz_mono [THEN [2] rev_subsetD]) |
|
190 |
||
24122 | 191 |
|
61830 | 192 |
subsection\<open>Tactics for possibility theorems\<close> |
24122 | 193 |
|
13926 | 194 |
ML |
61830 | 195 |
\<open> |
24122 | 196 |
structure Shared = |
197 |
struct |
|
198 |
||
199 |
(*Omitting used_Says makes the tactic much faster: it leaves expressions |
|
200 |
such as Nonce ?N \<notin> used evs that match Nonce_supply*) |
|
201 |
fun possibility_tac ctxt = |
|
202 |
(REPEAT |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
41693
diff
changeset
|
203 |
(ALLGOALS (simp_tac (ctxt |
24122 | 204 |
delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}] |
205 |
setSolver safe_solver)) |
|
206 |
THEN |
|
207 |
REPEAT_FIRST (eq_assume_tac ORELSE' |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
55416
diff
changeset
|
208 |
resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}]))) |
13926 | 209 |
|
24122 | 210 |
(*For harder protocols (such as Recur) where we have to set up some |
211 |
nonces and keys initially*) |
|
212 |
fun basic_possibility_tac ctxt = |
|
213 |
REPEAT |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
41693
diff
changeset
|
214 |
(ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver)) |
24122 | 215 |
THEN |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
55416
diff
changeset
|
216 |
REPEAT_FIRST (resolve_tac ctxt [refl, conjI])) |
24122 | 217 |
|
218 |
||
219 |
val analz_image_freshK_ss = |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
41693
diff
changeset
|
220 |
simpset_of |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
41693
diff
changeset
|
221 |
(@{context} delsimps [image_insert, image_Un] |
24122 | 222 |
delsimps [@{thm imp_disjL}] (*reduces blow-up*) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
41693
diff
changeset
|
223 |
addsimps @{thms analz_image_freshK_simps}) |
24122 | 224 |
|
225 |
end |
|
61830 | 226 |
\<close> |
13926 | 227 |
|
228 |
||
11104 | 229 |
|
230 |
(*Lets blast_tac perform this step without needing the simplifier*) |
|
231 |
lemma invKey_shrK_iff [iff]: |
|
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11230
diff
changeset
|
232 |
"(Key (invKey K) \<in> X) = (Key K \<in> X)" |
13507 | 233 |
by auto |
11104 | 234 |
|
235 |
(*Specialized methods*) |
|
236 |
||
61830 | 237 |
method_setup analz_freshK = \<open> |
30549 | 238 |
Scan.succeed (fn ctxt => |
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
24122
diff
changeset
|
239 |
(SIMPLE_METHOD |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
55416
diff
changeset
|
240 |
(EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]), |
60754 | 241 |
REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}), |
61830 | 242 |
ALLGOALS (asm_simp_tac (put_simpset Shared.analz_image_freshK_ss ctxt))])))\<close> |
11104 | 243 |
"for proving the Session Key Compromise theorem" |
244 |
||
61830 | 245 |
method_setup possibility = \<open> |
246 |
Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt))\<close> |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
21588
diff
changeset
|
247 |
"for proving possibility theorems" |
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
21588
diff
changeset
|
248 |
|
61830 | 249 |
method_setup basic_possibility = \<open> |
250 |
Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt))\<close> |
|
11104 | 251 |
"for proving possibility theorems" |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
252 |
|
12415
74977582a585
Slightly generalized the agents' knowledge theorems
paulson
parents:
11270
diff
changeset
|
253 |
lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)" |
53428 | 254 |
by (cases e) (auto simp: knows_Cons) |
12415
74977582a585
Slightly generalized the agents' knowledge theorems
paulson
parents:
11270
diff
changeset
|
255 |
|
1934 | 256 |
end |