author  wenzelm 
Tue, 19 Dec 2017 13:58:12 +0100  
changeset 67226  ec32cdaab97b 
parent 64364  464420ba7f74 
child 67443  3abf6a722518 
permissions  rwrr 
37936  1 
(* Title: HOL/Auth/Yahalom.thy 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

3 
Copyright 1996 University of Cambridge 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

4 
*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

5 

61830  6 
section\<open>The Yahalom Protocol\<close> 
13956  7 

16417  8 
theory Yahalom imports Public begin 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

9 

61830  10 
text\<open>From page 257 of 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

11 
Burrows, Abadi and Needham (1989). A Logic of Authentication. 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

12 
Proc. Royal Soc. 426 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

13 

f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

14 
This theory has the prototypical example of a secrecy relation, KeyCryptNonce. 
61830  15 
\<close> 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

16 

23746  17 
inductive_set yahalom :: "event list set" 
18 
where 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

19 
(*Initial trace is empty*) 
11251  20 
Nil: "[] \<in> yahalom" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

21 

2032  22 
(*The spy MAY say anything he CAN say. We do not expect him to 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

23 
invent new nonces here, but he can also use NS1. Common to 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

24 
all similar protocols.*) 
64364  25 
 Fake: "\<lbrakk>evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf))\<rbrakk> 
26 
\<Longrightarrow> Says Spy B X # evsf \<in> yahalom" 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

27 

6335  28 
(*A message that has been sent can be received by the 
29 
intended recipient.*) 

64364  30 
 Reception: "\<lbrakk>evsr \<in> yahalom; Says A B X \<in> set evsr\<rbrakk> 
31 
\<Longrightarrow> Gets B X # evsr \<in> yahalom" 

6335  32 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

33 
(*Alice initiates a protocol run*) 
64364  34 
 YM1: "\<lbrakk>evs1 \<in> yahalom; Nonce NA \<notin> used evs1\<rbrakk> 
35 
\<Longrightarrow> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom" 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

36 

6335  37 
(*Bob's response to Alice's message.*) 
64364  38 
 YM2: "\<lbrakk>evs2 \<in> yahalom; Nonce NB \<notin> used evs2; 
39 
Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2\<rbrakk> 

40 
\<Longrightarrow> Says B Server 

61956  41 
\<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 
11251  42 
# evs2 \<in> yahalom" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

43 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

44 
(*The Server receives Bob's message. He responds by sending a 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

45 
new session key to Alice, with a packet for forwarding to Bob.*) 
64364  46 
 YM3: "\<lbrakk>evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys; 
6335  47 
Gets Server 
61956  48 
\<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 
64364  49 
\<in> set evs3\<rbrakk> 
50 
\<Longrightarrow> Says Server A 

61956  51 
\<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA, Nonce NB\<rbrace>, 
52 
Crypt (shrK B) \<lbrace>Agent A, Key KAB\<rbrace>\<rbrace> 

11251  53 
# evs3 \<in> yahalom" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

54 

23746  55 
 YM4: 
61830  56 
\<comment>\<open>Alice receives the Server's (?) message, checks her Nonce, and 
3961  57 
uses the new session key to send Bob his Nonce. The premise 
61830  58 
@{term "A \<noteq> Server"} is needed for \<open>Says_Server_not_range\<close>. 
59 
Alice can check that K is symmetric by its length.\<close> 

64364  60 
"\<lbrakk>evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys; 
61956  61 
Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace> 
11251  62 
\<in> set evs4; 
64364  63 
Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4\<rbrakk> 
64 
\<Longrightarrow> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom" 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

65 

2110  66 
(*This message models possible leaks of session keys. The Nonces 
2156  67 
identify the protocol run. Quoting Server here ensures they are 
68 
correct.*) 

64364  69 
 Oops: "\<lbrakk>evso \<in> yahalom; 
61956  70 
Says Server A \<lbrace>Crypt (shrK A) 
71 
\<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, 

64364  72 
X\<rbrace> \<in> set evso\<rbrakk> 
73 
\<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom" 

2110  74 

3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

75 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

76 
definition KeyWithNonce :: "[key, nat, event list] => bool" where 
3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

77 
"KeyWithNonce K NB evs == 
11251  78 
\<exists>A B na X. 
61956  79 
Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace> 
11251  80 
\<in> set evs" 
81 

82 

18570  83 
declare Says_imp_analz_Spy [dest] 
11251  84 
declare parts.Body [dest] 
85 
declare Fake_parts_insert_in_Un [dest] 

86 
declare analz_into_parts [dest] 

87 

61830  88 
text\<open>A "possibility property": there are traces that reach the end\<close> 
64364  89 
lemma "\<lbrakk>A \<noteq> Server; K \<in> symKeys; Key K \<notin> used []\<rbrakk> 
90 
\<Longrightarrow> \<exists>X NB. \<exists>evs \<in> yahalom. 

61956  91 
Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" 
11251  92 
apply (intro exI bexI) 
93 
apply (rule_tac [2] yahalom.Nil 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

94 
[THEN yahalom.YM1, THEN yahalom.Reception, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

95 
THEN yahalom.YM2, THEN yahalom.Reception, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

96 
THEN yahalom.YM3, THEN yahalom.Reception, 
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset

97 
THEN yahalom.YM4]) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

98 
apply (possibility, simp add: used_Cons) 
11251  99 
done 
100 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

101 

61830  102 
subsection\<open>Regularity Lemmas for Yahalom\<close> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

103 

11251  104 
lemma Gets_imp_Says: 
64364  105 
"\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs" 
11251  106 
by (erule rev_mp, erule yahalom.induct, auto) 
107 

61830  108 
text\<open>Must be proved separately for each protocol\<close> 
11251  109 
lemma Gets_imp_knows_Spy: 
64364  110 
"\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk> \<Longrightarrow> X \<in> knows Spy evs" 
11251  111 
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 
112 

18570  113 
lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj] 
114 
declare Gets_imp_analz_Spy [dest] 

