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