Public-key examples
authorpaulson
Thu Dec 05 18:07:27 1996 +0100 (1996-12-05)
changeset 23186d3f7c7f70b0
parent 2317 672015b535d7
child 2319 95f0d5243c85
Public-key examples
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/Public.ML
src/HOL/Auth/Public.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/NS_Public.ML	Thu Dec 05 18:07:27 1996 +0100
     1.3 @@ -0,0 +1,438 @@
     1.4 +(*  Title:      HOL/Auth/NS_Public
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
    1.10 +Version incorporating Lowe's fix (inclusion of B's identify in round 2).
    1.11 +*)
    1.12 +
    1.13 +open NS_Public;
    1.14 +
    1.15 +proof_timing:=true;
    1.16 +HOL_quantifiers := false;
    1.17 +Pretty.setdepth 20;
    1.18 +
    1.19 +AddIffs [Spy_in_lost];
    1.20 +
    1.21 +(*Replacing the variable by a constant improves search speed by 50%!*)
    1.22 +val Says_imp_sees_Spy' = 
    1.23 +    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
    1.24 +
    1.25 +
    1.26 +(*A "possibility property": there are traces that reach the end*)
    1.27 +goal thy 
    1.28 + "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
    1.29 +\                     Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
    1.30 +by (REPEAT (resolve_tac [exI,bexI] 1));
    1.31 +by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
    1.32 +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.33 +by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    1.34 +by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    1.35 +result();
    1.36 +
    1.37 +
    1.38 +(**** Inductive proofs about ns_public ****)
    1.39 +
    1.40 +(*Nobody sends themselves messages*)
    1.41 +goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs";
    1.42 +by (etac ns_public.induct 1);
    1.43 +by (Auto_tac());
    1.44 +qed_spec_mp "not_Says_to_self";
    1.45 +Addsimps [not_Says_to_self];
    1.46 +AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    1.47 +
    1.48 +
    1.49 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    1.50 +fun parts_induct_tac i = SELECT_GOAL
    1.51 +    (DETERM (etac ns_public.induct 1 THEN 
    1.52 +             (*Fake message*)
    1.53 +             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.54 +                                           impOfSubs Fake_parts_insert]
    1.55 +                                    addss (!simpset)) 2)) THEN
    1.56 +     (*Base case*)
    1.57 +     fast_tac (!claset addss (!simpset)) 1 THEN
    1.58 +     ALLGOALS Asm_simp_tac) i;
    1.59 +
    1.60 +(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    1.61 +    sends messages containing X! **)
    1.62 +
    1.63 +(*Spy never sees another agent's private key! (unless it's lost at start)*)
    1.64 +goal thy 
    1.65 + "!!evs. evs : ns_public \
    1.66 +\        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
    1.67 +by (parts_induct_tac 1);
    1.68 +by (Auto_tac());
    1.69 +qed "Spy_see_priK";
    1.70 +Addsimps [Spy_see_priK];
    1.71 +
    1.72 +goal thy 
    1.73 + "!!evs. evs : ns_public \
    1.74 +\        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
    1.75 +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.76 +qed "Spy_analz_priK";
    1.77 +Addsimps [Spy_analz_priK];
    1.78 +
    1.79 +goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
    1.80 +\                  evs : ns_public |] ==> A:lost";
    1.81 +by (fast_tac (!claset addDs [Spy_see_priK]) 1);
    1.82 +qed "Spy_see_priK_D";
    1.83 +
    1.84 +bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
    1.85 +AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
    1.86 +
    1.87 +
    1.88 +(*** Future nonces can't be seen or used! ***)
    1.89 +
    1.90 +goal thy "!!evs. evs : ns_public ==> \
    1.91 +\                length evs <= length evt --> \
    1.92 +\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    1.93 +by (parts_induct_tac 1);
    1.94 +by (REPEAT_FIRST (fast_tac (!claset 
    1.95 +                              addSEs partsEs
    1.96 +                              addSDs  [Says_imp_sees_Spy' RS parts.Inj]
    1.97 +                              addEs [leD RS notE]
    1.98 +			      addDs  [impOfSubs analz_subset_parts,
    1.99 +                                      impOfSubs parts_insert_subset_Un,
   1.100 +                                      Suc_leD]
   1.101 +                              addss (!simpset))));
   1.102 +qed_spec_mp "new_nonces_not_seen";
   1.103 +Addsimps [new_nonces_not_seen];
   1.104 +
   1.105 +val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   1.106 +
   1.107 +
   1.108 +(**** Authenticity properties obtained from NS2 ****)
   1.109 +
   1.110 +(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
   1.111 +  is secret.  (Honest users generate fresh nonces.)*)
   1.112 +goal thy 
   1.113 + "!!evs. evs : ns_public                       \
   1.114 +\ ==> Nonce NA ~: analz (sees lost Spy evs) -->           \
   1.115 +\     Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
   1.116 +\     Crypt (pubK C) {|X, Nonce NA, Agent D|} ~: parts (sees lost Spy evs)";
   1.117 +by (etac ns_public.induct 1);
   1.118 +by (ALLGOALS
   1.119 +    (asm_simp_tac 
   1.120 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   1.121 +               setloop split_tac [expand_if])));
   1.122 +(*NS3*)
   1.123 +by (fast_tac (!claset addSEs partsEs
   1.124 +                      addEs  [nonce_not_seen_now]) 4);
   1.125 +(*NS2*)
   1.126 +by (fast_tac (!claset addSEs partsEs
   1.127 +                      addEs  [nonce_not_seen_now]) 3);
   1.128 +(*Fake*)
   1.129 +by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)]
   1.130 +		      addDs [impOfSubs analz_subset_parts,
   1.131 +			     impOfSubs Fake_parts_insert]
   1.132 +	              addss (!simpset)) 2);
   1.133 +(*Base*)
   1.134 +by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
   1.135 +                      addss (!simpset)) 1);
   1.136 +bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
   1.137 +
   1.138 +
   1.139 +(*Uniqueness for NS1: nonce NA identifies agents A and B*)
   1.140 +goal thy 
   1.141 + "!!evs. evs : ns_public                                                    \
   1.142 +\ ==> Nonce NA ~: analz (sees lost Spy evs) -->                             \
   1.143 +\     (EX A' B'. ALL A B.                                                   \
   1.144 +\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
   1.145 +\      A=A' & B=B')";
   1.146 +by (etac ns_public.induct 1);
   1.147 +by (ALLGOALS 
   1.148 +    (asm_simp_tac 
   1.149 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   1.150 +               setloop split_tac [expand_if])));
   1.151 +(*NS1*)
   1.152 +by (expand_case_tac "NA = ?y" 3 THEN
   1.153 +    REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
   1.154 +(*Base*)
   1.155 +by (fast_tac (!claset addss (!simpset)) 1);
   1.156 +(*Fake*)
   1.157 +by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
   1.158 +by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
   1.159 +by (ex_strip_tac 1);
   1.160 +by (best_tac (!claset delrules [conjI]
   1.161 +	              addDs  [impOfSubs analz_subset_parts,
   1.162 +			      impOfSubs Fake_parts_insert]
   1.163 +                      addss (!simpset)) 1);
   1.164 +val lemma = result();
   1.165 +
   1.166 +goal thy 
   1.167 + "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(sees lost Spy evs); \
   1.168 +\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \
   1.169 +\           Nonce NA ~: analz (sees lost Spy evs);                            \
   1.170 +\           evs : ns_public |]                                                \
   1.171 +\        ==> A=A' & B=B'";
   1.172 +by (dtac lemma 1);
   1.173 +by (mp_tac 1);
   1.174 +by (REPEAT (etac exE 1));
   1.175 +(*Duplicate the assumption*)
   1.176 +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.177 +by (fast_tac (!claset addSDs [spec]) 1);
   1.178 +qed "unique_NA";
   1.179 +
   1.180 +
   1.181 +(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
   1.182 +goal thy 
   1.183 + "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
   1.184 +\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \
   1.185 +\     --> Nonce NA ~: analz (sees lost Spy evs)";
   1.186 +by (etac ns_public.induct 1);
   1.187 +by (ALLGOALS 
   1.188 +    (asm_simp_tac 
   1.189 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   1.190 +               setloop split_tac [expand_if])));
   1.191 +(*NS3*)
   1.192 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.193 +                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
   1.194 +(*NS1*)
   1.195 +by (fast_tac (!claset addSEs partsEs
   1.196 +                      addSDs [new_nonces_not_seen, 
   1.197 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.198 +(*Fake*)
   1.199 +by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
   1.200 +(*NS2*)
   1.201 +by (Step_tac 1);
   1.202 +by (fast_tac (!claset addSEs partsEs
   1.203 +                      addSDs [new_nonces_not_seen, 
   1.204 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.205 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.206 +                      addDs  [unique_NA]) 1);
   1.207 +bind_thm ("Spy_not_see_NA", result() RSN (2, rev_mp));
   1.208 +
   1.209 +
   1.210 +(*Authentication for A: if she receives message 2 and has used NA
   1.211 +  to start a run, then B has sent message 2.*)
   1.212 +goal thy 
   1.213 + "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]       \
   1.214 +\ ==> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}         \
   1.215 +\                                : parts (sees lost Spy evs) \
   1.216 +\     --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \
   1.217 +\     --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})         \
   1.218 +\           : set_of_list evs";
   1.219 +by (etac ns_public.induct 1);
   1.220 +by (ALLGOALS Asm_simp_tac);
   1.221 +(*NS1*)
   1.222 +by (fast_tac (!claset addSEs partsEs
   1.223 +                      addSDs [new_nonces_not_seen, 
   1.224 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.225 +(*Fake*)
   1.226 +by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   1.227 +by (fast_tac (!claset addss (!simpset)) 1);
   1.228 +by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
   1.229 +by (best_tac (!claset addSIs [disjI2]
   1.230 +		      addDs [impOfSubs analz_subset_parts,
   1.231 +			     impOfSubs Fake_parts_insert]
   1.232 +	              addss (!simpset)) 1);
   1.233 +qed_spec_mp "NA_decrypt_imp_B_msg";
   1.234 +
   1.235 +(*Corollary: if A receives B's message NS2 and the nonce NA agrees
   1.236 +  then that message really originated with B.*)
   1.237 +goal thy 
   1.238 + "!!evs. [| Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   1.239 +\             : set_of_list evs;\
   1.240 +\           Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\
   1.241 +\           A ~: lost;  B ~: lost;  evs : ns_public |]  \
   1.242 +\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   1.243 +\              : set_of_list evs";
   1.244 +by (fast_tac (!claset addSIs [NA_decrypt_imp_B_msg]
   1.245 +                      addEs  partsEs
   1.246 +                      addDs  [Says_imp_sees_Spy' RS parts.Inj]) 1);
   1.247 +qed "A_trusts_NS2";
   1.248 +
   1.249 +(*If the encrypted message appears then it originated with Alice in NS1*)
   1.250 +goal thy 
   1.251 + "!!evs. evs : ns_public                   \
   1.252 +\    ==> Nonce NA ~: analz (sees lost Spy evs) --> \
   1.253 +\        Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
   1.254 +\        Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
   1.255 +by (etac ns_public.induct 1);
   1.256 +by (ALLGOALS
   1.257 +    (asm_simp_tac 
   1.258 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   1.259 +               setloop split_tac [expand_if])));
   1.260 +(*Fake*)
   1.261 +by (best_tac (!claset addSIs [disjI2]
   1.262 +		      addIs [impOfSubs (subset_insertI RS analz_mono)]
   1.263 +		      addDs [impOfSubs analz_subset_parts,
   1.264 +			     impOfSubs Fake_parts_insert]
   1.265 +	              addss (!simpset)) 2);
   1.266 +(*Base*)
   1.267 +by (fast_tac (!claset addss (!simpset)) 1);
   1.268 +qed_spec_mp "B_trusts_NS1";
   1.269 +
   1.270 +
   1.271 +
   1.272 +(**** Authenticity properties obtained from NS2 ****)
   1.273 +
   1.274 +(*Uniqueness for NS2: nonce NB identifies nonce NA and agents A, B 
   1.275 +  [unicity of B makes Lowe's fix work]
   1.276 +  [proof closely follows that for unique_NA] *)
   1.277 +goal thy 
   1.278 + "!!evs. evs : ns_public                                                    \
   1.279 +\ ==> Nonce NB ~: analz (sees lost Spy evs) -->                             \
   1.280 +\     (EX A' NA' B'. ALL A NA B.                                            \
   1.281 +\      Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}   \
   1.282 +\        : parts (sees lost Spy evs)  -->  A=A' & NA=NA' & B=B')";
   1.283 +by (etac ns_public.induct 1);
   1.284 +by (ALLGOALS 
   1.285 +    (asm_simp_tac 
   1.286 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   1.287 +               setloop split_tac [expand_if])));
   1.288 +(*NS2*)
   1.289 +by (expand_case_tac "NB = ?y" 3 THEN
   1.290 +    REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
   1.291 +(*Base*)
   1.292 +by (fast_tac (!claset addss (!simpset)) 1);
   1.293 +(*Fake*)
   1.294 +by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
   1.295 +by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
   1.296 +by (ex_strip_tac 1);
   1.297 +by (best_tac (!claset delrules [conjI]
   1.298 +	              addDs  [impOfSubs analz_subset_parts,
   1.299 +			      impOfSubs Fake_parts_insert]
   1.300 +                      addss (!simpset)) 1);
   1.301 +val lemma = result();
   1.302 +
   1.303 +goal thy 
   1.304 + "!!evs. [| Crypt(pubK A)  {|Nonce NA, Nonce NB, Agent B|}   \
   1.305 +\             : parts(sees lost Spy evs);                    \
   1.306 +\           Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
   1.307 +\             : parts(sees lost Spy evs);                    \
   1.308 +\           Nonce NB ~: analz (sees lost Spy evs);           \
   1.309 +\           evs : ns_public |]                               \
   1.310 +\        ==> A=A' & NA=NA' & B=B'";
   1.311 +by (dtac lemma 1);
   1.312 +by (mp_tac 1);
   1.313 +by (REPEAT (etac exE 1));
   1.314 +(*Duplicate the assumption*)
   1.315 +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.316 +by (fast_tac (!claset addSDs [spec]) 1);
   1.317 +qed "unique_NB";
   1.318 +
   1.319 +
   1.320 +(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
   1.321 +goal thy 
   1.322 + "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
   1.323 +\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   1.324 +\       : set_of_list evs \
   1.325 +\     --> Nonce NB ~: analz (sees lost Spy evs)";
   1.326 +by (etac ns_public.induct 1);
   1.327 +by (ALLGOALS 
   1.328 +    (asm_simp_tac 
   1.329 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   1.330 +               setloop split_tac [expand_if])));
   1.331 +(*NS3*)
   1.332 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.333 +                      addDs  [unique_NB]) 4);
   1.334 +(*NS1*)
   1.335 +by (fast_tac (!claset addSEs partsEs
   1.336 +                      addSDs [new_nonces_not_seen, 
   1.337 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.338 +(*Fake*)
   1.339 +by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
   1.340 +(*NS2*)
   1.341 +by (Step_tac 1);
   1.342 +by (fast_tac (!claset addSEs partsEs
   1.343 +                      addSDs [new_nonces_not_seen, 
   1.344 +                              Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.345 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.346 +                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
   1.347 +bind_thm ("Spy_not_see_NB", result() RSN (2, rev_mp));
   1.348 +
   1.349 +
   1.350 +(*Matches only NS2, not NS1 (or NS3)*)
   1.351 +val Says_imp_sees_Spy'' = 
   1.352 +    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy';
   1.353 +
   1.354 +
   1.355 +(*Authentication for B: if he receives message 3 and has used NB
   1.356 +  in message 2, then A has sent message 3.*)
   1.357 +goal thy 
   1.358 + "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]       \
   1.359 +\ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \
   1.360 +\     --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   1.361 +\       : set_of_list evs \
   1.362 +\     --> Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
   1.363 +by (etac ns_public.induct 1);
   1.364 +by (ALLGOALS Asm_simp_tac);
   1.365 +(*NS1*)
   1.366 +by (fast_tac (!claset addSEs partsEs
   1.367 +                      addSDs [new_nonces_not_seen, 
   1.368 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.369 +(*Fake*)
   1.370 +by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   1.371 +by (fast_tac (!claset addss (!simpset)) 1);
   1.372 +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.373 +by (best_tac (!claset addSIs [disjI2]
   1.374 +		      addDs [impOfSubs analz_subset_parts,
   1.375 +			     impOfSubs Fake_parts_insert]
   1.376 +	              addss (!simpset)) 1);
   1.377 +(*NS3*)
   1.378 +by (Step_tac 1);
   1.379 +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.380 +by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
   1.381 +	              addDs  [unique_NB]) 1);
   1.382 +qed_spec_mp "NB_decrypt_imp_A_msg";
   1.383 +
   1.384 +(*Corollary: if B receives message NS3 and the nonce NB agrees
   1.385 +  then that message really originated with A.*)
   1.386 +goal thy 
   1.387 + "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs;    \
   1.388 +\           Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   1.389 +\             : set_of_list evs;                                       \
   1.390 +\           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
   1.391 +\        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
   1.392 +by (fast_tac (!claset addSIs [NB_decrypt_imp_A_msg]
   1.393 +                      addEs  partsEs
   1.394 +                      addDs  [Says_imp_sees_Spy' RS parts.Inj]) 1);
   1.395 +qed "B_trusts_NS3";
   1.396 +
   1.397 +
   1.398 +(**** Overall guarantee for B*)
   1.399 +
   1.400 +(*If B receives NS3 and the nonce NB agrees with the nonce he joined with
   1.401 +  NA, then A initiated the run using NA.
   1.402 +  SAME PROOF AS NB_decrypt_imp_A_msg*)
   1.403 +goal thy 
   1.404 + "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]       \
   1.405 +\ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \
   1.406 +\     --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   1.407 +\       : set_of_list evs \
   1.408 +\     --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
   1.409 +by (etac ns_public.induct 1);
   1.410 +by (ALLGOALS Asm_simp_tac);
   1.411 +(*Fake, NS2, NS3*)
   1.412 +(*NS1*)
   1.413 +by (fast_tac (!claset addSEs partsEs
   1.414 +                      addSDs [new_nonces_not_seen, 
   1.415 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.416 +(*Fake*)
   1.417 +by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   1.418 +by (fast_tac (!claset addss (!simpset)) 1);
   1.419 +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.420 +by (best_tac (!claset addSIs [disjI2]
   1.421 +		      addDs [impOfSubs analz_subset_parts,
   1.422 +			     impOfSubs Fake_parts_insert]
   1.423 +	              addss (!simpset)) 1);
   1.424 +(*NS3*)
   1.425 +by (Step_tac 1);
   1.426 +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.427 +by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
   1.428 +	              addDs  [unique_NB]) 1);
   1.429 +val lemma = result() RSN (2, rev_mp) RSN (2, rev_mp);
   1.430 +
   1.431 +goal thy 
   1.432 + "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs;    \
   1.433 +\           Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   1.434 +\             : set_of_list evs;                                       \
   1.435 +\           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
   1.436 +\    ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
   1.437 +by (fast_tac (!claset addSIs [lemma]
   1.438 +                      addEs  partsEs
   1.439 +                      addDs  [Says_imp_sees_Spy' RS parts.Inj]) 1);
   1.440 +qed_spec_mp "B_trusts_protocol";
   1.441 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/NS_Public.thy	Thu Dec 05 18:07:27 1996 +0100
     2.3 @@ -0,0 +1,52 @@
     2.4 +(*  Title:      HOL/Auth/NS_Public
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1996  University of Cambridge
     2.8 +
     2.9 +Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
    2.10 +Version incorporating Lowe's fix (inclusion of B's identify in round 2).
    2.11 +*)
    2.12 +
    2.13 +NS_Public = Public + 
    2.14 +
    2.15 +consts  lost    :: agent set        (*No need for it to be a variable*)
    2.16 +	ns_public  :: event list set
    2.17 +inductive ns_public
    2.18 +  intrs 
    2.19 +         (*Initial trace is empty*)
    2.20 +    Nil  "[]: ns_public"
    2.21 +
    2.22 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    2.23 +           invent new nonces here, but he can also use NS1.  Common to
    2.24 +           all similar protocols.*)
    2.25 +    Fake "[| evs: ns_public;  B ~= Spy;  
    2.26 +             X: synth (analz (sees lost Spy evs)) |]
    2.27 +          ==> Says Spy B X  # evs : ns_public"
    2.28 +
    2.29 +         (*Alice initiates a protocol run, sending a nonce to Bob*)
    2.30 +    NS1  "[| evs: ns_public;  A ~= B |]
    2.31 +          ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs
    2.32 +                : ns_public"
    2.33 +
    2.34 +         (*Bob responds to Alice's message with a further nonce*)
    2.35 +    NS2  "[| evs: ns_public;  A ~= B;
    2.36 +             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
    2.37 +               : set_of_list evs |]
    2.38 +          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs), Agent B|})
    2.39 +                # evs  : ns_public"
    2.40 +
    2.41 +         (*Alice proves her existence by sending NB back to Bob.*)
    2.42 +    NS3  "[| evs: ns_public;  A ~= B;
    2.43 +             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    2.44 +               : set_of_list evs;
    2.45 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
    2.46 +               : set_of_list evs |]
    2.47 +          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    2.48 +
    2.49 +  (**Oops message??**)
    2.50 +
    2.51 +rules
    2.52 +  (*Spy has access to his own key for spoof messages*)
    2.53 +  Spy_in_lost "Spy: lost"
    2.54 +
    2.55 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Thu Dec 05 18:07:27 1996 +0100
     3.3 @@ -0,0 +1,453 @@
     3.4 +(*  Title:      HOL/Auth/NS_Public_Bad
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1996  University of Cambridge
     3.8 +
     3.9 +Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
    3.10 +Flawed version, vulnerable to Lowe's attack.
    3.11 +
    3.12 +From page 260 of
    3.13 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    3.14 +  Proc. Royal Soc. 426 (1989)
    3.15 +*)
    3.16 +
    3.17 +open NS_Public_Bad;
    3.18 +
    3.19 +proof_timing:=true;
    3.20 +HOL_quantifiers := false;
    3.21 +Pretty.setdepth 20;
    3.22 +
    3.23 +AddIffs [Spy_in_lost];
    3.24 +
    3.25 +(*Replacing the variable by a constant improves search speed by 50%!*)
    3.26 +val Says_imp_sees_Spy' = 
    3.27 +    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
    3.28 +
    3.29 +
    3.30 +(*A "possibility property": there are traces that reach the end*)
    3.31 +goal thy 
    3.32 + "!!A B. [| A ~= B |]   \
    3.33 +\        ==> EX NB. EX evs: ns_public.               \
    3.34 +\               Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
    3.35 +by (REPEAT (resolve_tac [exI,bexI] 1));
    3.36 +by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
    3.37 +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    3.38 +by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    3.39 +by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    3.40 +result();
    3.41 +
    3.42 +
    3.43 +(**** Inductive proofs about ns_public ****)
    3.44 +
    3.45 +(*Nobody sends themselves messages*)
    3.46 +goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs";
    3.47 +by (etac ns_public.induct 1);
    3.48 +by (Auto_tac());
    3.49 +qed_spec_mp "not_Says_to_self";
    3.50 +Addsimps [not_Says_to_self];
    3.51 +AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    3.52 +
    3.53 +
    3.54 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    3.55 +fun parts_induct_tac i = SELECT_GOAL
    3.56 +    (DETERM (etac ns_public.induct 1 THEN 
    3.57 +             (*Fake message*)
    3.58 +             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    3.59 +                                           impOfSubs Fake_parts_insert]
    3.60 +                                    addss (!simpset)) 2)) THEN
    3.61 +     (*Base case*)
    3.62 +     fast_tac (!claset addss (!simpset)) 1 THEN
    3.63 +     ALLGOALS Asm_simp_tac) i;
    3.64 +
    3.65 +(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    3.66 +    sends messages containing X! **)
    3.67 +
    3.68 +(*Spy never sees another agent's private key! (unless it's lost at start)*)
    3.69 +goal thy 
    3.70 + "!!evs. evs : ns_public \
    3.71 +\        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
    3.72 +by (parts_induct_tac 1);
    3.73 +by (Auto_tac());
    3.74 +qed "Spy_see_priK";
    3.75 +Addsimps [Spy_see_priK];
    3.76 +
    3.77 +goal thy 
    3.78 + "!!evs. evs : ns_public \
    3.79 +\        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
    3.80 +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    3.81 +qed "Spy_analz_priK";
    3.82 +Addsimps [Spy_analz_priK];
    3.83 +
    3.84 +goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
    3.85 +\                  evs : ns_public |] ==> A:lost";
    3.86 +by (fast_tac (!claset addDs [Spy_see_priK]) 1);
    3.87 +qed "Spy_see_priK_D";
    3.88 +
    3.89 +bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
    3.90 +AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
    3.91 +
    3.92 +
    3.93 +(*** Future nonces can't be seen or used! ***)
    3.94 +
    3.95 +goal thy "!!evs. evs : ns_public ==> \
    3.96 +\                length evs <= length evt --> \
    3.97 +\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    3.98 +by (parts_induct_tac 1);
    3.99 +by (REPEAT_FIRST (fast_tac (!claset 
   3.100 +                              addSEs partsEs
   3.101 +                              addSDs  [Says_imp_sees_Spy' RS parts.Inj]
   3.102 +                              addEs [leD RS notE]
   3.103 +			      addDs  [impOfSubs analz_subset_parts,
   3.104 +                                      impOfSubs parts_insert_subset_Un,
   3.105 +                                      Suc_leD]
   3.106 +                              addss (!simpset))));
   3.107 +qed_spec_mp "new_nonces_not_seen";
   3.108 +Addsimps [new_nonces_not_seen];
   3.109 +
   3.110 +val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   3.111 +
   3.112 +
   3.113 +(**** Authenticity properties obtained from NS2 ****)
   3.114 +
   3.115 +(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
   3.116 +  is secret.  (Honest users generate fresh nonces.)*)
   3.117 +goal thy 
   3.118 + "!!evs. evs : ns_public                       \
   3.119 +\ ==> Nonce NA ~: analz (sees lost Spy evs) -->           \
   3.120 +\     Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
   3.121 +\     Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees lost Spy evs)";
   3.122 +by (etac ns_public.induct 1);
   3.123 +by (ALLGOALS
   3.124 +    (asm_simp_tac 
   3.125 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   3.126 +               setloop split_tac [expand_if])));
   3.127 +(*NS3*)
   3.128 +by (fast_tac (!claset addSEs partsEs
   3.129 +                      addEs  [nonce_not_seen_now]) 4);
   3.130 +(*NS2*)
   3.131 +by (fast_tac (!claset addSEs partsEs
   3.132 +                      addEs  [nonce_not_seen_now]) 3);
   3.133 +(*Fake*)
   3.134 +by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)]
   3.135 +		      addDs [impOfSubs analz_subset_parts,
   3.136 +			     impOfSubs Fake_parts_insert]
   3.137 +	              addss (!simpset)) 2);
   3.138 +(*Base*)
   3.139 +by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
   3.140 +                      addss (!simpset)) 1);
   3.141 +bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
   3.142 +
   3.143 +
   3.144 +(*Uniqueness for NS1: nonce NA identifies agents A and B*)
   3.145 +goal thy 
   3.146 + "!!evs. evs : ns_public                                                    \
   3.147 +\ ==> Nonce NA ~: analz (sees lost Spy evs) -->                             \
   3.148 +\     (EX A' B'. ALL A B.                                                   \
   3.149 +\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
   3.150 +\      A=A' & B=B')";
   3.151 +by (etac ns_public.induct 1);
   3.152 +by (ALLGOALS 
   3.153 +    (asm_simp_tac 
   3.154 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   3.155 +               setloop split_tac [expand_if])));
   3.156 +(*NS1*)
   3.157 +by (expand_case_tac "NA = ?y" 3 THEN
   3.158 +    REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
   3.159 +(*Base*)
   3.160 +by (fast_tac (!claset addss (!simpset)) 1);
   3.161 +(*Fake*)
   3.162 +by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
   3.163 +by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
   3.164 +by (ex_strip_tac 1);
   3.165 +by (best_tac (!claset delrules [conjI]
   3.166 +	              addDs  [impOfSubs analz_subset_parts,
   3.167 +			      impOfSubs Fake_parts_insert]
   3.168 +                      addss (!simpset)) 1);
   3.169 +val lemma = result();
   3.170 +
   3.171 +goal thy 
   3.172 + "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(sees lost Spy evs); \
   3.173 +\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \
   3.174 +\           Nonce NA ~: analz (sees lost Spy evs);                            \
   3.175 +\           evs : ns_public |]                                                \
   3.176 +\        ==> A=A' & B=B'";
   3.177 +by (dtac lemma 1);
   3.178 +by (mp_tac 1);
   3.179 +by (REPEAT (etac exE 1));
   3.180 +(*Duplicate the assumption*)
   3.181 +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   3.182 +by (fast_tac (!claset addSDs [spec]) 1);
   3.183 +qed "unique_NA";
   3.184 +
   3.185 +
   3.186 +(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
   3.187 +goal thy 
   3.188 + "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
   3.189 +\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \
   3.190 +\     --> Nonce NA ~: analz (sees lost Spy evs)";
   3.191 +by (etac ns_public.induct 1);
   3.192 +by (ALLGOALS 
   3.193 +    (asm_simp_tac 
   3.194 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   3.195 +               setloop split_tac [expand_if])));
   3.196 +(*NS3*)
   3.197 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.198 +                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
   3.199 +(*NS1*)
   3.200 +by (fast_tac (!claset addSEs partsEs
   3.201 +                      addSDs [new_nonces_not_seen, 
   3.202 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.203 +(*Fake*)
   3.204 +by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
   3.205 +(*NS2*)
   3.206 +by (Step_tac 1);
   3.207 +by (fast_tac (!claset addSEs partsEs
   3.208 +                      addSDs [new_nonces_not_seen, 
   3.209 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.210 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.211 +                      addDs  [unique_NA]) 1);
   3.212 +bind_thm ("Spy_not_see_NA", result() RSN (2, rev_mp));
   3.213 +
   3.214 +
   3.215 +(*Authentication for A: if she receives message 2 and has used NA
   3.216 +  to start a run, then B has sent message 2.*)
   3.217 +goal thy 
   3.218 + "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]       \
   3.219 +\ ==> Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \
   3.220 +\     --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \
   3.221 +\     --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs";
   3.222 +by (etac ns_public.induct 1);
   3.223 +by (ALLGOALS Asm_simp_tac);
   3.224 +(*NS1*)
   3.225 +by (fast_tac (!claset addSEs partsEs
   3.226 +                      addSDs [new_nonces_not_seen, 
   3.227 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.228 +(*Fake*)
   3.229 +by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   3.230 +by (fast_tac (!claset addss (!simpset)) 1);
   3.231 +by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
   3.232 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   3.233 +			     impOfSubs Fake_parts_insert]
   3.234 +	              addss (!simpset)) 1);
   3.235 +(*NS2*)
   3.236 +by (Step_tac 1);
   3.237 +by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
   3.238 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.239 +                      addDs  [unique_NA]) 1);
   3.240 +qed_spec_mp "NA_decrypt_imp_B_msg";
   3.241 +
   3.242 +(*Corollary: if A receives B's message NS2 and the nonce NA agrees
   3.243 +  then that message really originated with B.*)
   3.244 +goal thy 
   3.245 + "!!evs. [| Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs;\
   3.246 +\           Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\
   3.247 +\           A ~: lost;  B ~: lost;  evs : ns_public |]  \
   3.248 +\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs";
   3.249 +by (fast_tac (!claset addSIs [NA_decrypt_imp_B_msg]
   3.250 +                      addEs  partsEs
   3.251 +                      addDs  [Says_imp_sees_Spy' RS parts.Inj]) 1);
   3.252 +qed "A_trusts_NS2";
   3.253 +
   3.254 +(*If the encrypted message appears then it originated with Alice in NS1*)
   3.255 +goal thy 
   3.256 + "!!evs. evs : ns_public                   \
   3.257 +\    ==> Nonce NA ~: analz (sees lost Spy evs) --> \
   3.258 +\        Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
   3.259 +\        Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
   3.260 +by (etac ns_public.induct 1);
   3.261 +by (ALLGOALS
   3.262 +    (asm_simp_tac 
   3.263 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   3.264 +               setloop split_tac [expand_if])));
   3.265 +(*Fake*)
   3.266 +by (best_tac (!claset addSIs [disjI2]
   3.267 +		      addIs [impOfSubs (subset_insertI RS analz_mono)]
   3.268 +		      addDs [impOfSubs analz_subset_parts,
   3.269 +			     impOfSubs Fake_parts_insert]
   3.270 +	              addss (!simpset)) 2);
   3.271 +(*Base*)
   3.272 +by (fast_tac (!claset addss (!simpset)) 1);
   3.273 +qed_spec_mp "B_trusts_NS1";
   3.274 +
   3.275 +
   3.276 +
   3.277 +(**** Authenticity properties obtained from NS2 ****)
   3.278 +
   3.279 +(*Uniqueness for NS2: nonce NB identifies agent A and nonce NA
   3.280 +  [proof closely follows that for unique_NA] *)
   3.281 +goal thy 
   3.282 + "!!evs. evs : ns_public                                                    \
   3.283 +\ ==> Nonce NB ~: analz (sees lost Spy evs) -->                             \
   3.284 +\     (EX A' NA'. ALL A NA.                                                   \
   3.285 +\      Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (sees lost Spy evs) --> \
   3.286 +\      A=A' & NA=NA')";
   3.287 +by (etac ns_public.induct 1);
   3.288 +by (ALLGOALS 
   3.289 +    (asm_simp_tac 
   3.290 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   3.291 +               setloop split_tac [expand_if])));
   3.292 +(*NS2*)
   3.293 +by (expand_case_tac "NB = ?y" 3 THEN
   3.294 +    REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
   3.295 +(*Base*)
   3.296 +by (fast_tac (!claset addss (!simpset)) 1);
   3.297 +(*Fake*)
   3.298 +by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
   3.299 +by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
   3.300 +by (ex_strip_tac 1);
   3.301 +by (best_tac (!claset delrules [conjI]
   3.302 +	              addDs  [impOfSubs analz_subset_parts,
   3.303 +			      impOfSubs Fake_parts_insert]
   3.304 +                      addss (!simpset)) 1);
   3.305 +val lemma = result();
   3.306 +
   3.307 +goal thy 
   3.308 + "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|}  : parts(sees lost Spy evs); \
   3.309 +\           Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(sees lost Spy evs); \
   3.310 +\           Nonce NB ~: analz (sees lost Spy evs);                            \
   3.311 +\           evs : ns_public |]                                                \
   3.312 +\        ==> A=A' & NA=NA'";
   3.313 +by (dtac lemma 1);
   3.314 +by (mp_tac 1);
   3.315 +by (REPEAT (etac exE 1));
   3.316 +(*Duplicate the assumption*)
   3.317 +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   3.318 +by (fast_tac (!claset addSDs [spec]) 1);
   3.319 +qed "unique_NB";
   3.320 +
   3.321 +
   3.322 +(*NB remains secret PROVIDED Alice never responds with round 3*)
   3.323 +goal thy 
   3.324 + "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
   3.325 +\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs --> \
   3.326 +\     (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set_of_list evs) --> \
   3.327 +\     Nonce NB ~: analz (sees lost Spy evs)";
   3.328 +by (etac ns_public.induct 1);
   3.329 +by (ALLGOALS 
   3.330 +    (asm_simp_tac 
   3.331 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   3.332 +               setloop split_tac [expand_if])));
   3.333 +(*NS1*)
   3.334 +by (fast_tac (!claset addSEs partsEs
   3.335 +                      addSDs [new_nonces_not_seen, 
   3.336 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.337 +(*Fake*)
   3.338 +by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
   3.339 +(*NS2 and NS3*)
   3.340 +by (Step_tac 1);
   3.341 +(*NS2*)
   3.342 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.343 +                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 3);
   3.344 +by (fast_tac (!claset addSEs partsEs
   3.345 +                      addSDs [new_nonces_not_seen, 
   3.346 +                              Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.347 +by (Fast_tac 1);
   3.348 +(*NS3*)
   3.349 +by (Fast_tac 2);
   3.350 +by (fast_tac (!claset addSEs partsEs
   3.351 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj,
   3.352 +			      new_nonces_not_seen, 
   3.353 +                              impOfSubs analz_subset_parts]) 1);
   3.354 +
   3.355 +by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1
   3.356 +    THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1));
   3.357 +by (Fast_tac 1);
   3.358 +bind_thm ("Spy_not_see_NB", result() RSN (2, rev_mp) RS mp);
   3.359 +
   3.360 +
   3.361 +
   3.362 +(*Authentication for B: if he receives message 3 and has used NB
   3.363 +  in message 2, then A has sent message 3.*)
   3.364 +goal thy 
   3.365 + "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]       \
   3.366 +\ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \
   3.367 +\     --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs \
   3.368 +\     --> (EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set_of_list evs)";
   3.369 +by (etac ns_public.induct 1);
   3.370 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   3.371 +by (ALLGOALS Asm_simp_tac);
   3.372 +(*NS1*)
   3.373 +by (fast_tac (!claset addSEs partsEs
   3.374 +                      addSDs [new_nonces_not_seen, 
   3.375 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.376 +(*Fake*)
   3.377 +by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   3.378 +by (fast_tac (!claset addss (!simpset)) 1);
   3.379 +br (ccontr RS disjI2) 1;
   3.380 +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   3.381 +by (Fast_tac 1);
   3.382 +(*37 seconds??*)
   3.383 +by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   3.384 +	              addDs  [impOfSubs analz_subset_parts] 
   3.385 +	              addss (!simpset)) 1);
   3.386 +(*NS3*)
   3.387 +by (Step_tac 1);
   3.388 +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT1 (assume_tac 1));
   3.389 +by (Fast_tac 1);
   3.390 +by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.391 +	              addDs  [unique_NB]) 1);
   3.392 +qed_spec_mp "NB_decrypt_imp_A_msg";
   3.393 +
   3.394 +
   3.395 +(*Corollary: if B receives message NS3 and the nonce NB agrees
   3.396 +  then A sent NB to somebody....*)
   3.397 +goal thy 
   3.398 + "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs;    \
   3.399 +\           Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB|})          \
   3.400 +\             : set_of_list evs;                                       \
   3.401 +\           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
   3.402 +\        ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set_of_list evs";
   3.403 +by (fast_tac (!claset addSIs [NB_decrypt_imp_A_msg]
   3.404 +                      addEs  partsEs
   3.405 +                      addDs  [Says_imp_sees_Spy' RS parts.Inj]) 1);
   3.406 +qed "B_trusts_NS3";
   3.407 +
   3.408 +
   3.409 +(*Can we strengthen the secrecy theorem?  NO*)
   3.410 +goal thy 
   3.411 + "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
   3.412 +\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs \
   3.413 +\     --> Nonce NB ~: analz (sees lost Spy evs)";
   3.414 +by (etac ns_public.induct 1);
   3.415 +by (ALLGOALS 
   3.416 +    (asm_simp_tac 
   3.417 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   3.418 +               setloop split_tac [expand_if])));
   3.419 +(*NS1*)
   3.420 +by (fast_tac (!claset addSEs partsEs
   3.421 +                      addSDs [new_nonces_not_seen, 
   3.422 +			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.423 +(*Fake*)
   3.424 +by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
   3.425 +(*NS2 and NS3*)
   3.426 +by (Step_tac 1);
   3.427 +(*NS2*)
   3.428 +by (fast_tac (!claset addSEs partsEs
   3.429 +                      addSDs [new_nonces_not_seen, 
   3.430 +                              Says_imp_sees_Spy' RS parts.Inj]) 2);
   3.431 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   3.432 +                      addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
   3.433 +(*NS3*)
   3.434 +by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1
   3.435 +    THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1));
   3.436 +by (Step_tac 1);
   3.437 +
   3.438 +(*
   3.439 +THIS IS THE ATTACK!
   3.440 +Level 9
   3.441 +!!evs. [| A ~: lost; B ~: lost; evs : ns_public |]
   3.442 +       ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
   3.443 +           : set_of_list evs -->
   3.444 +           Nonce NB ~: analz (sees lost Spy evs)
   3.445 + 1. !!evs Aa Ba B' NAa NBa evsa.
   3.446 +       [| A ~: lost; B ~: lost; evsa : ns_public; A ~= Ba;
   3.447 +          Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evsa;
   3.448 +          Says A Ba (Crypt (pubK Ba) {|Nonce NA, Agent A|}) : set_of_list evsa;
   3.449 +          Ba : lost;
   3.450 +          Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evsa;
   3.451 +          Nonce NB ~: analz (sees lost Spy evsa) |]
   3.452 +       ==> False
   3.453 +*)
   3.454 +
   3.455 +
   3.456 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Dec 05 18:07:27 1996 +0100
     4.3 @@ -0,0 +1,56 @@
     4.4 +(*  Title:      HOL/Auth/NS_Public_Bad
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1996  University of Cambridge
     4.8 +
     4.9 +Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
    4.10 +Flawed version, vulnerable to Lowe's attack.
    4.11 +
    4.12 +From page 260 of
    4.13 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    4.14 +  Proc. Royal Soc. 426 (1989)
    4.15 +*)
    4.16 +
    4.17 +NS_Public_Bad = Public + 
    4.18 +
    4.19 +consts  lost    :: agent set        (*No need for it to be a variable*)
    4.20 +	ns_public  :: event list set
    4.21 +inductive ns_public
    4.22 +  intrs 
    4.23 +         (*Initial trace is empty*)
    4.24 +    Nil  "[]: ns_public"
    4.25 +
    4.26 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    4.27 +           invent new nonces here, but he can also use NS1.  Common to
    4.28 +           all similar protocols.*)
    4.29 +    Fake "[| evs: ns_public;  B ~= Spy;  
    4.30 +             X: synth (analz (sees lost Spy evs)) |]
    4.31 +          ==> Says Spy B X  # evs : ns_public"
    4.32 +
    4.33 +         (*Alice initiates a protocol run, sending a nonce to Bob*)
    4.34 +    NS1  "[| evs: ns_public;  A ~= B |]
    4.35 +          ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs
    4.36 +                : ns_public"
    4.37 +
    4.38 +         (*Bob responds to Alice's message with a further nonce*)
    4.39 +    NS2  "[| evs: ns_public;  A ~= B;
    4.40 +             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
    4.41 +               : set_of_list evs |]
    4.42 +          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs)|}) # evs
    4.43 +                : ns_public"
    4.44 +
    4.45 +         (*Alice proves her existence by sending NB back to Bob.*)
    4.46 +    NS3  "[| evs: ns_public;  A ~= B;
    4.47 +             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    4.48 +               : set_of_list evs;
    4.49 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
    4.50 +               : set_of_list evs |]
    4.51 +          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    4.52 +
    4.53 +  (**Oops message??**)
    4.54 +
    4.55 +rules
    4.56 +  (*Spy has access to his own key for spoof messages*)
    4.57 +  Spy_in_lost "Spy: lost"
    4.58 +
    4.59 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Auth/Public.ML	Thu Dec 05 18:07:27 1996 +0100
     5.3 @@ -0,0 +1,186 @@
     5.4 +(*  Title:      HOL/Auth/Public
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   1996  University of Cambridge
     5.8 +
     5.9 +Theory of Public Keys (common to all symmetric-key protocols)
    5.10 +
    5.11 +Server keys; initial states of agents; new nonces and keys; function "sees" 
    5.12 +*)
    5.13 +
    5.14 +
    5.15 +open Public;
    5.16 +
    5.17 +(*Holds because Friend is injective: thus cannot prove for all f*)
    5.18 +goal thy "(Friend x : Friend``A) = (x:A)";
    5.19 +by (Auto_tac());
    5.20 +qed "Friend_image_eq";
    5.21 +Addsimps [Friend_image_eq];
    5.22 +
    5.23 +Addsimps [Un_insert_left, Un_insert_right];
    5.24 +
    5.25 +(*By default only o_apply is built-in.  But in the presence of eta-expansion
    5.26 +  this means that some terms displayed as (f o g) will be rewritten, and others
    5.27 +  will not!*)
    5.28 +Addsimps [o_def];
    5.29 +
    5.30 +(*** Basic properties of pubK ***)
    5.31 +
    5.32 +(*Injectiveness and freshness of new keys and nonces*)
    5.33 +AddIffs [inj_pubK RS inj_eq];
    5.34 +AddSDs  [newN_length];
    5.35 +
    5.36 +(** Rewrites should not refer to  initState(Friend i) 
    5.37 +    -- not in normal form! **)
    5.38 +
    5.39 +Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym];
    5.40 +
    5.41 +goal thy "Nonce (newN evs) ~: parts (initState lost B)";
    5.42 +by (agent.induct_tac "B" 1);
    5.43 +by (Auto_tac ());
    5.44 +qed "newN_notin_initState";
    5.45 +
    5.46 +AddIffs [newN_notin_initState];
    5.47 +
    5.48 +goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
    5.49 +by (agent.induct_tac "C" 1);
    5.50 +by (auto_tac (!claset addIs [range_eqI], !simpset));
    5.51 +qed "keysFor_parts_initState";
    5.52 +Addsimps [keysFor_parts_initState];
    5.53 +
    5.54 +goalw thy [keysFor_def] "keysFor (Key``E) = {}";
    5.55 +by (Auto_tac ());
    5.56 +qed "keysFor_image_Key";
    5.57 +Addsimps [keysFor_image_Key];
    5.58 +
    5.59 +
    5.60 +(*** Function "sees" ***)
    5.61 +
    5.62 +goal thy
    5.63 +    "!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs";
    5.64 +by (list.induct_tac "evs" 1);
    5.65 +by (agent.induct_tac "A" 1);
    5.66 +by (event.induct_tac "a" 2);
    5.67 +by (Auto_tac ());
    5.68 +qed "sees_mono";
    5.69 +
    5.70 +(*Agents see their own private keys!*)
    5.71 +goal thy "A ~= Spy --> Key (priK A) : sees lost A evs";
    5.72 +by (list.induct_tac "evs" 1);
    5.73 +by (agent.induct_tac "A" 1);
    5.74 +by (Auto_tac ());
    5.75 +qed_spec_mp "sees_own_priK";
    5.76 +
    5.77 +(*All public keys are visible*)
    5.78 +goal thy "Key (pubK A) : sees lost A evs";
    5.79 +by (list.induct_tac "evs" 1);
    5.80 +by (agent.induct_tac "A" 1);
    5.81 +by (Auto_tac ());
    5.82 +qed_spec_mp "sees_pubK";
    5.83 +
    5.84 +(*Spy sees private keys of lost agents!*)
    5.85 +goal thy "!!A. A: lost ==> Key (priK A) : sees lost Spy evs";
    5.86 +by (list.induct_tac "evs" 1);
    5.87 +by (Auto_tac());
    5.88 +qed "Spy_sees_lost";
    5.89 +
    5.90 +AddIffs [sees_pubK];
    5.91 +AddSIs  [sees_own_priK, Spy_sees_lost];
    5.92 +
    5.93 +(*Added for Yahalom/lost_tac*)
    5.94 +goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs);  A: lost |] \
    5.95 +\              ==> X : analz (sees lost Spy evs)";
    5.96 +by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
    5.97 +qed "Crypt_Spy_analz_lost";
    5.98 +
    5.99 +(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
   5.100 +
   5.101 +goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)";
   5.102 +by (Simp_tac 1);
   5.103 +qed "sees_own";
   5.104 +
   5.105 +goal thy "!!A. Server ~= B ==> \
   5.106 +\          sees lost Server (Says A B X # evs) = sees lost Server evs";
   5.107 +by (Asm_simp_tac 1);
   5.108 +qed "sees_Server";
   5.109 +
   5.110 +goal thy "!!A. Friend i ~= B ==> \
   5.111 +\          sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
   5.112 +by (Asm_simp_tac 1);
   5.113 +qed "sees_Friend";
   5.114 +
   5.115 +goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)";
   5.116 +by (Simp_tac 1);
   5.117 +qed "sees_Spy";
   5.118 +
   5.119 +goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
   5.120 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   5.121 +by (Fast_tac 1);
   5.122 +qed "sees_Says_subset_insert";
   5.123 +
   5.124 +goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
   5.125 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   5.126 +by (Fast_tac 1);
   5.127 +qed "sees_subset_sees_Says";
   5.128 +
   5.129 +(*Pushing Unions into parts.  One of the agents A is B, and thus sees Y.
   5.130 +  Once used to prove new_keys_not_seen; now obsolete.*)
   5.131 +goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
   5.132 +\         parts {Y} Un (UN A. parts (sees lost A evs))";
   5.133 +by (Step_tac 1);
   5.134 +by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
   5.135 +by (ALLGOALS
   5.136 +    (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] 
   5.137 +                       setloop split_tac [expand_if]))));
   5.138 +qed "UN_parts_sees_Says";
   5.139 +
   5.140 +goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
   5.141 +by (list.induct_tac "evs" 1);
   5.142 +by (Auto_tac ());
   5.143 +qed_spec_mp "Says_imp_sees_Spy";
   5.144 +
   5.145 +goal thy  
   5.146 + "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs;  C : lost |] \
   5.147 +\        ==> X : analz (sees lost Spy evs)";
   5.148 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   5.149 +                      addss (!simpset)) 1);
   5.150 +qed "Says_Crypt_lost";
   5.151 +
   5.152 +goal thy  
   5.153 + "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs;        \
   5.154 +\           X ~: analz (sees lost Spy evs) |]                     \
   5.155 +\        ==> C ~: lost";
   5.156 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   5.157 +                      addss (!simpset)) 1);
   5.158 +qed "Says_Crypt_not_lost";
   5.159 +
   5.160 +Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
   5.161 +Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)
   5.162 +
   5.163 +
   5.164 +(** Power of the Spy **)
   5.165 +
   5.166 +(*The Spy can see more than anybody else, except for their initial state*)
   5.167 +goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs";
   5.168 +by (list.induct_tac "evs" 1);
   5.169 +by (event.induct_tac "a" 2);
   5.170 +by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
   5.171 +                                addss (!simpset))));
   5.172 +qed "sees_agent_subset_sees_Spy";
   5.173 +
   5.174 +(*The Spy can see more than anybody else who's lost their key!*)
   5.175 +goal thy "A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
   5.176 +by (list.induct_tac "evs" 1);
   5.177 +by (event.induct_tac "a" 2);
   5.178 +by (agent.induct_tac "A" 1);
   5.179 +by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
   5.180 +qed_spec_mp "sees_lost_agent_subset_sees_Spy";
   5.181 +
   5.182 +
   5.183 +(** Simplifying   parts (insert X (sees lost A evs))
   5.184 +      = parts {X} Un parts (sees lost A evs) -- since general case loops*)
   5.185 +
   5.186 +val parts_insert_sees = 
   5.187 +    parts_insert |> read_instantiate_sg (sign_of thy)
   5.188 +                                        [("H", "sees lost A evs")]
   5.189 +                 |> standard;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Auth/Public.thy	Thu Dec 05 18:07:27 1996 +0100
     6.3 @@ -0,0 +1,66 @@
     6.4 +(*  Title:      HOL/Auth/Public
     6.5 +    ID:         $Id$
     6.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 +    Copyright   1996  University of Cambridge
     6.8 +
     6.9 +Theory of Public Keys (common to all symmetric-key protocols)
    6.10 +
    6.11 +Server keys; initial states of agents; new nonces and keys; function "sees" 
    6.12 +*)
    6.13 +
    6.14 +Public = Message + List + 
    6.15 +
    6.16 +consts
    6.17 +  pubK    :: agent => key
    6.18 +
    6.19 +syntax
    6.20 +  priK    :: agent => key
    6.21 +
    6.22 +translations
    6.23 +  "priK x"  == "invKey(pubK x)"
    6.24 +
    6.25 +consts  (*Initial states of agents -- parameter of the construction*)
    6.26 +  initState :: [agent set, agent] => msg set
    6.27 +
    6.28 +primrec initState agent
    6.29 +        (*Agents know their private key and all public keys*)
    6.30 +  initState_Server  "initState lost Server     =    
    6.31 + 		         insert (Key (priK Server)) (Key `` range pubK)"
    6.32 +  initState_Friend  "initState lost (Friend i) =    
    6.33 + 		         insert (Key (priK (Friend i))) (Key `` range pubK)"
    6.34 +  initState_Spy     "initState lost Spy        =    
    6.35 + 		         (Key``invKey``pubK``lost) Un (Key `` range pubK)"
    6.36 +
    6.37 +
    6.38 +datatype  (*Messages, and components of agent stores*)
    6.39 +  event = Says agent agent msg
    6.40 +
    6.41 +consts  
    6.42 +  sees1 :: [agent, event] => msg set
    6.43 +
    6.44 +primrec sees1 event
    6.45 +           (*Spy reads all traffic whether addressed to him or not*)
    6.46 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    6.47 +
    6.48 +consts  
    6.49 +  sees :: [agent set, agent, event list] => msg set
    6.50 +
    6.51 +primrec sees list
    6.52 +  sees_Nil  "sees lost A []       = initState lost A"
    6.53 +  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
    6.54 +
    6.55 +
    6.56 +(*Agents generate "random" nonces.  These are uniquely determined by
    6.57 +  the length of their argument, a trace.*)
    6.58 +consts
    6.59 +  newN :: "event list => nat"
    6.60 +
    6.61 +rules
    6.62 +
    6.63 +  (*Public keys are disjoint, and never clash with private keys*)
    6.64 +  inj_pubK      "inj pubK"
    6.65 +  priK_neq_pubK "priK A ~= pubK B"
    6.66 +
    6.67 +  newN_length   "(newN evs = newN evt) ==> (length evs = length evt)"
    6.68 +
    6.69 +end