author | paulson |
Fri, 10 Oct 2003 11:13:29 +0200 | |
changeset 14225 | 6d1026266e2b |
parent 14207 | f20fbb141673 |
child 14238 | 59b02c1efd01 |
permissions | -rw-r--r-- |
11251 | 1 |
(* Title: HOL/Auth/OtwayRees |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
1941 | 5 |
*) |
6 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
7 |
header{*The Original Otway-Rees Protocol*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
8 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
9 |
theory OtwayRees = Public: |
13907 | 10 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
11 |
text{* From page 244 of |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
12 |
Burrows, Abadi and Needham (1989). A Logic of Authentication. |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
13 |
Proc. Royal Soc. 426 |
1941 | 14 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
15 |
This is the original version, which encrypts Nonce NB.*} |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
16 |
|
11251 | 17 |
consts otway :: "event list set" |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3465
diff
changeset
|
18 |
inductive "otway" |
11251 | 19 |
intros |
1941 | 20 |
(*Initial trace is empty*) |
11251 | 21 |
Nil: "[] \<in> otway" |
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
22 |
|
2032 | 23 |
(*The spy MAY say anything he CAN say. We do not expect him to |
1941 | 24 |
invent new nonces here, but he can also use NS1. Common to |
25 |
all similar protocols.*) |
|
11251 | 26 |
Fake: "[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |] |
27 |
==> Says Spy B X # evsf \<in> otway" |
|
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
28 |
|
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
29 |
(*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
|
30 |
intended recipient.*) |
11251 | 31 |
Reception: "[| evsr \<in> otway; Says A B X \<in>set evsr |] |
32 |
==> Gets B X # evsr \<in> otway" |
|
1941 | 33 |
|
34 |
(*Alice initiates a protocol run*) |
|
11251 | 35 |
OR1: "[| evs1 \<in> otway; Nonce NA \<notin> used evs1 |] |
36 |
==> Says A B {|Nonce NA, Agent A, Agent B, |
|
37 |
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} |
|
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
38 |
# evs1 : otway" |
1941 | 39 |
|
6333 | 40 |
(*Bob's response to Alice's message. Note that NB is encrypted.*) |
11251 | 41 |
OR2: "[| evs2 \<in> otway; Nonce NB \<notin> used evs2; |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
42 |
Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |] |
11251 | 43 |
==> Says B Server |
44 |
{|Nonce NA, Agent A, Agent B, X, |
|
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset
|
45 |
Crypt (shrK B) |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
46 |
{|Nonce NA, Nonce NB, Agent A, Agent B|}|} |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
47 |
# evs2 : otway" |
1941 | 48 |
|
49 |
(*The Server receives Bob's message and checks that the three NAs |
|
50 |
match. Then he sends a new session key to Bob with a packet for |
|
51 |
forwarding to Alice.*) |
|
11251 | 52 |
OR3: "[| evs3 \<in> otway; Key KAB \<notin> used evs3; |
53 |
Gets Server |
|
54 |
{|Nonce NA, Agent A, Agent B, |
|
55 |
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, |
|
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset
|
56 |
Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|} |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
57 |
: set evs3 |] |
11251 | 58 |
==> Says Server B |
59 |
{|Nonce NA, |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
60 |
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
|
61 |
Crypt (shrK B) {|Nonce NB, Key KAB|}|} |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
62 |
# evs3 : otway" |
1941 | 63 |
|
64 |
(*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
|
65 |
those in the message he previously sent the Server. |
11251 | 66 |
Need B \<noteq> Server because we allow messages to self.*) |
67 |
OR4: "[| evs4 \<in> otway; B \<noteq> Server; |
|
68 |
Says B Server {|Nonce NA, Agent A, Agent B, X', |
|
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset
|
69 |
Crypt (shrK B) |
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset
|
70 |
{|Nonce NA, Nonce NB, Agent A, Agent B|}|} |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
71 |
: set evs4; |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
72 |
Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
73 |
: set evs4 |] |
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
74 |
==> Says B A {|Nonce NA, X|} # evs4 : otway" |
1941 | 75 |
|
2135 | 76 |
(*This message models possible leaks of session keys. The nonces |
77 |
identify the protocol run.*) |
|
11251 | 78 |
Oops: "[| evso \<in> otway; |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset
|
79 |
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
80 |
: set evso |] |
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
3683
diff
changeset
|
81 |
==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway" |
1941 | 82 |
|
11251 | 83 |
|
84 |
declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
|
85 |
declare parts.Body [dest] |
|
86 |
declare analz_into_parts [dest] |
|
87 |
declare Fake_parts_insert_in_Un [dest] |
|
88 |
||
89 |
||
13907 | 90 |
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:
13907
diff
changeset
|
91 |
lemma "[| B \<noteq> Server; Key K \<notin> used [] |] |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13907
diff
changeset
|
92 |
==> \<exists>evs \<in> otway. |
11251 | 93 |
Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} |
94 |
\<in> set evs" |
|
95 |
apply (intro exI bexI) |
|
96 |
apply (rule_tac [2] otway.Nil |
|
97 |
[THEN otway.OR1, THEN otway.Reception, |
|
98 |
THEN otway.OR2, THEN otway.Reception, |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13907
diff
changeset
|
99 |
THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13907
diff
changeset
|
100 |
apply (possibility, simp add: used_Cons) |
11251 | 101 |
done |
102 |
||
103 |
lemma Gets_imp_Says [dest!]: |
|
104 |
"[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs" |
|
105 |
apply (erule rev_mp) |
|
13507 | 106 |
apply (erule otway.induct, auto) |
11251 | 107 |
done |
108 |
||
109 |
||
110 |
(** For reasoning about the encrypted portion of messages **) |
|
111 |
||
112 |
lemma OR2_analz_knows_Spy: |
|
113 |
"[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs; evs \<in> otway |] |
|
114 |
==> X \<in> analz (knows Spy evs)" |
|
115 |
by blast |
|
116 |
||
117 |
lemma OR4_analz_knows_Spy: |
|
118 |
"[| Gets B {|N, X, Crypt (shrK B) X'|} \<in> set evs; evs \<in> otway |] |
|
119 |
==> X \<in> analz (knows Spy evs)" |
|
120 |
by blast |
|
121 |
||
122 |
(*These lemmas assist simplification by removing forwarded X-variables. |
|
123 |
We can replace them by rewriting with parts_insert2 and proving using |
|
124 |
dest: parts_cut, but the proofs become more difficult.*) |
|
125 |
lemmas OR2_parts_knows_Spy = |
|
126 |
OR2_analz_knows_Spy [THEN analz_into_parts, standard] |
|
127 |
||
128 |
(*There could be OR4_parts_knows_Spy and Oops_parts_knows_Spy, but for |
|
129 |
some reason proofs work without them!*) |
|
130 |
||
131 |
||
14225 | 132 |
text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that |
133 |
NOBODY sends messages containing X! *} |
|
11251 | 134 |
|
14225 | 135 |
text{*Spy never sees a good agent's shared key!*} |
11251 | 136 |
lemma Spy_see_shrK [simp]: |
137 |
"evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
|
13907 | 138 |
by (erule otway.induct, force, |
139 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
|
140 |
||
11251 | 141 |
|
142 |
lemma Spy_analz_shrK [simp]: |
|
143 |
"evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
|
144 |
by auto |
|
145 |
||
146 |
lemma Spy_see_shrK_D [dest!]: |
|
147 |
"[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway|] ==> A \<in> bad" |
|
148 |
by (blast dest: Spy_see_shrK) |
|
149 |
||
150 |
||
13907 | 151 |
subsection{*Towards Secrecy: Proofs Involving @{term analz}*} |
11251 | 152 |
|
153 |
(*Describes the form of K and NA when the Server sends this message. Also |
|
154 |
for Oops case.*) |
|
155 |
lemma Says_Server_message_form: |
|
156 |
"[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
|
157 |
evs \<in> otway |] |
|
158 |
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)" |
|
13907 | 159 |
by (erule rev_mp, erule otway.induct, simp_all, blast) |
11251 | 160 |
|
161 |
||
162 |
(**** |
|
163 |
The following is to prove theorems of the form |
|
164 |
||
165 |
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
|
166 |
Key K \<in> analz (knows Spy evs) |
|
167 |
||
168 |
A more general formula must be proved inductively. |
|
169 |
****) |
|
170 |
||
171 |
||
13907 | 172 |
text{*Session keys are not used to encrypt other session keys*} |
11251 | 173 |
|
14225 | 174 |
text{*The equality makes the induction hypothesis easier to apply*} |
11251 | 175 |
lemma analz_image_freshK [rule_format]: |
176 |
"evs \<in> otway ==> |
|
177 |
\<forall>K KK. KK <= -(range shrK) --> |
|
178 |
(Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
|
179 |
(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
|
180 |
apply (erule otway.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
181 |
apply (frule_tac [8] Says_Server_message_form) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
182 |
apply (drule_tac [7] OR4_analz_knows_Spy) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
183 |
apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto) |
11251 | 184 |
done |
185 |
||
186 |
lemma analz_insert_freshK: |
|
187 |
"[| evs \<in> otway; KAB \<notin> range shrK |] ==> |
|
11655 | 188 |
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
11251 | 189 |
(K = KAB | Key K \<in> analz (knows Spy evs))" |
190 |
by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
191 |
||
192 |
||
14225 | 193 |
text{*The Key K uniquely identifies the Server's message. *} |
11251 | 194 |
lemma unique_session_keys: |
195 |
"[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \<in> set evs; |
|
196 |
Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs; |
|
197 |
evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'" |
|
198 |
apply (erule rev_mp) |
|
199 |
apply (erule rev_mp) |
|
200 |
apply (erule otway.induct, simp_all) |
|
14225 | 201 |
apply blast+ --{*OR3 and OR4*} |
11251 | 202 |
done |
203 |
||
204 |
||
13907 | 205 |
subsection{*Authenticity properties relating to NA*} |
11251 | 206 |
|
14225 | 207 |
text{*Only OR1 can have caused such a part of a message to appear.*} |
11251 | 208 |
lemma Crypt_imp_OR1 [rule_format]: |
209 |
"[| A \<notin> bad; evs \<in> otway |] |
|
210 |
==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) --> |
|
211 |
Says A B {|NA, Agent A, Agent B, |
|
212 |
Crypt (shrK A) {|NA, Agent A, Agent B|}|} |
|
213 |
\<in> set evs" |
|
14225 | 214 |
by (erule otway.induct, force, |
215 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
|
11251 | 216 |
|
217 |
lemma Crypt_imp_OR1_Gets: |
|
218 |
"[| Gets B {|NA, Agent A, Agent B, |
|
219 |
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs; |
|
220 |
A \<notin> bad; evs \<in> otway |] |
|
221 |
==> Says A B {|NA, Agent A, Agent B, |
|
222 |
Crypt (shrK A) {|NA, Agent A, Agent B|}|} |
|
223 |
\<in> set evs" |
|
224 |
by (blast dest: Crypt_imp_OR1) |
|
225 |
||
226 |
||
13907 | 227 |
text{*The Nonce NA uniquely identifies A's message*} |
11251 | 228 |
lemma unique_NA: |
229 |
"[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs); |
|
230 |
Crypt (shrK A) {|NA, Agent A, Agent C|} \<in> parts (knows Spy evs); |
|
231 |
evs \<in> otway; A \<notin> bad |] |
|
232 |
==> B = C" |
|
233 |
apply (erule rev_mp, erule rev_mp) |
|
234 |
apply (erule otway.induct, force, |
|
13507 | 235 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
11251 | 236 |
done |
237 |
||
238 |
||
14225 | 239 |
text{*It is impossible to re-use a nonce in both OR1 and OR2. This holds because |
11251 | 240 |
OR2 encrypts Nonce NB. It prevents the attack that can occur in the |
14225 | 241 |
over-simplified version of this protocol: see OtwayRees_Bad.*} |
11251 | 242 |
lemma no_nonce_OR1_OR2: |
243 |
"[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs); |
|
244 |
A \<notin> bad; evs \<in> otway |] |
|
245 |
==> Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \<notin> parts (knows Spy evs)" |
|
246 |
apply (erule rev_mp) |
|
247 |
apply (erule otway.induct, force, |
|
13507 | 248 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
11251 | 249 |
done |
250 |
||
14225 | 251 |
text{*Crucial property: If the encrypted message appears, and A has used NA |
252 |
to start a run, then it originated with the Server!*} |
|
11251 | 253 |
lemma NA_Crypt_imp_Server_msg [rule_format]: |
254 |
"[| A \<notin> bad; evs \<in> otway |] |
|
255 |
==> Says A B {|NA, Agent A, Agent B, |
|
256 |
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs --> |
|
257 |
Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs) |
|
258 |
--> (\<exists>NB. Says Server B |
|
259 |
{|NA, |
|
260 |
Crypt (shrK A) {|NA, Key K|}, |
|
261 |
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)" |
|
262 |
apply (erule otway.induct, force, |
|
13507 | 263 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast) |
14225 | 264 |
apply blast --{*OR1: by freshness*} |
265 |
apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA) --{*OR3*} |
|
266 |
apply (blast intro!: Crypt_imp_OR1) --{*OR4*} |
|
11251 | 267 |
done |
268 |
||
269 |
||
14225 | 270 |
text{*Corollary: if A receives B's OR4 message and the nonce NA agrees |
11251 | 271 |
then the key really did come from the Server! CANNOT prove this of the |
272 |
bad form of this protocol, even though we can prove |
|
14225 | 273 |
Spy_not_see_encrypted_key*} |
11251 | 274 |
lemma A_trusts_OR4: |
275 |
"[| Says A B {|NA, Agent A, Agent B, |
|
276 |
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs; |
|
277 |
Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs; |
|
278 |
A \<notin> bad; evs \<in> otway |] |
|
279 |
==> \<exists>NB. Says Server B |
|
280 |
{|NA, |
|
281 |
Crypt (shrK A) {|NA, Key K|}, |
|
282 |
Crypt (shrK B) {|NB, Key K|}|} |
|
283 |
\<in> set evs" |
|
284 |
by (blast intro!: NA_Crypt_imp_Server_msg) |
|
285 |
||
286 |
||
14225 | 287 |
text{*Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
11251 | 288 |
Does not in itself guarantee security: an attack could violate |
14225 | 289 |
the premises, e.g. by having @{term "A=Spy"}*} |
11251 | 290 |
lemma secrecy_lemma: |
291 |
"[| A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
292 |
==> Says Server B |
|
293 |
{|NA, Crypt (shrK A) {|NA, Key K|}, |
|
294 |
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs --> |
|
295 |
Notes Spy {|NA, NB, Key K|} \<notin> set evs --> |
|
296 |
Key K \<notin> analz (knows Spy evs)" |
|
297 |
apply (erule otway.induct, force) |
|
298 |
apply (frule_tac [7] Says_Server_message_form) |
|
299 |
apply (drule_tac [6] OR4_analz_knows_Spy) |
|
300 |
apply (drule_tac [4] OR2_analz_knows_Spy) |
|
14225 | 301 |
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) |
302 |
apply spy_analz --{*Fake*} |
|
303 |
apply (blast dest: unique_session_keys)+ --{*OR3, OR4, Oops*} |
|
11251 | 304 |
done |
305 |
||
13907 | 306 |
theorem Spy_not_see_encrypted_key: |
11251 | 307 |
"[| Says Server B |
308 |
{|NA, Crypt (shrK A) {|NA, Key K|}, |
|
309 |
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
|
310 |
Notes Spy {|NA, NB, Key K|} \<notin> set evs; |
|
311 |
A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
312 |
==> Key K \<notin> analz (knows Spy evs)" |
|
313 |
by (blast dest: Says_Server_message_form secrecy_lemma) |
|
314 |
||
13907 | 315 |
text{*This form is an immediate consequence of the previous result. It is |
316 |
similar to the assertions established by other methods. It is equivalent |
|
317 |
to the previous result in that the Spy already has @{term analz} and |
|
318 |
@{term synth} at his disposal. However, the conclusion |
|
319 |
@{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases |
|
320 |
other than Fake are trivial, while Fake requires |
|
321 |
@{term "Key K \<notin> analz (knows Spy evs)"}. *} |
|
322 |
lemma Spy_not_know_encrypted_key: |
|
323 |
"[| Says Server B |
|
324 |
{|NA, Crypt (shrK A) {|NA, Key K|}, |
|
325 |
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
|
326 |
Notes Spy {|NA, NB, Key K|} \<notin> set evs; |
|
327 |
A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
328 |
==> Key K \<notin> knows Spy evs" |
|
329 |
by (blast dest: Spy_not_see_encrypted_key) |
|
330 |
||
11251 | 331 |
|
14225 | 332 |
text{*A's guarantee. The Oops premise quantifies over NB because A cannot know |
333 |
what it is.*} |
|
11251 | 334 |
lemma A_gets_good_key: |
335 |
"[| Says A B {|NA, Agent A, Agent B, |
|
336 |
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs; |
|
337 |
Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs; |
|
338 |
\<forall>NB. Notes Spy {|NA, NB, Key K|} \<notin> set evs; |
|
339 |
A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
340 |
==> Key K \<notin> analz (knows Spy evs)" |
|
341 |
by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key) |
|
342 |
||
343 |
||
344 |
||
13907 | 345 |
subsection{*Authenticity properties relating to NB*} |
11251 | 346 |
|
14225 | 347 |
text{*Only OR2 can have caused such a part of a message to appear. We do not |
348 |
know anything about X: it does NOT have to have the right form.*} |
|
11251 | 349 |
lemma Crypt_imp_OR2: |
350 |
"[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts (knows Spy evs); |
|
351 |
B \<notin> bad; evs \<in> otway |] |
|
352 |
==> \<exists>X. Says B Server |
|
353 |
{|NA, Agent A, Agent B, X, |
|
354 |
Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} |
|
355 |
\<in> set evs" |
|
356 |
apply (erule rev_mp) |
|
357 |
apply (erule otway.induct, force, |
|
13507 | 358 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
11251 | 359 |
done |
360 |
||
361 |
||
13907 | 362 |
text{*The Nonce NB uniquely identifies B's message*} |
11251 | 363 |
lemma unique_NB: |
364 |
"[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts(knows Spy evs); |
|
365 |
Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \<in> parts(knows Spy evs); |
|
366 |
evs \<in> otway; B \<notin> bad |] |
|
367 |
==> NC = NA & C = A" |
|
368 |
apply (erule rev_mp, erule rev_mp) |
|
369 |
apply (erule otway.induct, force, |
|
370 |
drule_tac [4] OR2_parts_knows_Spy, simp_all) |
|
14225 | 371 |
apply blast+ --{*Fake, OR2*} |
11251 | 372 |
done |
373 |
||
14225 | 374 |
text{*If the encrypted message appears, and B has used Nonce NB, |
375 |
then it originated with the Server! Quite messy proof.*} |
|
11251 | 376 |
lemma NB_Crypt_imp_Server_msg [rule_format]: |
377 |
"[| B \<notin> bad; evs \<in> otway |] |
|
378 |
==> Crypt (shrK B) {|NB, Key K|} \<in> parts (knows Spy evs) |
|
379 |
--> (\<forall>X'. Says B Server |
|
380 |
{|NA, Agent A, Agent B, X', |
|
381 |
Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} |
|
382 |
\<in> set evs |
|
383 |
--> Says Server B |
|
384 |
{|NA, Crypt (shrK A) {|NA, Key K|}, |
|
385 |
Crypt (shrK B) {|NB, Key K|}|} |
|
386 |
\<in> set evs)" |
|
387 |
apply simp |
|
388 |
apply (erule otway.induct, force, |
|
14225 | 389 |
drule_tac [4] OR2_parts_knows_Spy, simp_all) |
390 |
apply blast --{*Fake*} |
|
391 |
apply blast --{*OR2*} |
|
392 |
apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2) --{*OR3*} |
|
393 |
apply (blast dest!: Crypt_imp_OR2) --{*OR4*} |
|
11251 | 394 |
done |
395 |
||
396 |
||
13907 | 397 |
text{*Guarantee for B: if it gets a message with matching NB then the Server |
398 |
has sent the correct message.*} |
|
399 |
theorem B_trusts_OR3: |
|
11251 | 400 |
"[| Says B Server {|NA, Agent A, Agent B, X', |
401 |
Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} |
|
402 |
\<in> set evs; |
|
403 |
Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
|
404 |
B \<notin> bad; evs \<in> otway |] |
|
405 |
==> Says Server B |
|
406 |
{|NA, |
|
407 |
Crypt (shrK A) {|NA, Key K|}, |
|
408 |
Crypt (shrK B) {|NB, Key K|}|} |
|
409 |
\<in> set evs" |
|
410 |
by (blast intro!: NB_Crypt_imp_Server_msg) |
|
411 |
||
412 |
||
14225 | 413 |
text{*The obvious combination of @{text B_trusts_OR3} with |
414 |
@{text Spy_not_see_encrypted_key}*} |
|
11251 | 415 |
lemma B_gets_good_key: |
416 |
"[| Says B Server {|NA, Agent A, Agent B, X', |
|
417 |
Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} |
|
418 |
\<in> set evs; |
|
419 |
Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
|
420 |
Notes Spy {|NA, NB, Key K|} \<notin> set evs; |
|
421 |
A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
422 |
==> Key K \<notin> analz (knows Spy evs)" |
|
423 |
by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key) |
|
424 |
||
425 |
||
426 |
lemma OR3_imp_OR2: |
|
427 |
"[| Says Server B |
|
428 |
{|NA, Crypt (shrK A) {|NA, Key K|}, |
|
429 |
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
|
430 |
B \<notin> bad; evs \<in> otway |] |
|
431 |
==> \<exists>X. Says B Server {|NA, Agent A, Agent B, X, |
|
432 |
Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} |
|
433 |
\<in> set evs" |
|
434 |
apply (erule rev_mp) |
|
435 |
apply (erule otway.induct, simp_all) |
|
436 |
apply (blast dest!: Crypt_imp_OR2)+ |
|
437 |
done |
|
438 |
||
439 |
||
13907 | 440 |
text{*After getting and checking OR4, agent A can trust that B has been active. |
11251 | 441 |
We could probably prove that X has the expected form, but that is not |
13907 | 442 |
strictly necessary for authentication.*} |
443 |
theorem A_auths_B: |
|
11251 | 444 |
"[| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs; |
445 |
Says A B {|NA, Agent A, Agent B, |
|
446 |
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs; |
|
447 |
A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
448 |
==> \<exists>NB X. Says B Server {|NA, Agent A, Agent B, X, |
|
449 |
Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} |
|
450 |
\<in> set evs" |
|
451 |
by (blast dest!: A_trusts_OR4 OR3_imp_OR2) |
|
452 |
||
1941 | 453 |
end |