11251  115 

116 

61830  117 
text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close> 
11251  118 
lemma YM4_analz_knows_Spy: 
64364  119 
"\<lbrakk>Gets A \<lbrace>Crypt (shrK A) Y, X\<rbrace> \<in> set evs; evs \<in> yahalom\<rbrakk> 
120 
\<Longrightarrow> X \<in> analz (knows Spy evs)" 

11251  121 
by blast 
122 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

123 
lemmas YM4_parts_knows_Spy = 
45605  124 
YM4_analz_knows_Spy [THEN analz_into_parts] 
11251  125 

61830  126 
text\<open>For Oops\<close> 
11251  127 
lemma YM4_Key_parts_knows_Spy: 
61956  128 
"Says Server A \<lbrace>Crypt (shrK A) \<lbrace>B,K,NA,NB\<rbrace>, X\<rbrace> \<in> set evs 
64364  129 
\<Longrightarrow> K \<in> parts (knows Spy evs)" 
32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

130 
by (metis parts.Body parts.Fst parts.Snd Says_imp_knows_Spy parts.Inj) 
11251  131 

61830  132 
text\<open>Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply 
133 
that NOBODY sends messages containing X!\<close> 

11251  134 

61830  135 
text\<open>Spy never sees a good agent's shared key!\<close> 
11251  136 
lemma Spy_see_shrK [simp]: 
64364  137 
"evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

138 
by (erule yahalom.induct, force, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

139 
drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) 
11251  140 

141 
lemma Spy_analz_shrK [simp]: 

64364  142 
"evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" 
11251  143 
by auto 
144 

145 
lemma Spy_see_shrK_D [dest!]: 

64364  146 
"\<lbrakk>Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom\<rbrakk> \<Longrightarrow> A \<in> bad" 
11251  147 
by (blast dest: Spy_see_shrK) 
148 

61830  149 
text\<open>Nobody can have used nonexistent keys! 
150 
Needed to apply \<open>analz_insert_Key\<close>\<close> 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

