author | berghofe |
Fri, 28 Apr 2006 15:59:31 +0200 | |
changeset 19497 | 630073ef9212 |
parent 17778 | 93d7e524417a |
child 23746 | a455e69c31cc |
permissions | -rw-r--r-- |
2002 | 1 |
(* Title: HOL/Auth/OtwayRees_Bad |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
5 |
*) |
2002 | 6 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
7 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
8 |
header{*The Otway-Rees Protocol: The Faulty BAN Version*} |
2002 | 9 |
|
16417 | 10 |
theory OtwayRees_Bad imports Public begin |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
11 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
12 |
text{*The FAULTY version omitting encryption of Nonce NB, as suggested on |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
13 |
page 247 of |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
14 |
Burrows, Abadi and Needham (1988). A Logic of Authentication. |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
15 |
Proc. Royal Soc. 426 |
11251 | 16 |
|
17 |
This file illustrates the consequences of such errors. We can still prove |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
18 |
impressive-looking properties such as @{text Spy_not_see_encrypted_key}, yet |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
19 |
the protocol is open to a middleperson attack. Attempting to prove some key |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
20 |
lemmas indicates the possibility of this attack.*} |
2052 | 21 |
|
11251 | 22 |
consts otway :: "event list set" |
23 |
inductive "otway" |
|
24 |
intros |
|
14225 | 25 |
Nil: --{*The empty trace*} |
26 |
"[] \<in> otway" |
|
2002 | 27 |
|
14225 | 28 |
Fake: --{*The Spy may say anything he can say. The sender field is correct, |
29 |
but agents don't use that information.*} |
|
30 |
"[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |] |
|
11251 | 31 |
==> Says Spy B X # evsf \<in> otway" |
2002 | 32 |
|
14225 | 33 |
|
34 |
Reception: --{*A message that has been sent can be received by the |
|
35 |
intended recipient.*} |
|
36 |
"[| evsr \<in> otway; Says A B X \<in>set evsr |] |
|
11251 | 37 |
==> Gets B X # evsr \<in> otway" |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
38 |
|
14225 | 39 |
OR1: --{*Alice initiates a protocol run*} |
40 |
"[| evs1 \<in> otway; Nonce NA \<notin> used evs1 |] |
|
11251 | 41 |
==> Says A B {|Nonce NA, Agent A, Agent B, |
42 |
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} |
|
43 |
# evs1 \<in> otway" |
|
2002 | 44 |
|
14225 | 45 |
OR2: --{*Bob's response to Alice's message. |
46 |
This variant of the protocol does NOT encrypt NB.*} |
|
47 |
"[| evs2 \<in> otway; Nonce NB \<notin> used evs2; |
|
11251 | 48 |
Gets B {|Nonce NA, Agent A, Agent B, X|} \<in> set evs2 |] |
49 |
==> Says B Server |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
50 |
{|Nonce NA, Agent A, Agent B, X, Nonce NB, |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset
|
51 |
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
11251 | 52 |
# evs2 \<in> otway" |
2002 | 53 |
|
14225 | 54 |
OR3: --{*The Server receives Bob's message and checks that the three NAs |
2002 | 55 |
match. Then he sends a new session key to Bob with a packet for |
14225 | 56 |
forwarding to Alice.*} |
57 |
"[| evs3 \<in> otway; Key KAB \<notin> used evs3; |
|
11251 | 58 |
Gets Server |
59 |
{|Nonce NA, Agent A, Agent B, |
|
60 |
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, |
|
61 |
Nonce NB, |
|
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset
|
62 |
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
11251 | 63 |
\<in> set evs3 |] |
64 |
==> Says Server B |
|
65 |
{|Nonce NA, |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
66 |
Crypt (shrK A) {|Nonce NA, Key KAB|}, |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
67 |
Crypt (shrK B) {|Nonce NB, Key KAB|}|} |
11251 | 68 |
# evs3 \<in> otway" |
2002 | 69 |
|
14225 | 70 |
OR4: --{*Bob receives the Server's (?) message and compares the Nonces with |
71 |
those in the message he previously sent the Server. |
|
72 |
Need @{term "B \<noteq> Server"} because we allow messages to self.*} |
|
73 |
"[| evs4 \<in> otway; B \<noteq> Server; |
|
4522
0218c486cf07
Restored the ciphertext in OR4 in order to make the spec closer to that in
paulson
parents:
3683
diff
changeset
|
74 |
Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, |
0218c486cf07
Restored the ciphertext in OR4 in order to make the spec closer to that in
paulson
parents:
3683
diff
changeset
|
75 |
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} |
11251 | 76 |
\<in> set evs4; |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
77 |
Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
11251 | 78 |
\<in> set evs4 |] |
79 |
==> Says B A {|Nonce NA, X|} # evs4 \<in> otway" |
|
2002 | 80 |
|
14225 | 81 |
Oops: --{*This message models possible leaks of session keys. The nonces |
82 |
identify the protocol run.*} |
|
83 |
"[| evso \<in> otway; |
|
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset
|
84 |
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
11251 | 85 |
\<in> set evso |] |
86 |
==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway" |
|
87 |
||
88 |
||
89 |
declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
|
90 |
declare parts.Body [dest] |
|
91 |
declare analz_into_parts [dest] |
|
92 |
declare Fake_parts_insert_in_Un [dest] |
|
93 |
||
14225 | 94 |
text{*A "possibility property": there are traces that reach the end*} |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13507
diff
changeset
|
95 |
lemma "[| B \<noteq> Server; Key K \<notin> used [] |] |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13507
diff
changeset
|
96 |
==> \<exists>NA. \<exists>evs \<in> otway. |
11251 | 97 |
Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} |
98 |
\<in> set evs" |
|
99 |
apply (intro exI bexI) |
|
100 |
apply (rule_tac [2] otway.Nil |
|
101 |
[THEN otway.OR1, THEN otway.Reception, |
|
102 |
THEN otway.OR2, THEN otway.Reception, |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13507
diff
changeset
|
103 |
THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13507
diff
changeset
|
104 |
apply (possibility, simp add: used_Cons) |
11251 | 105 |
done |
106 |
||
107 |
lemma Gets_imp_Says [dest!]: |
|
108 |
"[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs" |
|
109 |
apply (erule rev_mp) |
|
13507 | 110 |
apply (erule otway.induct, auto) |
11251 | 111 |
done |
112 |
||
113 |
||
14225 | 114 |
subsection{*For reasoning about the encrypted portion of messages *} |
11251 | 115 |
|
116 |
lemma OR2_analz_knows_Spy: |
|
117 |
"[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs; evs \<in> otway |] |
|
118 |
==> X \<in> analz (knows Spy evs)" |
|
119 |
by blast |
|
120 |
||
121 |
lemma OR4_analz_knows_Spy: |
|
122 |
"[| Gets B {|N, X, Crypt (shrK B) X'|} \<in> set evs; evs \<in> otway |] |
|
123 |
==> X \<in> analz (knows Spy evs)" |
|
124 |
by blast |
|
125 |
||
126 |
lemma Oops_parts_knows_Spy: |
|
127 |
"Says Server B {|NA, X, Crypt K' {|NB,K|}|} \<in> set evs |
|
128 |
==> K \<in> parts (knows Spy evs)" |
|
129 |
by blast |
|
130 |
||
14225 | 131 |
text{*Forwarding lemma: see comments in OtwayRees.thy*} |
11251 | 132 |
lemmas OR2_parts_knows_Spy = |
133 |
OR2_analz_knows_Spy [THEN analz_into_parts, standard] |
|
134 |
||
135 |
||
14225 | 136 |
text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that |
137 |
NOBODY sends messages containing X! *} |
|
11251 | 138 |
|
14225 | 139 |
text{*Spy never sees a good agent's shared key!*} |
11251 | 140 |
lemma Spy_see_shrK [simp]: |
141 |
"evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
|
14225 | 142 |
by (erule otway.induct, force, |
143 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
|
144 |
||
11251 | 145 |
|
146 |
lemma Spy_analz_shrK [simp]: |
|
147 |
"evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
|
148 |
by auto |
|
149 |
||
150 |
lemma Spy_see_shrK_D [dest!]: |
|
151 |
"[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway|] ==> A \<in> bad" |
|
152 |
by (blast dest: Spy_see_shrK) |
|
153 |
||
154 |
||
14225 | 155 |
subsection{*Proofs involving analz *} |
11251 | 156 |
|
14225 | 157 |
text{*Describes the form of K and NA when the Server sends this message. Also |
158 |
for Oops case.*} |
|
11251 | 159 |
lemma Says_Server_message_form: |
160 |
"[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
|
161 |
evs \<in> otway |] |
|
162 |
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)" |
|
163 |
apply (erule rev_mp) |
|
17778 | 164 |
apply (erule otway.induct, simp_all) |
11251 | 165 |
done |
166 |
||
167 |
||
168 |
(**** |
|
169 |
The following is to prove theorems of the form |
|
170 |
||
171 |
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
|
172 |
Key K \<in> analz (knows Spy evs) |
|
173 |
||
174 |
A more general formula must be proved inductively. |
|
175 |
****) |
|
176 |
||
177 |
||
14225 | 178 |
text{*Session keys are not used to encrypt other session keys*} |
11251 | 179 |
|
14225 | 180 |
text{*The equality makes the induction hypothesis easier to apply*} |
11251 | 181 |
lemma analz_image_freshK [rule_format]: |
182 |
"evs \<in> otway ==> |
|
183 |
\<forall>K KK. KK <= -(range shrK) --> |
|
184 |
(Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
|
185 |
(K \<in> KK | Key K \<in> analz (knows Spy evs))" |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
186 |
apply (erule otway.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
187 |
apply (frule_tac [8] Says_Server_message_form) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
188 |
apply (drule_tac [7] OR4_analz_knows_Spy) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
189 |
apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto) |
11251 | 190 |
done |
191 |
||
192 |
lemma analz_insert_freshK: |
|
193 |
"[| evs \<in> otway; KAB \<notin> range shrK |] ==> |
|
11655 | 194 |
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
11251 | 195 |
(K = KAB | Key K \<in> analz (knows Spy evs))" |
196 |
by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
197 |
||
198 |
||
14225 | 199 |
text{*The Key K uniquely identifies the Server's message. *} |
11251 | 200 |
lemma unique_session_keys: |
201 |
"[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \<in> set evs; |
|
202 |
Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs; |
|
203 |
evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'" |
|
204 |
apply (erule rev_mp) |
|
205 |
apply (erule rev_mp) |
|
206 |
apply (erule otway.induct, simp_all) |
|
14225 | 207 |
apply blast+ --{*OR3 and OR4*} |
11251 | 208 |
done |
209 |
||
210 |
||
14238 | 211 |
text{*Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
11251 | 212 |
Does not in itself guarantee security: an attack could violate |
14225 | 213 |
the premises, e.g. by having @{term "A=Spy"} *} |
11251 | 214 |
lemma secrecy_lemma: |
215 |
"[| A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
216 |
==> Says Server B |
|
217 |
{|NA, Crypt (shrK A) {|NA, Key K|}, |
|
218 |
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs --> |
|
219 |
Notes Spy {|NA, NB, Key K|} \<notin> set evs --> |
|
220 |
Key K \<notin> analz (knows Spy evs)" |
|
221 |
apply (erule otway.induct, force) |
|
222 |
apply (frule_tac [7] Says_Server_message_form) |
|
223 |
apply (drule_tac [6] OR4_analz_knows_Spy) |
|
224 |
apply (drule_tac [4] OR2_analz_knows_Spy) |
|
14225 | 225 |
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) |
226 |
apply spy_analz --{*Fake*} |
|
227 |
apply (blast dest: unique_session_keys)+ --{*OR3, OR4, Oops*} |
|
11251 | 228 |
done |
229 |
||
230 |
||
231 |
lemma Spy_not_see_encrypted_key: |
|
232 |
"[| Says Server B |
|
233 |
{|NA, Crypt (shrK A) {|NA, Key K|}, |
|
234 |
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
|
235 |
Notes Spy {|NA, NB, Key K|} \<notin> set evs; |
|
236 |
A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
237 |
==> Key K \<notin> analz (knows Spy evs)" |
|
238 |
by (blast dest: Says_Server_message_form secrecy_lemma) |
|
239 |
||
240 |
||
14225 | 241 |
subsection{*Attempting to prove stronger properties *} |
11251 | 242 |
|
14225 | 243 |
text{*Only OR1 can have caused such a part of a message to appear. The premise |
244 |
@{term "A \<noteq> B"} prevents OR2's similar-looking cryptogram from being picked |
|
245 |
up. Original Otway-Rees doesn't need it.*} |
|
11251 | 246 |
lemma Crypt_imp_OR1 [rule_format]: |
247 |
"[| A \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
248 |
==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) --> |
|
249 |
Says A B {|NA, Agent A, Agent B, |
|
250 |
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs" |
|
14225 | 251 |
by (erule otway.induct, force, |
252 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
|
11251 | 253 |
|
254 |
||
14225 | 255 |
text{*Crucial property: If the encrypted message appears, and A has used NA |
11251 | 256 |
to start a run, then it originated with the Server! |
14225 | 257 |
The premise @{term "A \<noteq> B"} allows use of @{text Crypt_imp_OR1}*} |
258 |
text{*Only it is FALSE. Somebody could make a fake message to Server |
|
259 |
substituting some other nonce NA' for NB.*} |
|
11251 | 260 |
lemma "[| A \<notin> bad; A \<noteq> B; evs \<in> otway |] |
261 |
==> Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs) --> |
|
262 |
Says A B {|NA, Agent A, Agent B, |
|
263 |
Crypt (shrK A) {|NA, Agent A, Agent B|}|} |
|
264 |
\<in> set evs --> |
|
265 |
(\<exists>B NB. Says Server B |
|
266 |
{|NA, |
|
267 |
Crypt (shrK A) {|NA, Key K|}, |
|
268 |
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)" |
|
269 |
apply (erule otway.induct, force, |
|
13507 | 270 |
drule_tac [4] OR2_parts_knows_Spy, simp_all) |
14225 | 271 |
apply blast --{*Fake*} |
272 |
apply blast --{*OR1: it cannot be a new Nonce, contradiction.*} |
|
273 |
txt{*OR3 and OR4*} |
|
11251 | 274 |
apply (simp_all add: ex_disj_distrib) |
14225 | 275 |
prefer 2 apply (blast intro!: Crypt_imp_OR1) --{*OR4*} |
276 |
txt{*OR3*} |
|
11251 | 277 |
apply clarify |
278 |
(*The hypotheses at this point suggest an attack in which nonce NB is used |
|
279 |
in two different roles: |
|
280 |
Gets Server |
|
281 |
{|Nonce NA, Agent Aa, Agent A, |
|
282 |
Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB, |
|
283 |
Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|} |
|
284 |
\<in> set evs3 |
|
285 |
Says A B |
|
286 |
{|Nonce NB, Agent A, Agent B, |
|
287 |
Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|} |
|
288 |
\<in> set evs3; |
|
289 |
*) |
|
290 |
||
291 |
||
292 |
(*Thus the key property A_can_trust probably fails too.*) |
|
293 |
oops |
|
2002 | 294 |
|
295 |
end |