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