151 
lemma new_keys_not_used [simp]: 
64364  152 
"\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom\<rbrakk> 
153 
\<Longrightarrow> K \<notin> keysFor (parts (spies evs))" 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

154 
apply (erule rev_mp) 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

155 
apply (erule yahalom.induct, force, 
11251  156 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 
61830  157 
txt\<open>Fake\<close> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

158 
apply (force dest!: keysFor_parts_insert, auto) 
11251  159 
done 
160 

161 

61830  162 
text\<open>Earlier, all protocol proofs declared this theorem. 
163 
But only a few proofs need it, e.g. Yahalom and Kerberos IV.\<close> 

11251  164 
lemma new_keys_not_analzd: 
64364  165 
"\<lbrakk>K \<in> symKeys; evs \<in> yahalom; Key K \<notin> used evs\<rbrakk> 
166 
\<Longrightarrow> K \<notin> keysFor (analz (knows Spy evs))" 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

167 
by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD]) 
11251  168 

169 

61830  170 
text\<open>Describes the form of K when the Server sends this message. Useful for 
171 
Oops as well as main secrecy property.\<close> 

11251  172 
lemma Says_Server_not_range [simp]: 
64364  173 
"\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> 
174 
\<in> set evs; evs \<in> yahalom\<rbrakk> 

175 
\<Longrightarrow> K \<notin> range shrK" 

17778  176 
by (erule rev_mp, erule yahalom.induct, simp_all) 
11251  177 

178 

61830  179 
subsection\<open>Secrecy Theorems\<close> 
11251  180 

181 
(**** 

182 
The following is to prove theorems of the form 

183 

64364  184 
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow> 
11251  185 
Key K \<in> analz (knows Spy evs) 
186 

187 
A more general formula must be proved inductively. 

188 
****) 

189 

61830  190 
text\<open>Session keys are not used to encrypt other session keys\<close> 
11251  191 

192 
lemma analz_image_freshK [rule_format]: 

64364  193 
"evs \<in> yahalom \<Longrightarrow> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

194 
\<forall>K KK. KK <=  (range shrK) > 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

