author | paulson |
Tue, 23 Sep 2003 15:41:33 +0200 | |
changeset 14200 | d8598e24f8fa |
parent 13507 | febb8e5d2a9d |
child 14207 | f20fbb141673 |
permissions | -rw-r--r-- |
2090 | 1 |
(* Title: HOL/Auth/OtwayRees |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Inductive relation "otway" for the Otway-Rees protocol. |
|
7 |
||
11251 | 8 |
Abadi-Needham simplified version: minimal encryption, explicit messages |
2090 | 9 |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
10 |
Note that the formalization does not even assume that nonces are fresh. |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
11 |
This is because the protocol does not rely on uniqueness of nonces for |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
12 |
security, only for freshness, and the proof script does not prove freshness |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
13 |
properties. |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
14 |
|
2090 | 15 |
From page 11 of |
16 |
Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. |
|
17 |
IEEE Trans. SE 22 (1), 1996 |
|
18 |
*) |
|
19 |
||
11251 | 20 |
theory OtwayRees_AN = Shared: |
2090 | 21 |
|
11251 | 22 |
consts otway :: "event list set" |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset
|
23 |
inductive "otway" |
11251 | 24 |
intros |
2090 | 25 |
(*Initial trace is empty*) |
11251 | 26 |
Nil: "[] \<in> otway" |
2090 | 27 |
|
28 |
(*The spy MAY say anything he CAN say. We do not expect him to |
|
29 |
invent new nonces here, but he can also use NS1. Common to |
|
30 |
all similar protocols.*) |
|
11251 | 31 |
Fake: "[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |] |
32 |
==> Says Spy B X # evsf \<in> otway" |
|
2090 | 33 |
|
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
34 |
(*A message that has been sent can be received by the |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
35 |
intended recipient.*) |
11251 | 36 |
Reception: "[| evsr \<in> otway; Says A B X \<in>set evsr |] |
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 |
|
2090 | 39 |
(*Alice initiates a protocol run*) |
11251 | 40 |
OR1: "evs1 \<in> otway |
41 |
==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 \<in> otway" |
|
2090 | 42 |
|
6333 | 43 |
(*Bob's response to Alice's message.*) |
11251 | 44 |
OR2: "[| evs2 \<in> otway; |
45 |
Gets B {|Agent A, Agent B, Nonce NA|} \<in>set evs2 |] |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
46 |
==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
11251 | 47 |
# evs2 \<in> otway" |
2090 | 48 |
|
49 |
(*The Server receives Bob's message. Then he sends a new |
|
50 |
session key to Bob with a packet for forwarding to Alice.*) |
|
11251 | 51 |
OR3: "[| evs3 \<in> otway; Key KAB \<notin> used evs3; |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
52 |
Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|} |
11251 | 53 |
\<in>set evs3 |] |
54 |
==> Says Server B |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
55 |
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|}, |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
56 |
Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|} |
11251 | 57 |
# evs3 \<in> otway" |
2090 | 58 |
|
59 |
(*Bob receives the Server's (?) message and compares the Nonces with |
|
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
60 |
those in the message he previously sent the Server. |
11251 | 61 |
Need B \<noteq> Server because we allow messages to self.*) |
62 |
OR4: "[| evs4 \<in> otway; B \<noteq> Server; |
|
63 |
Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \<in>set evs4; |
|
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
64 |
Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|} |
11251 | 65 |
\<in>set evs4 |] |
66 |
==> Says B A X # evs4 \<in> otway" |
|
2090 | 67 |
|
2131 | 68 |
(*This message models possible leaks of session keys. The nonces |
69 |
identify the protocol run. B is not assumed to know shrK A.*) |
|
11251 | 70 |
Oops: "[| evso \<in> otway; |
71 |
Says Server B |
|
72 |
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, |
|
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2131
diff
changeset
|
73 |
Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|} |
11251 | 74 |
\<in>set evso |] |
75 |
==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway" |
|
76 |
||
77 |
||
78 |
declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
|
79 |
declare parts.Body [dest] |
|
80 |
declare analz_into_parts [dest] |
|
81 |
declare Fake_parts_insert_in_Un [dest] |
|
82 |
||
83 |
||
84 |
(*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
|
85 |
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
|
86 |
==> \<exists>evs \<in> otway. |
11251 | 87 |
Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) |
88 |
\<in> set evs" |
|
89 |
apply (intro exI bexI) |
|
90 |
apply (rule_tac [2] otway.Nil |
|
91 |
[THEN otway.OR1, THEN otway.Reception, |
|
92 |
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
|
93 |
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
|
94 |
apply (possibility, simp add: used_Cons) |
11251 | 95 |
done |
96 |
||
97 |
lemma Gets_imp_Says [dest!]: |
|
98 |
"[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs" |
|
99 |
by (erule rev_mp, erule otway.induct, auto) |
|
100 |
||
101 |
||
102 |
(**** Inductive proofs about otway ****) |
|
103 |
||
104 |
(** For reasoning about the encrypted portion of messages **) |
|
105 |
||
106 |
lemma OR4_analz_knows_Spy: |
|
107 |
"[| Gets B {|X, Crypt(shrK B) X'|} \<in> set evs; evs \<in> otway |] |
|
108 |
==> X \<in> analz (knows Spy evs)" |
|
109 |
by blast |
|
110 |
||
111 |
||
112 |
(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY |
|
113 |
sends messages containing X! **) |
|
114 |
||
115 |
(*Spy never sees a good agent's shared key!*) |
|
116 |
lemma Spy_see_shrK [simp]: |
|
117 |
"evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
|
13507 | 118 |
apply (erule otway.induct, simp_all, blast+) |
11251 | 119 |
done |
120 |
||
121 |
lemma Spy_analz_shrK [simp]: |
|
122 |
"evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
|
123 |
by auto |
|
124 |
||
125 |
lemma Spy_see_shrK_D [dest!]: |
|
126 |
"[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway|] ==> A \<in> bad" |
|
127 |
by (blast dest: Spy_see_shrK) |
|
128 |
||
129 |
||
130 |
(*** Proofs involving analz ***) |
|
131 |
||
132 |
(*Describes the form of K and NA when the Server sends this message.*) |
|
133 |
lemma Says_Server_message_form: |
|
134 |
"[| Says Server B |
|
135 |
{|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, |
|
136 |
Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} |
|
137 |
\<in> set evs; |
|
138 |
evs \<in> otway |] |
|
139 |
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)" |
|
140 |
apply (erule rev_mp) |
|
13507 | 141 |
apply (erule otway.induct, simp_all, blast) |
11251 | 142 |
done |
143 |
||
144 |
||
145 |
||
146 |
(**** |
|
147 |
The following is to prove theorems of the form |
|
148 |
||
149 |
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
|
150 |
Key K \<in> analz (knows Spy evs) |
|
151 |
||
152 |
A more general formula must be proved inductively. |
|
153 |
****) |
|
154 |
||
155 |
||
156 |
(** Session keys are not used to encrypt other session keys **) |
|
157 |
||
158 |
(*The equality makes the induction hypothesis easier to apply*) |
|
159 |
lemma analz_image_freshK [rule_format]: |
|
160 |
"evs \<in> otway ==> |
|
161 |
\<forall>K KK. KK <= -(range shrK) --> |
|
162 |
(Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
|
163 |
(K \<in> KK | Key K \<in> analz (knows Spy evs))" |
|
164 |
apply (erule otway.induct, force) |
|
165 |
apply (frule_tac [7] Says_Server_message_form) |
|
13507 | 166 |
apply (drule_tac [6] OR4_analz_knows_Spy, analz_freshK, spy_analz) |
11251 | 167 |
done |
168 |
||
169 |
lemma analz_insert_freshK: |
|
170 |
"[| evs \<in> otway; KAB \<notin> range shrK |] ==> |
|
11655 | 171 |
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
11251 | 172 |
(K = KAB | Key K \<in> analz (knows Spy evs))" |
173 |
by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
174 |
||
175 |
||
176 |
(*** The Key K uniquely identifies the Server's message. **) |
|
177 |
||
178 |
lemma unique_session_keys: |
|
179 |
"[| Says Server B |
|
180 |
{|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, |
|
181 |
Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} |
|
182 |
\<in> set evs; |
|
183 |
Says Server B' |
|
184 |
{|Crypt (shrK A') {|NA', Agent A', Agent B', K|}, |
|
185 |
Crypt (shrK B') {|NB', Agent A', Agent B', K|}|} |
|
186 |
\<in> set evs; |
|
187 |
evs \<in> otway |] |
|
188 |
==> A=A' & B=B' & NA=NA' & NB=NB'" |
|
13507 | 189 |
apply (erule rev_mp, erule rev_mp, erule otway.induct, simp_all) |
11251 | 190 |
(*Remaining cases: OR3 and OR4*) |
191 |
apply blast+ |
|
192 |
done |
|
193 |
||
194 |
||
195 |
(**** Authenticity properties relating to NA ****) |
|
196 |
||
197 |
(*If the encrypted message appears then it originated with the Server!*) |
|
198 |
lemma NA_Crypt_imp_Server_msg [rule_format]: |
|
199 |
"[| A \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
200 |
==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \<in> parts (knows Spy evs) |
|
201 |
--> (\<exists>NB. Says Server B |
|
202 |
{|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, |
|
203 |
Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} |
|
204 |
\<in> set evs)" |
|
205 |
apply (erule otway.induct, force) |
|
206 |
apply (simp_all add: ex_disj_distrib) |
|
207 |
(*Fake, OR3*) |
|
13507 | 208 |
apply blast+ |
11251 | 209 |
done |
210 |
||
211 |
||
212 |
(*Corollary: if A receives B's OR4 message then it originated with the Server. |
|
213 |
Freshness may be inferred from nonce NA.*) |
|
214 |
lemma A_trusts_OR4: |
|
215 |
"[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \<in> set evs; |
|
216 |
A \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
217 |
==> \<exists>NB. Says Server B |
|
218 |
{|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, |
|
219 |
Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} |
|
220 |
\<in> set evs" |
|
221 |
by (blast intro!: NA_Crypt_imp_Server_msg) |
|
222 |
||
223 |
||
224 |
(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
|
225 |
Does not in itself guarantee security: an attack could violate |
|
226 |
the premises, e.g. by having A=Spy **) |
|
227 |
||
228 |
lemma secrecy_lemma: |
|
229 |
"[| A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
230 |
==> Says Server B |
|
231 |
{|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, |
|
232 |
Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} |
|
233 |
\<in> set evs --> |
|
234 |
Notes Spy {|NA, NB, Key K|} \<notin> set evs --> |
|
235 |
Key K \<notin> analz (knows Spy evs)" |
|
236 |
apply (erule otway.induct, force) |
|
237 |
apply (frule_tac [7] Says_Server_message_form) |
|
238 |
apply (drule_tac [6] OR4_analz_knows_Spy) |
|
13507 | 239 |
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz) (*Fake*) |
11251 | 240 |
(*OR3, OR4, Oops*) |
241 |
apply (blast dest: unique_session_keys)+ |
|
242 |
done |
|
243 |
||
244 |
||
245 |
lemma Spy_not_see_encrypted_key: |
|
246 |
"[| Says Server B |
|
247 |
{|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, |
|
248 |
Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} |
|
249 |
\<in> set evs; |
|
250 |
Notes Spy {|NA, NB, Key K|} \<notin> set evs; |
|
251 |
A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
252 |
==> Key K \<notin> analz (knows Spy evs)" |
|
253 |
by (blast dest: Says_Server_message_form secrecy_lemma) |
|
254 |
||
255 |
||
256 |
(*A's guarantee. The Oops premise quantifies over NB because A cannot know |
|
257 |
what it is.*) |
|
258 |
lemma A_gets_good_key: |
|
259 |
"[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \<in> set evs; |
|
260 |
\<forall>NB. Notes Spy {|NA, NB, Key K|} \<notin> set evs; |
|
261 |
A \<notin> bad; B \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
262 |
==> Key K \<notin> analz (knows Spy evs)" |
|
263 |
by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key) |
|
264 |
||
265 |
||
266 |
||
267 |
(**** Authenticity properties relating to NB ****) |
|
268 |
||
269 |
(*If the encrypted message appears then it originated with the Server!*) |
|
270 |
||
271 |
lemma NB_Crypt_imp_Server_msg [rule_format]: |
|
272 |
"[| B \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
273 |
==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \<in> parts (knows Spy evs) |
|
274 |
--> (\<exists>NA. Says Server B |
|
275 |
{|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, |
|
276 |
Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} |
|
277 |
\<in> set evs)" |
|
278 |
apply (erule otway.induct, force, simp_all add: ex_disj_distrib) |
|
279 |
(*Fake, OR3*) |
|
13507 | 280 |
apply blast+ |
11251 | 281 |
done |
282 |
||
283 |
||
284 |
||
285 |
(*Guarantee for B: if it gets a well-formed certificate then the Server |
|
286 |
has sent the correct message in round 3.*) |
|
287 |
lemma B_trusts_OR3: |
|
288 |
"[| Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} |
|
289 |
\<in> set evs; |
|
290 |
B \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
291 |
==> \<exists>NA. Says Server B |
|
292 |
{|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, |
|
293 |
Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} |
|
294 |
\<in> set evs" |
|
295 |
by (blast intro!: NB_Crypt_imp_Server_msg) |
|
296 |
||
297 |
||
298 |
(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) |
|
299 |
lemma B_gets_good_key: |
|
300 |
"[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} |
|
301 |
\<in> set evs; |
|
302 |
\<forall>NA. Notes Spy {|NA, NB, Key K|} \<notin> set evs; |
|
303 |
A \<notin> bad; B \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
304 |
==> Key K \<notin> analz (knows Spy evs)" |
|
305 |
by (blast dest: B_trusts_OR3 Spy_not_see_encrypted_key) |
|
2090 | 306 |
|
307 |
end |