author | wenzelm |
Sat, 10 Nov 2018 19:01:20 +0100 | |
changeset 69281 | 599b6d0d199b |
parent 67613 | ce654b0e6d69 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/Auth/OtwayRees_AN.thy |
2090 | 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 |
*) |
2090 | 5 |
|
61830 | 6 |
section\<open>The Otway-Rees Protocol as Modified by Abadi and Needham\<close> |
2090 | 7 |
|
16417 | 8 |
theory OtwayRees_AN imports Public begin |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
9 |
|
61830 | 10 |
text\<open> |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
11 |
This simplified version has minimal encryption and explicit messages. |
2090 | 12 |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
13 |
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
|
14 |
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
|
15 |
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
|
16 |
properties. |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
17 |
|
2090 | 18 |
From page 11 of |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
19 |
Abadi and Needham (1996). |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
20 |
Prudent Engineering Practice for Cryptographic Protocols. |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
21 |
IEEE Trans. SE 22 (1) |
61830 | 22 |
\<close> |
2090 | 23 |
|
23746 | 24 |
inductive_set otway :: "event list set" |
25 |
where |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
26 |
Nil: \<comment> \<open>The empty trace\<close> |
14238 | 27 |
"[] \<in> otway" |
2090 | 28 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
29 |
| Fake: \<comment> \<open>The Spy may say anything he can say. The sender field is correct, |
61830 | 30 |
but agents don't use that information.\<close> |
14238 | 31 |
"[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |] |
11251 | 32 |
==> Says Spy B X # evsf \<in> otway" |
2090 | 33 |
|
14238 | 34 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
35 |
| Reception: \<comment> \<open>A message that has been sent can be received by the |
61830 | 36 |
intended recipient.\<close> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32366
diff
changeset
|
37 |
"[| evsr \<in> otway; Says A B X \<in>set evsr |] |
11251 | 38 |
==> 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
|
39 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
40 |
| OR1: \<comment> \<open>Alice initiates a protocol run\<close> |
14238 | 41 |
"evs1 \<in> otway |
61956 | 42 |
==> Says A B \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1 \<in> otway" |
2090 | 43 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
44 |
| OR2: \<comment> \<open>Bob's response to Alice's message.\<close> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32366
diff
changeset
|
45 |
"[| evs2 \<in> otway; |
61956 | 46 |
Gets B \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in>set evs2 |] |
47 |
==> Says B Server \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB\<rbrace> |
|
11251 | 48 |
# evs2 \<in> otway" |
2090 | 49 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
50 |
| OR3: \<comment> \<open>The Server receives Bob's message. Then he sends a new |
61830 | 51 |
session key to Bob with a packet for forwarding to Alice.\<close> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32366
diff
changeset
|
52 |
"[| evs3 \<in> otway; Key KAB \<notin> used evs3; |
61956 | 53 |
Gets Server \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB\<rbrace> |
11251 | 54 |
\<in>set evs3 |] |
55 |
==> Says Server B |
|
61956 | 56 |
\<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B, Key KAB\<rbrace>, |
57 |
Crypt (shrK B) \<lbrace>Nonce NB, Agent A, Agent B, Key KAB\<rbrace>\<rbrace> |
|
11251 | 58 |
# evs3 \<in> otway" |
2090 | 59 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
60 |
| 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:
32366
diff
changeset
|
61 |
those in the message he previously sent the Server. |
61830 | 62 |
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:
32366
diff
changeset
|
63 |
"[| evs4 \<in> otway; B \<noteq> Server; |
61956 | 64 |
Says B Server \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB\<rbrace> \<in>set evs4; |
65 |
Gets B \<lbrace>X, Crypt(shrK B)\<lbrace>Nonce NB,Agent A,Agent B,Key K\<rbrace>\<rbrace> |
|
11251 | 66 |
\<in>set evs4 |] |
67 |
==> Says B A X # evs4 \<in> otway" |
|
2090 | 68 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
69 |
| Oops: \<comment> \<open>This message models possible leaks of session keys. The nonces |
61830 | 70 |
identify the protocol run.\<close> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32366
diff
changeset
|
71 |
"[| evso \<in> otway; |
11251 | 72 |
Says Server B |
61956 | 73 |
\<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B, Key K\<rbrace>, |
74 |
Crypt (shrK B) \<lbrace>Nonce NB, Agent A, Agent B, Key K\<rbrace>\<rbrace> |
|
11251 | 75 |
\<in>set evso |] |
61956 | 76 |
==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> otway" |
11251 | 77 |
|
78 |
||
79 |
declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
|
80 |
declare parts.Body [dest] |
|
81 |
declare analz_into_parts [dest] |
|
82 |
declare Fake_parts_insert_in_Un [dest] |
|
83 |
||
84 |
||
61830 | 85 |
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
|
86 |
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
|
87 |
==> \<exists>evs \<in> otway. |
61956 | 88 |
Says B A (Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B, Key K\<rbrace>) |
11251 | 89 |
\<in> set evs" |
90 |
apply (intro exI bexI) |
|
91 |
apply (rule_tac [2] otway.Nil |
|
92 |
[THEN otway.OR1, THEN otway.Reception, |
|
93 |
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
|
94 |
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
|
95 |
apply (possibility, simp add: used_Cons) |
11251 | 96 |
done |
97 |
||
98 |
lemma Gets_imp_Says [dest!]: |
|
99 |
"[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs" |
|
100 |
by (erule rev_mp, erule otway.induct, auto) |
|
101 |
||
102 |
||
103 |
||
61830 | 104 |
text\<open>For reasoning about the encrypted portion of messages\<close> |
11251 | 105 |
|
106 |
lemma OR4_analz_knows_Spy: |
|
61956 | 107 |
"[| Gets B \<lbrace>X, Crypt(shrK B) X'\<rbrace> \<in> set evs; evs \<in> otway |] |
11251 | 108 |
==> X \<in> analz (knows Spy evs)" |
109 |
by blast |
|
110 |
||
111 |
||
61830 | 112 |
text\<open>Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that |
113 |
NOBODY sends messages containing X!\<close> |
|
11251 | 114 |
|
61830 | 115 |
text\<open>Spy never sees a good agent's shared key!\<close> |
11251 | 116 |
lemma Spy_see_shrK [simp]: |
117 |
"evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
|
14238 | 118 |
by (erule otway.induct, simp_all, blast+) |
11251 | 119 |
|
120 |
lemma Spy_analz_shrK [simp]: |
|
121 |
"evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
|
122 |
by auto |
|
123 |
||
124 |
lemma Spy_see_shrK_D [dest!]: |
|
125 |
"[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway|] ==> A \<in> bad" |
|
126 |
by (blast dest: Spy_see_shrK) |
|
127 |
||
128 |
||
61830 | 129 |
subsection\<open>Proofs involving analz\<close> |
11251 | 130 |
|
61830 | 131 |
text\<open>Describes the form of K and NA when the Server sends this message.\<close> |
11251 | 132 |
lemma Says_Server_message_form: |
133 |
"[| Says Server B |
|
61956 | 134 |
\<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>, |
135 |
Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace> |
|
11251 | 136 |
\<in> set evs; |
137 |
evs \<in> otway |] |
|
67613 | 138 |
==> K \<notin> range shrK \<and> (\<exists>i. NA = Nonce i) \<and> (\<exists>j. NB = Nonce j)" |
11251 | 139 |
apply (erule rev_mp) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
140 |
apply (erule otway.induct, auto) |
11251 | 141 |
done |
142 |
||
143 |
||
144 |
||
145 |
(**** |
|
146 |
The following is to prove theorems of the form |
|
147 |
||
148 |
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
|
149 |
Key K \<in> analz (knows Spy evs) |
|
150 |
||
151 |
A more general formula must be proved inductively. |
|
152 |
****) |
|
153 |
||
154 |
||
61830 | 155 |
text\<open>Session keys are not used to encrypt other session keys\<close> |
11251 | 156 |
|
61830 | 157 |
text\<open>The equality makes the induction hypothesis easier to apply\<close> |
11251 | 158 |
lemma analz_image_freshK [rule_format]: |
159 |
"evs \<in> otway ==> |
|
67613 | 160 |
\<forall>K KK. KK \<subseteq> -(range shrK) \<longrightarrow> |
161 |
(Key K \<in> analz (Key`KK \<union> (knows Spy evs))) = |
|
11251 | 162 |
(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
|
163 |
apply (erule otway.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
164 |
apply (frule_tac [8] Says_Server_message_form) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
165 |
apply (drule_tac [7] OR4_analz_knows_Spy, analz_freshK, spy_analz, auto) |
11251 | 166 |
done |
167 |
||
168 |
lemma analz_insert_freshK: |
|
169 |
"[| evs \<in> otway; KAB \<notin> range shrK |] ==> |
|
11655 | 170 |
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
11251 | 171 |
(K = KAB | Key K \<in> analz (knows Spy evs))" |
172 |
by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
173 |
||
174 |
||
61830 | 175 |
text\<open>The Key K uniquely identifies the Server's message.\<close> |
11251 | 176 |
lemma unique_session_keys: |
177 |
"[| Says Server B |
|
61956 | 178 |
\<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, K\<rbrace>, |
179 |
Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, K\<rbrace>\<rbrace> |
|
11251 | 180 |
\<in> set evs; |
181 |
Says Server B' |
|
61956 | 182 |
\<lbrace>Crypt (shrK A') \<lbrace>NA', Agent A', Agent B', K\<rbrace>, |
183 |
Crypt (shrK B') \<lbrace>NB', Agent A', Agent B', K\<rbrace>\<rbrace> |
|
11251 | 184 |
\<in> set evs; |
185 |
evs \<in> otway |] |
|
67613 | 186 |
==> A=A' \<and> B=B' \<and> NA=NA' \<and> NB=NB'" |
13507 | 187 |
apply (erule rev_mp, erule rev_mp, erule otway.induct, simp_all) |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
188 |
apply blast+ \<comment> \<open>OR3 and OR4\<close> |
11251 | 189 |
done |
190 |
||
191 |
||
61830 | 192 |
subsection\<open>Authenticity properties relating to NA\<close> |
11251 | 193 |
|
61830 | 194 |
text\<open>If the encrypted message appears then it originated with the Server!\<close> |
11251 | 195 |
lemma NA_Crypt_imp_Server_msg [rule_format]: |
196 |
"[| A \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
61956 | 197 |
==> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace> \<in> parts (knows Spy evs) |
67613 | 198 |
\<longrightarrow> (\<exists>NB. Says Server B |
61956 | 199 |
\<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>, |
200 |
Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace> |
|
11251 | 201 |
\<in> set evs)" |
202 |
apply (erule otway.induct, force) |
|
203 |
apply (simp_all add: ex_disj_distrib) |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
204 |
apply blast+ \<comment> \<open>Fake, OR3\<close> |
11251 | 205 |
done |
206 |
||
207 |
||
61830 | 208 |
text\<open>Corollary: if A receives B's OR4 message then it originated with the |
209 |
Server. Freshness may be inferred from nonce NA.\<close> |
|
11251 | 210 |
lemma A_trusts_OR4: |
61956 | 211 |
"[| Says B' A (Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>) \<in> set evs; |
11251 | 212 |
A \<notin> bad; A \<noteq> B; evs \<in> otway |] |
213 |
==> \<exists>NB. Says Server B |
|
61956 | 214 |
\<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>, |
215 |
Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace> |
|
11251 | 216 |
\<in> set evs" |
217 |
by (blast intro!: NA_Crypt_imp_Server_msg) |
|
218 |
||
219 |
||
61830 | 220 |
text\<open>Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
11251 | 221 |
Does not in itself guarantee security: an attack could violate |
61830 | 222 |
the premises, e.g. by having @{term "A=Spy"}\<close> |
11251 | 223 |
lemma secrecy_lemma: |
224 |
"[| A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
|
225 |
==> Says Server B |
|
61956 | 226 |
\<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>, |
227 |
Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace> |
|
67613 | 228 |
\<in> set evs \<longrightarrow> |
229 |
Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs \<longrightarrow> |
|
11251 | 230 |
Key K \<notin> analz (knows Spy evs)" |
231 |
apply (erule otway.induct, force) |
|
232 |
apply (frule_tac [7] Says_Server_message_form) |
|
233 |
apply (drule_tac [6] OR4_analz_knows_Spy) |
|
14238 | 234 |
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
235 |
apply spy_analz \<comment> \<open>Fake\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
236 |
apply (blast dest: unique_session_keys)+ \<comment> \<open>OR3, OR4, Oops\<close> |
11251 | 237 |
done |
238 |
||
239 |
||
240 |
lemma Spy_not_see_encrypted_key: |
|
241 |
"[| Says Server B |
|
61956 | 242 |
\<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>, |
243 |
Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace> |
|
11251 | 244 |
\<in> set evs; |
61956 | 245 |
Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; |
11251 | 246 |
A \<notin> bad; B \<notin> bad; evs \<in> otway |] |
247 |
==> Key K \<notin> analz (knows Spy evs)" |
|
32366
b269b56b6a14
Demonstrations of sledgehammer in protocol proofs.
paulson
parents:
23746
diff
changeset
|
248 |
by (metis secrecy_lemma) |
11251 | 249 |
|
250 |
||
61830 | 251 |
text\<open>A's guarantee. The Oops premise quantifies over NB because A cannot know |
252 |
what it is.\<close> |
|
11251 | 253 |
lemma A_gets_good_key: |
61956 | 254 |
"[| Says B' A (Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>) \<in> set evs; |
255 |
\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; |
|
11251 | 256 |
A \<notin> bad; B \<notin> bad; A \<noteq> B; evs \<in> otway |] |
257 |
==> Key K \<notin> analz (knows Spy evs)" |
|
32366
b269b56b6a14
Demonstrations of sledgehammer in protocol proofs.
paulson
parents:
23746
diff
changeset
|
258 |
by (metis A_trusts_OR4 secrecy_lemma) |
11251 | 259 |
|
260 |
||
261 |
||
61830 | 262 |
subsection\<open>Authenticity properties relating to NB\<close> |
11251 | 263 |
|
61830 | 264 |
text\<open>If the encrypted message appears then it originated with the Server!\<close> |
11251 | 265 |
lemma NB_Crypt_imp_Server_msg [rule_format]: |
266 |
"[| B \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
61956 | 267 |
==> Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace> \<in> parts (knows Spy evs) |
67613 | 268 |
\<longrightarrow> (\<exists>NA. Says Server B |
61956 | 269 |
\<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>, |
270 |
Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace> |
|
11251 | 271 |
\<in> set evs)" |
272 |
apply (erule otway.induct, force, simp_all add: ex_disj_distrib) |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
61956
diff
changeset
|
273 |
apply blast+ \<comment> \<open>Fake, OR3\<close> |
11251 | 274 |
done |
275 |
||
276 |
||
277 |
||
61830 | 278 |
text\<open>Guarantee for B: if it gets a well-formed certificate then the Server |
279 |
has sent the correct message in round 3.\<close> |
|
11251 | 280 |
lemma B_trusts_OR3: |
61956 | 281 |
"[| Says S B \<lbrace>X, Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace> |
11251 | 282 |
\<in> set evs; |
283 |
B \<notin> bad; A \<noteq> B; evs \<in> otway |] |
|
284 |
==> \<exists>NA. Says Server B |
|
61956 | 285 |
\<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>, |
286 |
Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace> |
|
11251 | 287 |
\<in> set evs" |
288 |
by (blast intro!: NB_Crypt_imp_Server_msg) |
|
289 |
||
290 |
||
61830 | 291 |
text\<open>The obvious combination of \<open>B_trusts_OR3\<close> with |
292 |
\<open>Spy_not_see_encrypted_key\<close>\<close> |
|
11251 | 293 |
lemma B_gets_good_key: |
61956 | 294 |
"[| Gets B \<lbrace>X, Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace> |
11251 | 295 |
\<in> set evs; |
61956 | 296 |
\<forall>NA. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; |
11251 | 297 |
A \<notin> bad; B \<notin> bad; A \<noteq> B; evs \<in> otway |] |
298 |
==> Key K \<notin> analz (knows Spy evs)" |
|
299 |
by (blast dest: B_trusts_OR3 Spy_not_see_encrypted_key) |
|
2090 | 300 |
|
301 |
end |