195 
(Key K \<in> analz (Key`KK Un (knows Spy evs))) = 
11251  196 
(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

197 
apply (erule yahalom.induct, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

198 
drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) 
11251  199 
apply (simp only: Says_Server_not_range analz_image_freshK_simps) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
37936
diff
changeset

200 
apply safe 
11251  201 
done 
202 

203 
lemma analz_insert_freshK: 

64364  204 
"\<lbrakk>evs \<in> yahalom; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow> 
11655  205 
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = 
11251  206 
(K = KAB  Key K \<in> analz (knows Spy evs))" 
207 
by (simp only: analz_image_freshK analz_image_freshK_simps) 

208 

209 

61830  210 
text\<open>The Key K uniquely identifies the Server's message.\<close> 
11251  211 
lemma unique_session_keys: 
64364  212 
"\<lbrakk>Says Server A 
61956  213 
\<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> \<in> set evs; 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

214 
Says Server A' 
61956  215 
\<lbrace>Crypt (shrK A') \<lbrace>Agent B', Key K, na', nb'\<rbrace>, X'\<rbrace> \<in> set evs; 
64364  216 
evs \<in> yahalom\<rbrakk> 
217 
\<Longrightarrow> A=A' & B=B' & na=na' & nb=nb'" 

11251  218 
apply (erule rev_mp, erule rev_mp) 
219 
apply (erule yahalom.induct, simp_all) 

61830  220 
txt\<open>YM3, by freshness, and YM4\<close> 
11251  221 
apply blast+ 
222 
done 

223 

224 

61830  225 
text\<open>Crucial secrecy property: Spy does not see the keys sent in msg YM3\<close> 
11251  226 
lemma secrecy_lemma: 
64364  227 
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
228 
\<Longrightarrow> Says Server A 

61956  229 
\<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, 
230 
Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

231 
\<in> set evs > 
61956  232 
Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs > 
11251  233 
Key K \<notin> analz (knows Spy evs)" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

234 
apply (erule yahalom.induct, force, 
11251  235 
drule_tac [6] YM4_analz_knows_Spy) 
64364  236 
apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) 
67226  237 
subgoal \<comment>\<open>Fake\<close> by spy_analz 
238 
subgoal \<comment>\<open>YM3\<close> by blast 

239 
subgoal \<comment>\<open>Oops\<close> by (blast dest: unique_session_keys) 

11251  240 
done 
241 

61830  242 
text\<open>Final version\<close> 
11251  243 
lemma Spy_not_see_encrypted_key: 
64364  244 
"\<lbrakk>Says Server A 
61956  245 
\<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, 
246 
Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

247 
\<in> set evs; 
61956  248 
Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 
64364  249 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
250 
\<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 

11251  251 
by (blast dest: secrecy_lemma) 
252 

253 

61830  254 
subsubsection\<open>Security Guarantee for A upon receiving YM3\<close> 
11251  255 

61830  256 
text\<open>If the encrypted message appears then it originated with the Server\<close> 
11251  257 
lemma A_trusts_YM3: 
64364  258 
"\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs); 
259 
A \<notin> bad; evs \<in> yahalom\<rbrakk> 

260 
\<Longrightarrow> Says Server A 

61956  261 
\<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, 
262 
Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 

11251  263 
\<in> set evs" 
264 
apply (erule rev_mp) 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

265 
apply (erule yahalom.induct, force, 
11251  266 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 
61830  267 
txt\<open>Fake, YM3\<close> 
11251  268 
apply blast+ 
269 
done 

270 

61830  271 
text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with 
272 
\<open>Spy_not_see_encrypted_key\<close>\<close> 

11251  273 
lemma A_gets_good_key: 
64364  274 
"\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs); 
61956  275 
Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 
64364  276 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
277 
\<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 

32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

278 
by (metis A_trusts_YM3 secrecy_lemma) 
11251  279 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

280 

61830  281 
subsubsection\<open>Security Guarantees for B upon receiving YM4\<close> 
11251  282 

61830  283 
text\<open>B knows, by the first part of A's message, that the Server distributed 
284 
the key for A and B. But this part says nothing about nonces.\<close> 

11251  285 
lemma B_trusts_YM4_shrK: 
64364  286 
"\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs); 
287 
B \<notin> bad; evs \<in> yahalom\<rbrakk> 

288 
\<Longrightarrow> \<exists>NA NB. Says Server A 

61956  289 
\<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, 
290 
Nonce NA, Nonce NB\<rbrace>, 

291 
Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 

11251  292 
\<in> set evs" 
293 
apply (erule rev_mp) 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

294 
apply (erule yahalom.induct, force, 
11251  295 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 
61830  296 
txt\<open>Fake, YM3\<close> 
11251  297 
apply blast+ 
298 
done 

299 

61830  300 
text\<open>B knows, by the second part of A's message, that the Server 
17411  301 
distributed the key quoting nonce NB. This part says nothing about 
302 
agent names. Secrecy of NB is crucial. Note that @{term "Nonce NB 

303 
\<notin> analz(knows Spy evs)"} must be the FIRST antecedent of the 

61830  304 
induction formula.\<close> 
17411  305 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

306 
lemma B_trusts_YM4_newK [rule_format]: 
64364  307 
"\<lbrakk>Crypt K (Nonce NB) \<in> parts (knows Spy evs); 
308 
Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom\<rbrakk> 

309 
\<Longrightarrow> \<exists>A B NA. Says Server A 

61956  310 
\<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, 
311 
Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 

11251  312 
\<in> set evs" 
313 
apply (erule rev_mp, erule rev_mp) 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

314 
apply (erule yahalom.induct, force, 
11251  315 
frule_tac [6] YM4_parts_knows_Spy) 
64364  316 
apply (analz_mono_contra, simp_all) 
67226  317 
subgoal \<comment>\<open>Fake\<close> by blast 
318 
subgoal \<comment>\<open>YM3\<close> by blast 

61830  319 
txt\<open>YM4. A is uncompromised because NB is secure 
320 
A's certificate guarantees the existence of the Server message\<close> 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

321 
apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

322 
dest: Says_imp_spies 
11251  323 
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) 
324 
done 

325 

326 

61830  327 
subsubsection\<open>Towards proving secrecy of Nonce NB\<close> 
11251  328 

61830  329 
text\<open>Lemmas about the predicate KeyWithNonce\<close> 
11251  330 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

331 
lemma KeyWithNonceI: 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

332 
"Says Server A 
61956  333 
\<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace> 
64364  334 
\<in> set evs \<Longrightarrow> KeyWithNonce K NB evs" 
11251  335 
by (unfold KeyWithNonce_def, blast) 
336 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

337 
lemma KeyWithNonce_Says [simp]: 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

338 
"KeyWithNonce K NB (Says S A X # evs) = 
11251  339 
(Server = S & 
61956  340 
(\<exists>B n X'. X = \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, n, Nonce NB\<rbrace>, X'\<rbrace>) 
11251  341 
 KeyWithNonce K NB evs)" 
342 
by (simp add: KeyWithNonce_def, blast) 

343 

344 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

345 
lemma KeyWithNonce_Notes [simp]: 
11251  346 
"KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs" 
347 
by (simp add: KeyWithNonce_def) 

348 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

349 
lemma KeyWithNonce_Gets [simp]: 
11251  350 
"KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs" 
351 
by (simp add: KeyWithNonce_def) 

352 

61830  353 
text\<open>A fresh key cannot be associated with any nonce 
354 
(with respect to a given trace).\<close> 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

355 
lemma fresh_not_KeyWithNonce: 
64364  356 
"Key K \<notin> used evs \<Longrightarrow> ~ KeyWithNonce K NB evs" 
11251  357 
by (unfold KeyWithNonce_def, blast) 
358 

61830  359 
text\<open>The Server message associates K with NB' and therefore not with any 
360 
other nonce NB.\<close> 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

361 
lemma Says_Server_KeyWithNonce: 
64364  362 
"\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB'\<rbrace>, X\<rbrace> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

363 
\<in> set evs; 
64364  364 
NB \<noteq> NB'; evs \<in> yahalom\<rbrakk> 
365 
\<Longrightarrow> ~ KeyWithNonce K NB evs" 

11251  366 
by (unfold KeyWithNonce_def, blast dest: unique_session_keys) 
367 

368 

61830  369 
text\<open>The only nonces that can be found with the help of session keys are 
11251  370 
those distributed as nonce NB by the Server. The form of the theorem 
61830  371 
recalls \<open>analz_image_freshK\<close>, but it is much more complicated.\<close> 
11251  372 

373 

61830  374 
text\<open>As with \<open>analz_image_freshK\<close>, we take some pains to express the 
375 
property as a logical equivalence so that the simplifier can apply it.\<close> 

11251  376 
lemma Nonce_secrecy_lemma: 
64364  377 
"P > (X \<in> analz (G Un H)) > (X \<in> analz H) \<Longrightarrow> 
11251  378 
P > (X \<in> analz (G Un H)) = (X \<in> analz H)" 
379 
by (blast intro: analz_mono [THEN subsetD]) 

380 

381 
lemma Nonce_secrecy: 

64364  382 
"evs \<in> yahalom \<Longrightarrow> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

383 
(\<forall>KK. KK <=  (range shrK) > 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

384 
(\<forall>K \<in> KK. K \<in> symKeys > ~ KeyWithNonce K NB evs) > 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

385 
(Nonce NB \<in> analz (Key`KK Un (knows Spy evs))) = 
11251  386 
(Nonce NB \<in> analz (knows Spy evs)))" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

