author | paulson <lp15@cam.ac.uk> |
Wed, 26 Apr 2017 15:53:35 +0100 | |
changeset 65583 | 8d53b3bebab4 |
parent 62343 | 24106dc44def |
child 67613 | ce654b0e6d69 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/Auth/Recur.thy |
2449 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1996 University of Cambridge |
|
4 |
*) |
|
5 |
||
61830 | 6 |
section\<open>The Otway-Bull Recursive Authentication Protocol\<close> |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
7 |
|
16417 | 8 |
theory Recur imports Public begin |
2449 | 9 |
|
61830 | 10 |
text\<open>End marker for message bundles\<close> |
20768 | 11 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
12 |
END :: "msg" where |
20768 | 13 |
"END == Number 0" |
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
14 |
|
2449 | 15 |
(*Two session keys are distributed to each agent except for the initiator, |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
16 |
who receives one. |
2449 | 17 |
Perhaps the two session keys could be bundled into a single message. |
18 |
*) |
|
23746 | 19 |
inductive_set (*Server's response to the nested message*) |
20 |
respond :: "event list => (msg*msg*key)set" |
|
21 |
for evs :: "event list" |
|
22 |
where |
|
11264 | 23 |
One: "Key KAB \<notin> used evs |
61956 | 24 |
==> (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>, |
25 |
\<lbrace>Crypt (shrK A) \<lbrace>Key KAB, Agent B, Nonce NA\<rbrace>, END\<rbrace>, |
|
11264 | 26 |
KAB) \<in> respond evs" |
2449 | 27 |
|
2532 | 28 |
(*The most recent session key is passed up to the caller*) |
23746 | 29 |
| Cons: "[| (PA, RA, KAB) \<in> respond evs; |
11264 | 30 |
Key KBC \<notin> used evs; Key KBC \<notin> parts {RA}; |
61956 | 31 |
PA = Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, P\<rbrace> |] |
32 |
==> (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>, |
|
33 |
\<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>, |
|
34 |
Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>, |
|
35 |
RA\<rbrace>, |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
36 |
KBC) |
11264 | 37 |
\<in> respond evs" |
2449 | 38 |
|
39 |
||
2481 | 40 |
(*Induction over "respond" can be difficult due to the complexity of the |
2532 | 41 |
subgoals. Set "responses" captures the general form of certificates. |
2449 | 42 |
*) |
23746 | 43 |
inductive_set |
44 |
responses :: "event list => msg set" |
|
45 |
for evs :: "event list" |
|
46 |
where |
|
2449 | 47 |
(*Server terminates lists*) |
11264 | 48 |
Nil: "END \<in> responses evs" |
2449 | 49 |
|
23746 | 50 |
| Cons: "[| RA \<in> responses evs; Key KAB \<notin> used evs |] |
61956 | 51 |
==> \<lbrace>Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>, |
52 |
RA\<rbrace> \<in> responses evs" |
|
2449 | 53 |
|
54 |
||
23746 | 55 |
inductive_set recur :: "event list set" |
56 |
where |
|
2449 | 57 |
(*Initial trace is empty*) |
11264 | 58 |
Nil: "[] \<in> recur" |
2449 | 59 |
|
2532 | 60 |
(*The spy MAY say anything he CAN say. Common to |
2449 | 61 |
all similar protocols.*) |
23746 | 62 |
| Fake: "[| evsf \<in> recur; X \<in> synth (analz (knows Spy evsf)) |] |
11264 | 63 |
==> Says Spy B X # evsf \<in> recur" |
2449 | 64 |
|
65 |
(*Alice initiates a protocol run. |
|
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
66 |
END is a placeholder to terminate the nesting.*) |
23746 | 67 |
| RA1: "[| evs1 \<in> recur; Nonce NA \<notin> used evs1 |] |
61956 | 68 |
==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>) |
11264 | 69 |
# evs1 \<in> recur" |
2449 | 70 |
|
71 |
(*Bob's response to Alice's message. C might be the Server. |
|
61956 | 72 |
We omit PA = \<lbrace>XA, Agent A, Agent B, Nonce NA, P\<rbrace> because |
4552
bb8ff763c93d
Simplified proofs by omitting PA = {|XA, ...|} from RA2
paulson
parents:
3683
diff
changeset
|
73 |
it complicates proofs, so B may respond to any message at all!*) |
23746 | 74 |
| RA2: "[| evs2 \<in> recur; Nonce NB \<notin> used evs2; |
11264 | 75 |
Says A' B PA \<in> set evs2 |] |
61956 | 76 |
==> Says B C (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>) |
11264 | 77 |
# evs2 \<in> recur" |
2449 | 78 |
|
2550
8d8344bcf98a
Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents:
2532
diff
changeset
|
79 |
(*The Server receives Bob's message and prepares a response.*) |
23746 | 80 |
| RA3: "[| evs3 \<in> recur; Says B' Server PB \<in> set evs3; |
11264 | 81 |
(PB,RB,K) \<in> respond evs3 |] |
82 |
==> Says Server B RB # evs3 \<in> recur" |
|
2449 | 83 |
|
84 |
(*Bob receives the returned message and compares the Nonces with |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
85 |
those in the message he previously sent the Server.*) |
23746 | 86 |
| RA4: "[| evs4 \<in> recur; |
61956 | 87 |
Says B C \<lbrace>XH, Agent B, Agent C, Nonce NB, |
88 |
XA, Agent A, Agent B, Nonce NA, P\<rbrace> \<in> set evs4; |
|
89 |
Says C' B \<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>, |
|
90 |
Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>, |
|
91 |
RA\<rbrace> \<in> set evs4 |] |
|
11264 | 92 |
==> Says B A RA # evs4 \<in> recur" |
5359 | 93 |
|
94 |
(*No "oops" message can easily be expressed. Each session key is |
|
11264 | 95 |
associated--in two separate messages--with two nonces. This is |
5359 | 96 |
one try, but it isn't that useful. Re domino attack, note that |
24122 | 97 |
Recur.thy proves that each session key is secure provided the two |
5359 | 98 |
peers are, even if there are compromised agents elsewhere in |
99 |
the chain. Oops cases proved using parts_cut, Key_in_keysFor_parts, |
|
100 |
etc. |
|
101 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
102 |
Oops: "[| evso \<in> recur; Says Server B RB \<in> set evso; |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32404
diff
changeset
|
103 |
RB \<in> responses evs'; Key K \<in> parts {RB} |] |
61956 | 104 |
==> Notes Spy \<lbrace>Key K, RB\<rbrace> # evso \<in> recur" |
5359 | 105 |
*) |
11264 | 106 |
|
107 |
||
108 |
declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
|
109 |
declare parts.Body [dest] |
|
110 |
declare analz_into_parts [dest] |
|
111 |
declare Fake_parts_insert_in_Un [dest] |
|
112 |
||
113 |
||
114 |
(** Possibility properties: traces that reach the end |
|
115 |
ONE theorem would be more elegant and faster! |
|
116 |
By induction on a list of agents (no repetitions) |
|
117 |
**) |
|
118 |
||
119 |
||
61830 | 120 |
text\<open>Simplest case: Alice goes directly to the server\<close> |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
121 |
lemma "Key K \<notin> used [] |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
122 |
==> \<exists>NA. \<exists>evs \<in> recur. |
61956 | 123 |
Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent Server, Nonce NA\<rbrace>, |
124 |
END\<rbrace> \<in> set evs" |
|
11264 | 125 |
apply (intro exI bexI) |
126 |
apply (rule_tac [2] recur.Nil [THEN recur.RA1, |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
127 |
THEN recur.RA3 [OF _ _ respond.One]]) |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
128 |
apply (possibility, simp add: used_Cons) |
11264 | 129 |
done |
130 |
||
131 |
||
61830 | 132 |
text\<open>Case two: Alice, Bob and the server\<close> |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
133 |
lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K'; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
134 |
Nonce NA \<notin> used []; Nonce NB \<notin> used []; NA < NB |] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
135 |
==> \<exists>NA. \<exists>evs \<in> recur. |
61956 | 136 |
Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>, |
137 |
END\<rbrace> \<in> set evs" |
|
11264 | 138 |
apply (intro exI bexI) |
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
139 |
apply (rule_tac [2] |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
140 |
recur.Nil |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
141 |
[THEN recur.RA1 [of _ NA], |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32404
diff
changeset
|
142 |
THEN recur.RA2 [of _ NB], |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32404
diff
changeset
|
143 |
THEN recur.RA3 [OF _ _ respond.One |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
144 |
[THEN respond.Cons [of _ _ K _ K']]], |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32404
diff
changeset
|
145 |
THEN recur.RA4], possibility) |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
146 |
apply (auto simp add: used_Cons) |
11264 | 147 |
done |
148 |
||
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
149 |
(*Case three: Alice, Bob, Charlie and the server Rather slow (5 seconds)*) |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
150 |
lemma "[| Key K \<notin> used []; Key K' \<notin> used []; |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
151 |
Key K'' \<notin> used []; K \<noteq> K'; K' \<noteq> K''; K \<noteq> K''; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
152 |
Nonce NA \<notin> used []; Nonce NB \<notin> used []; Nonce NC \<notin> used []; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
153 |
NA < NB; NB < NC |] |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
154 |
==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur. |
61956 | 155 |
Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>, |
156 |
END\<rbrace> \<in> set evs" |
|
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
157 |
apply (intro exI bexI) |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
158 |
apply (rule_tac [2] |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
159 |
recur.Nil [THEN recur.RA1, |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
160 |
THEN recur.RA2, THEN recur.RA2, |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
161 |
THEN recur.RA3 |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
162 |
[OF _ _ respond.One |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
163 |
[THEN respond.Cons, THEN respond.Cons]], |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
164 |
THEN recur.RA4, THEN recur.RA4]) |
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23746
diff
changeset
|
165 |
apply basic_possibility |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
166 |
apply (tactic "DEPTH_SOLVE (swap_res_tac @{context} [refl, conjI, disjCI] 1)") |
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
167 |
done |
11264 | 168 |
|
169 |
||
170 |
lemma respond_imp_not_used: "(PA,RB,KAB) \<in> respond evs ==> Key KAB \<notin> used evs" |
|
171 |
by (erule respond.induct, simp_all) |
|
172 |
||
173 |
lemma Key_in_parts_respond [rule_format]: |
|
174 |
"[| Key K \<in> parts {RB}; (PB,RB,K') \<in> respond evs |] ==> Key K \<notin> used evs" |
|
175 |
apply (erule rev_mp, erule respond.induct) |
|
176 |
apply (auto dest: Key_not_used respond_imp_not_used) |
|
177 |
done |
|
178 |
||
61830 | 179 |
text\<open>Simple inductive reasoning about responses\<close> |
11264 | 180 |
lemma respond_imp_responses: |
181 |
"(PA,RB,KAB) \<in> respond evs ==> RB \<in> responses evs" |
|
182 |
apply (erule respond.induct) |
|
183 |
apply (blast intro!: respond_imp_not_used responses.intros)+ |
|
184 |
done |
|
185 |
||
186 |
||
187 |
(** For reasoning about the encrypted portion of messages **) |
|
188 |
||
189 |
lemmas RA2_analz_spies = Says_imp_spies [THEN analz.Inj] |
|
190 |
||
191 |
lemma RA4_analz_spies: |
|
61956 | 192 |
"Says C' B \<lbrace>Crypt K X, X', RA\<rbrace> \<in> set evs ==> RA \<in> analz (spies evs)" |
11264 | 193 |
by blast |
194 |
||
195 |
||
196 |
(*RA2_analz... and RA4_analz... let us treat those cases using the same |
|
197 |
argument as for the Fake case. This is possible for most, but not all, |
|
198 |
proofs: Fake does not invent new nonces (as in RA2), and of course Fake |
|
199 |
messages originate from the Spy. *) |
|
200 |
||
201 |
lemmas RA2_parts_spies = RA2_analz_spies [THEN analz_into_parts] |
|
202 |
lemmas RA4_parts_spies = RA4_analz_spies [THEN analz_into_parts] |
|
203 |
||
204 |
||
205 |
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY |
|
206 |
sends messages containing X! **) |
|
207 |
||
208 |
(** Spy never sees another agent's shared key! (unless it's bad at start) **) |
|
209 |
||
210 |
lemma Spy_see_shrK [simp]: |
|
211 |
"evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)" |
|
13507 | 212 |
apply (erule recur.induct, auto) |
61830 | 213 |
txt\<open>RA3. It's ugly to call auto twice, but it seems necessary.\<close> |
11264 | 214 |
apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies) |
215 |
done |
|
216 |
||
217 |
lemma Spy_analz_shrK [simp]: |
|
218 |
"evs \<in> recur ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)" |
|
219 |
by auto |
|
220 |
||
221 |
lemma Spy_see_shrK_D [dest!]: |
|
222 |
"[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> recur|] ==> A \<in> bad" |
|
223 |
by (blast dest: Spy_see_shrK) |
|
224 |
||
225 |
||
226 |
(*** Proofs involving analz ***) |
|
227 |
||
228 |
(** Session keys are not used to encrypt other session keys **) |
|
229 |
||
230 |
(*Version for "responses" relation. Handles case RA3 in the theorem below. |
|
231 |
Note that it holds for *any* set H (not just "spies evs") |
|
232 |
satisfying the inductive hypothesis.*) |
|
233 |
lemma resp_analz_image_freshK_lemma: |
|
234 |
"[| RB \<in> responses evs; |
|
235 |
\<forall>K KK. KK \<subseteq> - (range shrK) --> |
|
236 |
(Key K \<in> analz (Key`KK Un H)) = |
|
237 |
(K \<in> KK | Key K \<in> analz H) |] |
|
238 |
==> \<forall>K KK. KK \<subseteq> - (range shrK) --> |
|
239 |
(Key K \<in> analz (insert RB (Key`KK Un H))) = |
|
240 |
(K \<in> KK | Key K \<in> analz (insert RB H))" |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
241 |
apply (erule responses.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
242 |
apply (simp_all del: image_insert |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32404
diff
changeset
|
243 |
add: analz_image_freshK_simps, auto) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
244 |
done |
11264 | 245 |
|
246 |
||
61830 | 247 |
text\<open>Version for the protocol. Proof is easy, thanks to the lemma.\<close> |
11264 | 248 |
lemma raw_analz_image_freshK: |
249 |
"evs \<in> recur ==> |
|
250 |
\<forall>K KK. KK \<subseteq> - (range shrK) --> |
|
251 |
(Key K \<in> analz (Key`KK Un (spies evs))) = |
|
252 |
(K \<in> KK | Key K \<in> analz (spies evs))" |
|
253 |
apply (erule recur.induct) |
|
254 |
apply (drule_tac [4] RA2_analz_spies, |
|
11281 | 255 |
drule_tac [5] respond_imp_responses, |
13507 | 256 |
drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz) |
61830 | 257 |
txt\<open>RA3\<close> |
11264 | 258 |
apply (simp_all add: resp_analz_image_freshK_lemma) |
259 |
done |
|
260 |
||
261 |
||
262 |
(*Instance of the lemma with H replaced by (spies evs): |
|
263 |
[| RB \<in> responses evs; evs \<in> recur; |] |
|
264 |
==> KK \<subseteq> - (range shrK) --> |
|
265 |
Key K \<in> analz (insert RB (Key`KK Un spies evs)) = |
|
266 |
(K \<in> KK | Key K \<in> analz (insert RB (spies evs))) |
|
267 |
*) |
|
268 |
lemmas resp_analz_image_freshK = |
|
269 |
resp_analz_image_freshK_lemma [OF _ raw_analz_image_freshK] |
|
270 |
||
271 |
lemma analz_insert_freshK: |
|
272 |
"[| evs \<in> recur; KAB \<notin> range shrK |] |
|
11655 | 273 |
==> (Key K \<in> analz (insert (Key KAB) (spies evs))) = |
11264 | 274 |
(K = KAB | Key K \<in> analz (spies evs))" |
275 |
by (simp del: image_insert |
|
276 |
add: analz_image_freshK_simps raw_analz_image_freshK) |
|
277 |
||
278 |
||
61830 | 279 |
text\<open>Everything that's hashed is already in past traffic.\<close> |
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11264
diff
changeset
|
280 |
lemma Hash_imp_body: |
61956 | 281 |
"[| Hash \<lbrace>Key(shrK A), X\<rbrace> \<in> parts (spies evs); |
11264 | 282 |
evs \<in> recur; A \<notin> bad |] ==> X \<in> parts (spies evs)" |
283 |
apply (erule rev_mp) |
|
284 |
apply (erule recur.induct, |
|
11281 | 285 |
drule_tac [6] RA4_parts_spies, |
286 |
drule_tac [5] respond_imp_responses, |
|
287 |
drule_tac [4] RA2_parts_spies) |
|
61830 | 288 |
txt\<open>RA3 requires a further induction\<close> |
13507 | 289 |
apply (erule_tac [5] responses.induct, simp_all) |
61830 | 290 |
txt\<open>Fake\<close> |
11264 | 291 |
apply (blast intro: parts_insertI) |
292 |
done |
|
293 |
||
294 |
||
295 |
(** The Nonce NA uniquely identifies A's message. |
|
296 |
This theorem applies to steps RA1 and RA2! |
|
297 |
||
298 |
Unicity is not used in other proofs but is desirable in its own right. |
|
299 |
**) |
|
300 |
||
301 |
lemma unique_NA: |
|
61956 | 302 |
"[| Hash \<lbrace>Key(shrK A), Agent A, B, NA, P\<rbrace> \<in> parts (spies evs); |
303 |
Hash \<lbrace>Key(shrK A), Agent A, B',NA, P'\<rbrace> \<in> parts (spies evs); |
|
11264 | 304 |
evs \<in> recur; A \<notin> bad |] |
305 |
==> B=B' & P=P'" |
|
306 |
apply (erule rev_mp, erule rev_mp) |
|
307 |
apply (erule recur.induct, |
|
11281 | 308 |
drule_tac [5] respond_imp_responses) |
11264 | 309 |
apply (force, simp_all) |
61830 | 310 |
txt\<open>Fake\<close> |
11264 | 311 |
apply blast |
312 |
apply (erule_tac [3] responses.induct) |
|
61830 | 313 |
txt\<open>RA1,2: creation of new Nonce\<close> |
11264 | 314 |
apply simp_all |
315 |
apply (blast dest!: Hash_imp_body)+ |
|
316 |
done |
|
317 |
||
318 |
||
319 |
(*** Lemmas concerning the Server's response |
|
320 |
(relations "respond" and "responses") |
|
321 |
***) |
|
322 |
||
323 |
lemma shrK_in_analz_respond [simp]: |
|
324 |
"[| RB \<in> responses evs; evs \<in> recur |] |
|
325 |
==> (Key (shrK B) \<in> analz (insert RB (spies evs))) = (B:bad)" |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
326 |
apply (erule responses.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
327 |
apply (simp_all del: image_insert |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
328 |
add: analz_image_freshK_simps resp_analz_image_freshK, auto) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
329 |
done |
11264 | 330 |
|
331 |
||
332 |
lemma resp_analz_insert_lemma: |
|
333 |
"[| Key K \<in> analz (insert RB H); |
|
334 |
\<forall>K KK. KK \<subseteq> - (range shrK) --> |
|
335 |
(Key K \<in> analz (Key`KK Un H)) = |
|
336 |
(K \<in> KK | Key K \<in> analz H); |
|
337 |
RB \<in> responses evs |] |
|
338 |
==> (Key K \<in> parts{RB} | Key K \<in> analz H)" |
|
339 |
apply (erule rev_mp, erule responses.induct) |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61956
diff
changeset
|
340 |
apply (simp_all del: image_insert parts_image |
11264 | 341 |
add: analz_image_freshK_simps resp_analz_image_freshK_lemma) |
61830 | 342 |
txt\<open>Simplification using two distinct treatments of "image"\<close> |
13507 | 343 |
apply (simp add: parts_insert2, blast) |
11264 | 344 |
done |
345 |
||
346 |
lemmas resp_analz_insert = |
|
347 |
resp_analz_insert_lemma [OF _ raw_analz_image_freshK] |
|
348 |
||
61830 | 349 |
text\<open>The last key returned by respond indeed appears in a certificate\<close> |
11264 | 350 |
lemma respond_certificate: |
61956 | 351 |
"(Hash[Key(shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs |
352 |
==> Crypt (shrK A) \<lbrace>Key K, B, NA\<rbrace> \<in> parts {RA}" |
|
23746 | 353 |
apply (ind_cases "(Hash[Key (shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs") |
11264 | 354 |
apply simp_all |
355 |
done |
|
356 |
||
357 |
(*This unicity proof differs from all the others in the HOL/Auth directory. |
|
358 |
The conclusion isn't quite unicity but duplicity, in that there are two |
|
359 |
possibilities. Also, the presence of two different matching messages in |
|
360 |
the inductive step complicates the case analysis. Unusually for such proofs, |
|
361 |
the quantifiers appear to be necessary.*) |
|
362 |
lemma unique_lemma [rule_format]: |
|
363 |
"(PB,RB,KXY) \<in> respond evs ==> |
|
61956 | 364 |
\<forall>A B N. Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB} --> |
365 |
(\<forall>A' B' N'. Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB} --> |
|
11264 | 366 |
(A'=A & B'=B) | (A'=B & B'=A))" |
367 |
apply (erule respond.induct) |
|
368 |
apply (simp_all add: all_conj_distrib) |
|
369 |
apply (blast dest: respond_certificate) |
|
370 |
done |
|
371 |
||
372 |
lemma unique_session_keys: |
|
61956 | 373 |
"[| Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB}; |
374 |
Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB}; |
|
11264 | 375 |
(PB,RB,KXY) \<in> respond evs |] |
376 |
==> (A'=A & B'=B) | (A'=B & B'=A)" |
|
377 |
by (rule unique_lemma, auto) |
|
378 |
||
379 |
||
380 |
(** Crucial secrecy property: Spy does not see the keys sent in msg RA3 |
|
381 |
Does not in itself guarantee security: an attack could violate |
|
382 |
the premises, e.g. by having A=Spy **) |
|
383 |
||
384 |
lemma respond_Spy_not_see_session_key [rule_format]: |
|
385 |
"[| (PB,RB,KAB) \<in> respond evs; evs \<in> recur |] |
|
386 |
==> \<forall>A A' N. A \<notin> bad & A' \<notin> bad --> |
|
61956 | 387 |
Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts{RB} --> |
11264 | 388 |
Key K \<notin> analz (insert RB (spies evs))" |
389 |
apply (erule respond.induct) |
|
390 |
apply (frule_tac [2] respond_imp_responses) |
|
391 |
apply (frule_tac [2] respond_imp_not_used) |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61956
diff
changeset
|
392 |
apply (simp_all del: image_insert parts_image |
11264 | 393 |
add: analz_image_freshK_simps split_ifs shrK_in_analz_respond |
394 |
resp_analz_image_freshK parts_insert2) |
|
61830 | 395 |
txt\<open>Base case of respond\<close> |
11264 | 396 |
apply blast |
61830 | 397 |
txt\<open>Inductive step of respond\<close> |
13507 | 398 |
apply (intro allI conjI impI, simp_all) |
61830 | 399 |
txt\<open>by unicity, either @{term "B=Aa"} or @{term "B=A'"}, a contradiction |
400 |
if @{term "B \<in> bad"}\<close> |
|
13935 | 401 |
apply (blast dest: unique_session_keys respond_certificate) |
11264 | 402 |
apply (blast dest!: respond_certificate) |
403 |
apply (blast dest!: resp_analz_insert) |
|
404 |
done |
|
405 |
||
406 |
||
407 |
lemma Spy_not_see_session_key: |
|
61956 | 408 |
"[| Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts (spies evs); |
11264 | 409 |
A \<notin> bad; A' \<notin> bad; evs \<in> recur |] |
410 |
==> Key K \<notin> analz (spies evs)" |
|
411 |
apply (erule rev_mp) |
|
412 |
apply (erule recur.induct) |
|
413 |
apply (drule_tac [4] RA2_analz_spies, |
|
414 |
frule_tac [5] respond_imp_responses, |
|
415 |
drule_tac [6] RA4_analz_spies, |
|
416 |
simp_all add: split_ifs analz_insert_eq analz_insert_freshK) |
|
61830 | 417 |
txt\<open>Fake\<close> |
11264 | 418 |
apply spy_analz |
61830 | 419 |
txt\<open>RA2\<close> |
11264 | 420 |
apply blast |
61830 | 421 |
txt\<open>RA3\<close> |
11264 | 422 |
apply (simp add: parts_insert_spies) |
32404 | 423 |
apply (metis Key_in_parts_respond parts.Body parts.Fst resp_analz_insert |
424 |
respond_Spy_not_see_session_key usedI) |
|
61830 | 425 |
txt\<open>RA4\<close> |
11264 | 426 |
apply blast |
427 |
done |
|
428 |
||
429 |
(**** Authenticity properties for Agents ****) |
|
430 |
||
61830 | 431 |
text\<open>The response never contains Hashes\<close> |
11264 | 432 |
lemma Hash_in_parts_respond: |
61956 | 433 |
"[| Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts (insert RB H); |
11264 | 434 |
(PB,RB,K) \<in> respond evs |] |
61956 | 435 |
==> Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts H" |
11264 | 436 |
apply (erule rev_mp) |
13507 | 437 |
apply (erule respond_imp_responses [THEN responses.induct], auto) |
11264 | 438 |
done |
439 |
||
61830 | 440 |
text\<open>Only RA1 or RA2 can have caused such a part of a message to appear. |
11264 | 441 |
This result is of no use to B, who cannot verify the Hash. Moreover, |
442 |
it can say nothing about how recent A's message is. It might later be |
|
61830 | 443 |
used to prove B's presence to A at the run's conclusion.\<close> |
11264 | 444 |
lemma Hash_auth_sender [rule_format]: |
61956 | 445 |
"[| Hash \<lbrace>Key(shrK A), Agent A, Agent B, NA, P\<rbrace> \<in> parts(spies evs); |
11264 | 446 |
A \<notin> bad; evs \<in> recur |] |
61956 | 447 |
==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, NA, P\<rbrace>) \<in> set evs" |
11264 | 448 |
apply (unfold HPair_def) |
449 |
apply (erule rev_mp) |
|
450 |
apply (erule recur.induct, |
|
11281 | 451 |
drule_tac [6] RA4_parts_spies, |
452 |
drule_tac [4] RA2_parts_spies, |
|
11264 | 453 |
simp_all) |
61830 | 454 |
txt\<open>Fake, RA3\<close> |
11281 | 455 |
apply (blast dest: Hash_in_parts_respond)+ |
11264 | 456 |
done |
457 |
||
458 |
(** These two results subsume (for all agents) the guarantees proved |
|
459 |
separately for A and B in the Otway-Rees protocol. |
|
460 |
**) |
|
461 |
||
462 |
||
61830 | 463 |
text\<open>Certificates can only originate with the Server.\<close> |
11264 | 464 |
lemma Cert_imp_Server_msg: |
465 |
"[| Crypt (shrK A) Y \<in> parts (spies evs); |
|
466 |
A \<notin> bad; evs \<in> recur |] |
|
467 |
==> \<exists>C RC. Says Server C RC \<in> set evs & |
|
468 |
Crypt (shrK A) Y \<in> parts {RC}" |
|
469 |
apply (erule rev_mp, erule recur.induct, simp_all) |
|
61830 | 470 |
txt\<open>Fake\<close> |
11264 | 471 |
apply blast |
61830 | 472 |
txt\<open>RA1\<close> |
11264 | 473 |
apply blast |
61830 | 474 |
txt\<open>RA2: it cannot be a new Nonce, contradiction.\<close> |
11264 | 475 |
apply blast |
61830 | 476 |
txt\<open>RA3. Pity that the proof is so brittle: this step requires the rewriting, |
477 |
which however would break all other steps.\<close> |
|
11264 | 478 |
apply (simp add: parts_insert_spies, blast) |
61830 | 479 |
txt\<open>RA4\<close> |
11264 | 480 |
apply blast |
481 |
done |
|
482 |
||
483 |
end |