1.1 --- a/src/HOL/Auth/Yahalom2.ML Fri Nov 01 18:27:38 1996 +0100
1.2 +++ b/src/HOL/Auth/Yahalom2.ML Fri Nov 01 18:28:19 1996 +0100
1.3 @@ -63,7 +63,7 @@
1.4 bind_thm ("YM4_parts_sees_Spy",
1.5 YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
1.6
1.7 -(*Relates to both YM4 and Revl*)
1.8 +(*Relates to both YM4 and Oops*)
1.9 goal thy "!!evs. Says S A {|NB, Crypt {|B, K, NA|} (shrK A), X|} \
1.10 \ : set_of_list evs ==> \
1.11 \ K : parts (sees lost Spy evs)";
1.12 @@ -169,7 +169,6 @@
1.13 \ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
1.14 by (parts_induct_tac 1);
1.15 by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
1.16 -
1.17 (*YM1, YM2 and YM3*)
1.18 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
1.19 (*Fake and YM4: these messages send unknown (X) components*)
1.20 @@ -200,40 +199,25 @@
1.21 Addsimps [new_keys_not_used, new_keys_not_analzd];
1.22
1.23
1.24 -(*Describes the form of Key K when the following message is sent. The use of
1.25 - "parts" strengthens the induction hyp for proving the Fake case. The
1.26 - assumption A ~: lost prevents its being a Faked message. (Based
1.27 - on NS_Shared/Says_S_message_form) *)
1.28 -goal thy
1.29 - "!!evs. evs: yahalom lost ==> \
1.30 -\ Crypt {|B, Key K, NA|} (shrK A) : parts (sees lost Spy evs) \
1.31 -\ --> A ~: lost --> (EX evt: yahalom lost. K = newK evt)";
1.32 -by (parts_induct_tac 1);
1.33 -by (Auto_tac());
1.34 -qed_spec_mp "Reveal_message_lemma";
1.35 -
1.36 -(*EITHER describes the form of Key K when the following message is sent,
1.37 - OR reduces it to the Fake case.*)
1.38 -
1.39 +(*Describes the form of K when the Server sends this message. Useful for
1.40 + Oops as well as main secrecy property.*)
1.41 goal thy
1.42 - "!!evs. [| Says S A {|NB, Crypt {|B, Key K, NA|} (shrK A), X|} \
1.43 -\ : set_of_list evs; \
1.44 -\ evs : yahalom lost |] \
1.45 -\ ==> (EX evt: yahalom lost. K = newK evt) \
1.46 -\ | Key K : analz (sees lost Spy evs)";
1.47 -br (Reveal_message_lemma RS disjCI) 1;
1.48 -ba 1;
1.49 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
1.50 - addDs [impOfSubs analz_subset_parts]) 1);
1.51 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
1.52 - addss (!simpset)) 1);
1.53 -qed "Reveal_message_form";
1.54 + "!!evs. [| Says Server A {|NB', Crypt {|Agent B, K, NA|} (shrK A), X|} \
1.55 +\ : set_of_list evs; \
1.56 +\ evs : yahalom lost |] \
1.57 +\ ==> (EX evt: yahalom lost. K = Key(newK evt)) & A ~= B";
1.58 +by (etac rev_mp 1);
1.59 +by (etac yahalom.induct 1);
1.60 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
1.61 +qed "Says_Server_message_form";
1.62
1.63
1.64 (*For proofs involving analz. We again instantiate the variable to "lost".*)
1.65 val analz_Fake_tac =
1.66 dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
1.67 - forw_inst_tac [("lost","lost")] Reveal_message_form 7;
1.68 + forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
1.69 + assume_tac 7 THEN Full_simp_tac 7 THEN
1.70 + REPEAT ((eresolve_tac [bexE,conjE] ORELSE' hyp_subst_tac) 7);
1.71
1.72
1.73 (****
1.74 @@ -255,16 +239,14 @@
1.75 by (etac yahalom.induct 1);
1.76 by analz_Fake_tac;
1.77 by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
1.78 -by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 8));
1.79 by (ALLGOALS (*Takes 26 secs*)
1.80 (asm_simp_tac
1.81 (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
1.82 @ pushes)
1.83 setloop split_tac [expand_if])));
1.84 -(** LEVEL 5 **)
1.85 -(*Reveal case 2, YM4, Fake*)
1.86 -by (EVERY (map spy_analz_tac [6, 4, 2]));
1.87 -(*Reveal case 1, YM3, Base*)
1.88 +(*YM4, Fake*)
1.89 +by (EVERY (map spy_analz_tac [4, 2]));
1.90 +(*Oops, YM3, Base*)
1.91 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
1.92 qed_spec_mp "analz_image_newK";
1.93
1.94 @@ -282,11 +264,10 @@
1.95
1.96 goal thy
1.97 "!!evs. evs : yahalom lost ==> \
1.98 -\ EX A' B' NA' NB'. ALL A B NA NB. \
1.99 +\ EX A' B' NA' NB' X'. ALL A B NA NB X. \
1.100 \ Says Server A \
1.101 -\ {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), \
1.102 -\ Crypt {|Agent A, Key K, NB, NB|} (shrK B)|} \
1.103 -\ : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB'";
1.104 +\ {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|} \
1.105 +\ : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
1.106 by (etac yahalom.induct 1);
1.107 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
1.108 by (Step_tac 1);
1.109 @@ -301,12 +282,10 @@
1.110
1.111 goal thy
1.112 "!!evs. [| Says Server A \
1.113 -\ {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), \
1.114 -\ Crypt {|Agent A, Key K, NB, NB|} (shrK B)|} \
1.115 +\ {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|} \
1.116 \ : set_of_list evs; \
1.117 \ Says Server A' \
1.118 -\ {|NB', Crypt {|Agent B', Key K, NA'|} (shrK A'), \
1.119 -\ Crypt {|Agent A', Key K, NB', NB'|} (shrK B')|} \
1.120 +\ {|NB', Crypt {|Agent B', Key K, NA'|} (shrK A'), X'|} \
1.121 \ : set_of_list evs; \
1.122 \ evs : yahalom lost |] \
1.123 \ ==> A=A' & B=B' & NA=NA' & NB=NB'";
1.124 @@ -318,49 +297,19 @@
1.125 qed "unique_session_keys";
1.126
1.127
1.128 -(*If the encrypted message appears then it originated with the Server*)
1.129 -goal thy
1.130 - "!!evs. [| Crypt {|Agent B, Key K, Nonce NA|} (shrK A) \
1.131 -\ : parts (sees lost Spy evs); \
1.132 -\ A ~: lost; evs : yahalom lost |] \
1.133 -\ ==> EX NB. Says Server A \
1.134 -\ {|NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
1.135 -\ Crypt {|Agent A, Key K, NB, NB|} (shrK B)|} \
1.136 -\ : set_of_list evs";
1.137 -by (etac rev_mp 1);
1.138 -by (parts_induct_tac 1);
1.139 -by (Fast_tac 1);
1.140 -qed "A_trust_YM3";
1.141 -
1.142 -
1.143 -(*Describes the form of K when the Server sends this message.*)
1.144 -goal thy
1.145 - "!!evs. [| Says Server A \
1.146 -\ {|NB, Crypt {|Agent B, K, NA|} (shrK A), \
1.147 -\ Crypt {|Agent A, K, NB, NB|} (shrK B)|} \
1.148 -\ : set_of_list evs; \
1.149 -\ evs : yahalom lost |] \
1.150 -\ ==> (EX evt: yahalom lost. K = Key(newK evt))";
1.151 -by (etac rev_mp 1);
1.152 -by (etac yahalom.induct 1);
1.153 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
1.154 -qed "Says_Server_message_form";
1.155 -
1.156 -
1.157 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
1.158
1.159 goal thy
1.160 - "!!evs. [| A ~: lost; B ~: lost; \
1.161 -\ evs : yahalom lost; evt : yahalom lost |] \
1.162 + "!!evs. [| A ~: lost; B ~: lost; A ~= B; \
1.163 +\ evs : yahalom lost |] \
1.164 \ ==> Says Server A \
1.165 \ {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), \
1.166 -\ Crypt {|Agent A, Key K, NB, NB|} (shrK B)|} \
1.167 +\ Crypt {|NB, Key K, Agent A|} (shrK B)|} \
1.168 \ : set_of_list evs --> \
1.169 -\ Says A Spy {|NA, Key K|} ~: set_of_list evs --> \
1.170 +\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
1.171 \ Key K ~: analz (sees lost Spy evs)";
1.172 by (etac yahalom.induct 1);
1.173 by analz_Fake_tac;
1.174 -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
1.175 by (ALLGOALS
1.176 (asm_simp_tac
1.177 (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
1.178 @@ -370,18 +319,11 @@
1.179 by (fast_tac (!claset addIs [parts_insertI]
1.180 addEs [Says_imp_old_keys RS less_irrefl]
1.181 addss (!simpset)) 2);
1.182 -(*Reveal case 2, OR4, Fake*)
1.183 +(*OR4, Fake*)
1.184 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
1.185 -(*Reveal case 1*) (** LEVEL 6 **)
1.186 -by (case_tac "Aa : lost" 1);
1.187 -(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
1.188 -by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
1.189 -by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
1.190 -(*So now we have Aa ~: lost *)
1.191 -bd (Says_imp_sees_Spy RS parts.Inj) 1;
1.192 +(*Oops*)
1.193 by (fast_tac (!claset delrules [disjE]
1.194 - addSEs [MPair_parts]
1.195 - addDs [A_trust_YM3, unique_session_keys]
1.196 + addDs [unique_session_keys]
1.197 addss (!simpset)) 1);
1.198 val lemma = result() RS mp RS mp RSN(2,rev_notE);
1.199
1.200 @@ -390,25 +332,25 @@
1.201 goal thy
1.202 "!!evs. [| Says Server A \
1.203 \ {|NB, Crypt {|Agent B, K, NA|} (shrK A), \
1.204 -\ Crypt {|Agent A, K, NB, NB|} (shrK B)|} \
1.205 +\ Crypt {|NB, K, Agent A|} (shrK B)|} \
1.206 \ : set_of_list evs; \
1.207 -\ Says A Spy {|NA, K|} ~: set_of_list evs; \
1.208 -\ A ~: lost; B ~: lost; evs : yahalom lost |] ==> \
1.209 -\ K ~: analz (sees lost Spy evs)";
1.210 +\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \
1.211 +\ A ~: lost; B ~: lost; evs : yahalom lost |] \
1.212 +\ ==> K ~: analz (sees lost Spy evs)";
1.213 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
1.214 by (fast_tac (!claset addSEs [lemma]) 1);
1.215 qed "Spy_not_see_encrypted_key";
1.216
1.217
1.218 goal thy
1.219 - "!!evs. [| C ~: {A,B,Server}; \
1.220 + "!!evs. [| C ~: {A,B,Server}; \
1.221 \ Says Server A \
1.222 \ {|NB, Crypt {|Agent B, K, NA|} (shrK A), \
1.223 -\ Crypt {|Agent A, K, NB, NB|} (shrK B)|} \
1.224 +\ Crypt {|NB, K, Agent A|} (shrK B)|} \
1.225 \ : set_of_list evs; \
1.226 -\ Says A Spy {|NA, K|} ~: set_of_list evs; \
1.227 -\ A ~: lost; B ~: lost; evs : yahalom lost |] ==> \
1.228 -\ K ~: analz (sees lost C evs)";
1.229 +\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \
1.230 +\ A ~: lost; B ~: lost; evs : yahalom lost |] \
1.231 +\ ==> K ~: analz (sees lost C evs)";
1.232 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
1.233 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
1.234 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
1.235 @@ -416,18 +358,34 @@
1.236 qed "Agent_not_see_encrypted_key";
1.237
1.238
1.239 -(*** Security Guarantee for B upon receiving YM4 ***)
1.240 +(*** Security Guarantees for A and B ***)
1.241 +
1.242 +(*If the encrypted message appears then it originated with the Server.*)
1.243 +goal thy
1.244 + "!!evs. [| Crypt {|Agent B, Key K, NA|} (shrK A) \
1.245 +\ : parts (sees lost Spy evs); \
1.246 +\ A ~: lost; evs : yahalom lost |] \
1.247 +\ ==> EX NB. Says Server A \
1.248 +\ {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), \
1.249 +\ Crypt {|NB, Key K, Agent A|} (shrK B)|} \
1.250 +\ : set_of_list evs";
1.251 +by (etac rev_mp 1);
1.252 +by (parts_induct_tac 1);
1.253 +(*The nested conjunctions are entirely useless*)
1.254 +by (REPEAT_FIRST (rtac conjI ORELSE' fast_tac (!claset delrules [conjI])));
1.255 +qed "A_trust_YM3";
1.256 +
1.257
1.258 (*B knows, by the first part of A's message, that the Server distributed
1.259 - the key for A and B. But this part says nothing about nonces.*)
1.260 + the key for A and B. *)
1.261 goal thy
1.262 - "!!evs. [| Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B) \
1.263 -\ : parts (sees lost Spy evs); \
1.264 -\ B ~: lost; evs : yahalom lost |] \
1.265 + "!!evs. [| Crypt {|Nonce NB, Key K, Agent A|} (shrK B) \
1.266 +\ : parts (sees lost Spy evs); \
1.267 +\ B ~: lost; evs : yahalom lost |] \
1.268 \ ==> EX NA. Says Server A \
1.269 -\ {|Nonce NB, \
1.270 -\ Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
1.271 -\ Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B)|}\
1.272 +\ {|Nonce NB, \
1.273 +\ Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
1.274 +\ Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|} \
1.275 \ : set_of_list evs";
1.276 by (etac rev_mp 1);
1.277 by (parts_induct_tac 1);
1.278 @@ -439,17 +397,16 @@
1.279 Nonce NB is available in the first part. However the 2nd part does assure B
1.280 of A's existence.*)
1.281
1.282 -(*What can B deduce from receipt of YM4? Note how the two components of
1.283 - the message contribute to a single conclusion about the Server's message.*)
1.284 +(*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom
1.285 + because we do not have to show that NB is secret. *)
1.286 goal thy
1.287 - "!!evs. [| Says A' B {|Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B), \
1.288 + "!!evs. [| Says A' B {|Crypt {|Nonce NB, Key K, Agent A|} (shrK B), \
1.289 \ Crypt (Nonce NB) K|} : set_of_list evs; \
1.290 -\ ALL N N'. Says A Spy {|N,N', Key K|} ~: set_of_list evs; \
1.291 \ A ~: lost; B ~: lost; evs : yahalom lost |] \
1.292 \ ==> EX NA. Says Server A \
1.293 -\ {|Nonce NB, \
1.294 -\ Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
1.295 -\ Crypt {|Agent A, Key K, Nonce NB, Nonce NB|} (shrK B)|}\
1.296 +\ {|Nonce NB, \
1.297 +\ Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
1.298 +\ Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|} \
1.299 \ : set_of_list evs";
1.300 be (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1;
1.301 by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
2.1 --- a/src/HOL/Auth/Yahalom2.thy Fri Nov 01 18:27:38 1996 +0100
2.2 +++ b/src/HOL/Auth/Yahalom2.thy Fri Nov 01 18:28:19 1996 +0100
2.3 @@ -6,6 +6,8 @@
2.4 Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
2.5
2.6 This version trades encryption of NB for additional explicitness in YM3.
2.7 +It also omits encryption in YM2. The resulting protocol no longer guarantees
2.8 +that the other agent is present.
2.9
2.10 From page 259 of
2.11 Burrows, Abadi and Needham. A Logic of Authentication.
2.12 @@ -35,38 +37,37 @@
2.13 the sender is, hence the A' in the sender field.*)
2.14 YM2 "[| evs: yahalom lost; B ~= Server;
2.15 Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
2.16 - ==> Says B Server
2.17 - {|Agent B, Nonce (newN evs),
2.18 - Crypt {|Agent A, Nonce NA|} (shrK B)|}
2.19 + ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN evs)|}
2.20 # evs : yahalom lost"
2.21
2.22 (*The Server receives Bob's message. He responds by sending a
2.23 - new session key to Alice, with a packet for forwarding to Bob.*)
2.24 - YM3 "[| evs: yahalom lost; A ~= Server;
2.25 - Says B' Server
2.26 - {|Agent B, Nonce NB, Crypt {|Agent A, Nonce NA|} (shrK B)|}
2.27 + new session key to Alice, with a packet for forwarding to Bob.
2.28 + Fields are reversed in the 2nd packet to prevent attacks.*)
2.29 + YM3 "[| evs: yahalom lost; A ~= B; A ~= Server;
2.30 + Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
2.31 : set_of_list evs |]
2.32 ==> Says Server A
2.33 {|Nonce NB,
2.34 Crypt {|Agent B, Key (newK evs), Nonce NA|} (shrK A),
2.35 - Crypt {|Agent A, Key (newK evs), Nonce NB, Nonce NB|} (shrK B)|}
2.36 + Crypt {|Nonce NB, Key (newK evs), Agent A|} (shrK B)|}
2.37 # evs : yahalom lost"
2.38
2.39 (*Alice receives the Server's (?) message, checks her Nonce, and
2.40 uses the new session key to send Bob his Nonce.*)
2.41 - YM4 "[| evs: yahalom lost; A ~= B;
2.42 + YM4 "[| evs: yahalom lost; A ~= Server; A ~= B;
2.43 Says S A {|Nonce NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
2.44 X|}
2.45 : set_of_list evs;
2.46 Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
2.47 ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
2.48
2.49 - (*This message models possible leaks of session keys. The Nonce NA
2.50 - identifies the protocol run. We can't be sure about NB.*)
2.51 - Revl "[| evs: yahalom lost; A ~= Spy;
2.52 - Says S A {|Nonce NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
2.53 - X|}
2.54 - : set_of_list evs |]
2.55 - ==> Says A Spy {|Nonce NA, Key K|} # evs : yahalom lost"
2.56 + (*This message models possible leaks of session keys. The nonces
2.57 + identify the protocol run. Quoting Server here ensures they are
2.58 + correct. *)
2.59 + Oops "[| evs: yahalom lost; A ~= Spy;
2.60 + Says Server A {|Nonce NB,
2.61 + Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
2.62 + X|} : set_of_list evs |]
2.63 + ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
2.64
2.65 end