387 
apply (erule yahalom.induct, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

388 
frule_tac [7] YM4_analz_knows_Spy) 
11251  389 
apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI]) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

390 
apply (simp_all del: image_insert image_Un 
11251  391 
add: analz_image_freshK_simps split_ifs 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

392 
all_conj_distrib ball_conj_distrib 
11251  393 
analz_image_freshK fresh_not_KeyWithNonce 
394 
imp_disj_not1 (*Moves NBa\<noteq>NB to the front*) 

395 
Says_Server_KeyWithNonce) 

61830  396 
txt\<open>For Oops, simplification proves @{prop "NBa\<noteq>NB"}. By 
17411  397 
@{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB 
398 
evs"}; then simplification can apply the induction hypothesis with 

61830  399 
@{term "KK = {K}"}.\<close> 
67226  400 
subgoal \<comment>\<open>Fake\<close> by spy_analz 
401 
subgoal \<comment>\<open>YM2\<close> by blast 

402 
subgoal \<comment>\<open>YM3\<close> by blast 

403 
subgoal \<comment>\<open>YM4: If @{prop "A \<in> bad"} then @{term NBa} is known, therefore @{prop "NBa \<noteq> NB"}.\<close> 

64364  404 
by (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def 
405 
Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj) 

11251  406 
done 
407 

408 

61830  409 
text\<open>Version required below: if NB can be decrypted using a session key then 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

410 
it was distributed with that key. The more general form above is required 
61830  411 
for the induction to carry through.\<close> 
11251  412 
lemma single_Nonce_secrecy: 
64364  413 
"\<lbrakk>Says Server A 
61956  414 
\<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, na, Nonce NB'\<rbrace>, X\<rbrace> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

415 
\<in> set evs; 
64364  416 
NB \<noteq> NB'; KAB \<notin> range shrK; evs \<in> yahalom\<rbrakk> 
417 
\<Longrightarrow> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) = 

11251  418 
(Nonce NB \<in> analz (knows Spy evs))" 
419 
by (simp_all del: image_insert image_Un imp_disjL 

420 
add: analz_image_freshK_simps split_ifs 

13507  421 
Nonce_secrecy Says_Server_KeyWithNonce) 
11251  422 

423 

61830  424 
subsubsection\<open>The Nonce NB uniquely identifies B's message.\<close> 
11251  425 

426 
lemma unique_NB: 

64364  427 
"\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs); 
61956  428 
Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace> \<in> parts (knows Spy evs); 
64364  429 
evs \<in> yahalom; B \<notin> bad; B' \<notin> bad\<rbrakk> 
430 
\<Longrightarrow> NA' = NA & A' = A & B' = B" 

11251  431 
apply (erule rev_mp, erule rev_mp) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

432 
apply (erule yahalom.induct, force, 
11251  433 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 
61830  434 
txt\<open>Fake, and YM2 by freshness\<close> 
11251  435 
apply blast+ 
436 
done 

437 

438 

61830  439 
text\<open>Variant useful for proving secrecy of NB. Because nb is assumed to be 
440 
secret, we no longer must assume B, B' not bad.\<close> 

11251  441 
lemma Says_unique_NB: 
64364  442 
"\<lbrakk>Says C S \<lbrace>X, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

443 
\<in> set evs; 
61956  444 
Gets S' \<lbrace>X', Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace>\<rbrace> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

445 
\<in> set evs; 
64364  446 
nb \<notin> analz (knows Spy evs); evs \<in> yahalom\<rbrakk> 
447 
\<Longrightarrow> NA' = NA & A' = A & B' = B" 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

448 
by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad 
11251  449 
dest: Says_imp_spies unique_NB parts.Inj analz.Inj) 
450 

451 

61830  452 
subsubsection\<open>A nonce value is never used both as NA and as NB\<close> 
11251  453 

454 
lemma no_nonce_YM1_YM2: 

64364  455 
"\<lbrakk>Crypt (shrK B') \<lbrace>Agent A', Nonce NB, nb'\<rbrace> \<in> parts(knows Spy evs); 
456 
Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom\<rbrakk> 

457 
\<Longrightarrow> Crypt (shrK B) \<lbrace>Agent A, na, Nonce NB\<rbrace> \<notin> parts(knows Spy evs)" 

11251  458 
apply (erule rev_mp, erule rev_mp) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

459 
apply (erule yahalom.induct, force, 
11251  460 
frule_tac [6] YM4_parts_knows_Spy) 
461 
apply (analz_mono_contra, simp_all) 

61830  462 
txt\<open>Fake, YM2\<close> 
11251  463 
apply blast+ 
464 
done 

465 

61830  466 
text\<open>The Server sends YM3 only in response to YM2.\<close> 
11251  467 
lemma Says_Server_imp_YM2: 
64364  468 
"\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, k, na, nb\<rbrace>, X\<rbrace> \<in> set evs; 
469 
evs \<in> yahalom\<rbrakk> 

470 
\<Longrightarrow> Gets Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, na, nb\<rbrace>\<rbrace> 

11251  471 
\<in> set evs" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

472 
by (erule rev_mp, erule yahalom.induct, auto) 
11251  473 

61830  474 
text\<open>A vital theorem for B, that nonce NB remains secure from the Spy.\<close> 
64364  475 
theorem Spy_not_see_NB : 
476 
"\<lbrakk>Says B Server 

61956  477 
\<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32377
diff
changeset

478 
\<in> set evs; 
61956  479 
(\<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs); 
64364  480 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
481 
\<Longrightarrow> Nonce NB \<notin> analz (knows Spy evs)" 

11251  482 
apply (erule rev_mp, erule rev_mp) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

483 
apply (erule yahalom.induct, force, 
11251  484 
frule_tac [6] YM4_analz_knows_Spy) 
485 
apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq 

486 
analz_insert_freshK) 

67226  487 
subgoal \<comment>\<open>Fake\<close> by spy_analz 
488 
subgoal \<comment>\<open>YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!\<close> by blast 

489 
subgoal \<comment>\<open>YM2\<close> by blast 

490 
subgoal \<comment>\<open>YM3: because no NB can also be an NA\<close> 

64364  491 
by (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB) 
67226  492 
subgoal \<comment>\<open>YM4: key K is visible to Spy, contradicting session key secrecy theorem\<close> 
493 
\<comment>\<open>Case analysis on whether Aa is bad; 

64364  494 
use \<open>Says_unique_NB\<close> to identify message components: @{term "Aa=A"}, @{term "Ba=B"}\<close> 
495 
apply clarify 

496 
apply (blast dest!: Says_unique_NB analz_shrK_Decrypt 

497 
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3] 

498 
dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2 

499 
Spy_not_see_encrypted_key) 

500 
done 

67226  501 
subgoal \<comment>\<open>Oops case: if the nonce is betrayed now, show that the Oops event is 
64364  502 
covered by the quantified Oops assumption.\<close> 
503 
apply clarsimp 

504 
apply (metis Says_Server_imp_YM2 Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1)) 

505 
done 

11251  506 
done 
507 

61830  508 
text\<open>B's session key guarantee from YM4. The two certificates contribute to a 
11251  509 
single conclusion about the Server's message. Note that the "Notes Spy" 
61830  510 
assumption must quantify over \<open>\<forall>\<close> POSSIBLE keys instead of our particular K. 
11251  511 
If this run is broken and the spy substitutes a certificate containing an 
61830  512 
old key, B has no means of telling.\<close> 
11251  513 
lemma B_trusts_YM4: 
64364  514 
"\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, 
61956  515 
Crypt K (Nonce NB)\<rbrace> \<in> set evs; 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

516 
Says B Server 
61956  517 
\<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

518 
\<in> set evs; 
61956  519 
\<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs; 
64364  520 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
521 
\<Longrightarrow> Says Server A 

61956  522 
\<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, 
523 
Nonce NA, Nonce NB\<rbrace>, 

524 
Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 

11251  525 
\<in> set evs" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

526 
by (blast dest: Spy_not_see_NB Says_unique_NB 
11251  527 
Says_Server_imp_YM2 B_trusts_YM4_newK) 
528 

529 

530 

61830  531 
text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with 
532 
\<open>Spy_not_see_encrypted_key\<close>\<close> 

11251  533 
lemma B_gets_good_key: 
64364  534 
"\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, 
61956  535 
Crypt K (Nonce NB)\<rbrace> \<in> set evs; 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

536 
Says B Server 
61956  537 
\<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

538 
\<in> set evs; 
61956  539 
\<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs; 
64364  540 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
541 
\<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 

32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

542 
by (metis B_trusts_YM4 Spy_not_see_encrypted_key) 
11251  543 

544 

61830  545 
subsection\<open>Authenticating B to A\<close> 
11251  546 

61830  547 
text\<open>The encryption in message YM2 tells us it cannot be faked.\<close> 
11251  548 
lemma B_Said_YM2 [rule_format]: 
64364  549 
"\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs); 
550 
evs \<in> yahalom\<rbrakk> 

551 
\<Longrightarrow> B \<notin> bad > 

61956  552 
Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> 
11251  553 
\<in> set evs" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

554 
apply (erule rev_mp, erule yahalom.induct, force, 
11251  555 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 
61830  556 
txt\<open>Fake\<close> 
11251  557 
apply blast 
558 
done 

559 

61830  560 
text\<open>If the server sends YM3 then B sent YM2\<close> 
11251  561 
lemma YM3_auth_B_to_A_lemma: 
64364  562 
"\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace> 
563 
\<in> set evs; evs \<in> yahalom\<rbrakk> 

564 
\<Longrightarrow> B \<notin> bad > 

61956  565 
Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> 
11251  566 
\<in> set evs" 
567 
apply (erule rev_mp, erule yahalom.induct, simp_all) 

61830  568 
txt\<open>YM3, YM4\<close> 
11251  569 
apply (blast dest!: B_Said_YM2)+ 
570 
done 

571 

61830  572 
text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close> 
64364  573 
theorem YM3_auth_B_to_A: 
574 
"\<lbrakk>Gets A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace> 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

575 
\<in> set evs; 
64364  576 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
577 
\<Longrightarrow> Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace> 

11251  578 
\<in> set evs" 
32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

579 
by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst 
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

580 
not_parts_not_analz) 
11251  581 

582 

61830  583 
subsection\<open>Authenticating A to B using the certificate 
584 
@{term "Crypt K (Nonce NB)"}\<close> 

11251  585 

61830  586 
text\<open>Assuming the session key is secure, if both certificates are present then 
11251  587 
A has said NB. We can't be sure about the rest of A's message, but only 
61830  588 
NB matters for freshness.\<close> 
64364  589 
theorem A_Said_YM3_lemma [rule_format]: 
11251  590 
"evs \<in> yahalom 
64364  591 
\<Longrightarrow> Key K \<notin> analz (knows Spy evs) > 
11251  592 
Crypt K (Nonce NB) \<in> parts (knows Spy evs) > 
61956  593 
Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs) > 
11251  594 
B \<notin> bad > 
61956  595 
(\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

596 
apply (erule yahalom.induct, force, 
11251  597 
frule_tac [6] YM4_parts_knows_Spy) 
598 
apply (analz_mono_contra, simp_all) 

67226  599 
subgoal \<comment>\<open>Fake\<close> by blast 
600 
subgoal \<comment>\<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close> 

64364  601 
by (force dest!: Crypt_imp_keysFor) 
67226  602 
subgoal \<comment>\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis, 
64364  603 
otherwise by unicity of session keys\<close> 
604 
by (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK Crypt_Spy_analz_bad 

11251  605 
dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) 
606 
done 

607 

61830  608 
text\<open>If B receives YM4 then A has used nonce NB (and therefore is alive). 
11251  609 
Moreover, A associates K with NB (thus is talking about the same run). 
61830  610 
Other premises guarantee secrecy of K.\<close> 
64364  611 
theorem YM4_imp_A_Said_YM3 [rule_format]: 
612 
"\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, 

61956  613 
Crypt K (Nonce NB)\<rbrace> \<in> set evs; 
11251  614 
Says B Server 
61956  615 
\<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace> 
11251  616 
\<in> set evs; 
61956  617 
(\<forall>NA k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs); 
64364  618 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
619 
\<Longrightarrow> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" 

32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

620 
by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz) 
64364  621 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

622 
end 