src/HOL/Auth/NS_Public.ML
author paulson
Fri Jan 17 12:49:31 1997 +0100 (1997-01-17)
changeset 2516 4d68fbe6378b
parent 2497 47de509bdd55
child 2536 1e04eb7f7eb1
permissions -rw-r--r--
Now with Andy Gordon's treatment of freshness to replace newN/K
     1 (*  Title:      HOL/Auth/NS_Public
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
     7 Version incorporating Lowe's fix (inclusion of B's identify in round 2).
     8 *)
     9 
    10 open NS_Public;
    11 
    12 proof_timing:=true;
    13 HOL_quantifiers := false;
    14 
    15 AddIffs [Spy_in_lost];
    16 
    17 (*Replacing the variable by a constant improves search speed by 50%!*)
    18 val Says_imp_sees_Spy' = 
    19     read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
    20 
    21 
    22 (*A "possibility property": there are traces that reach the end*)
    23 goal thy 
    24  "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
    25 \                     Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
    26 by (REPEAT (resolve_tac [exI,bexI] 1));
    27 by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
    28 by possibility_tac;
    29 result();
    30 
    31 
    32 (**** Inductive proofs about ns_public ****)
    33 
    34 (*Nobody sends themselves messages*)
    35 goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs";
    36 by (etac ns_public.induct 1);
    37 by (Auto_tac());
    38 qed_spec_mp "not_Says_to_self";
    39 Addsimps [not_Says_to_self];
    40 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    41 
    42 
    43 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    44 fun parts_induct_tac i = SELECT_GOAL
    45     (DETERM (etac ns_public.induct 1 THEN 
    46              (*Fake message*)
    47              TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    48                                            impOfSubs Fake_parts_insert]
    49                                     addss (!simpset)) 2)) THEN
    50      (*Base case*)
    51      fast_tac (!claset addss (!simpset)) 1 THEN
    52      ALLGOALS Asm_simp_tac) i;
    53 
    54 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    55     sends messages containing X! **)
    56 
    57 (*Spy never sees another agent's private key! (unless it's lost at start)*)
    58 goal thy 
    59  "!!evs. evs : ns_public \
    60 \        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
    61 by (parts_induct_tac 1);
    62 by (Auto_tac());
    63 qed "Spy_see_priK";
    64 Addsimps [Spy_see_priK];
    65 
    66 goal thy 
    67  "!!evs. evs : ns_public \
    68 \        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
    69 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    70 qed "Spy_analz_priK";
    71 Addsimps [Spy_analz_priK];
    72 
    73 goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
    74 \                  evs : ns_public |] ==> A:lost";
    75 by (fast_tac (!claset addDs [Spy_see_priK]) 1);
    76 qed "Spy_see_priK_D";
    77 
    78 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
    79 AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
    80 
    81 
    82 fun analz_induct_tac i = 
    83     etac ns_public.induct i     THEN
    84     ALLGOALS (asm_simp_tac 
    85               (!simpset addsimps [not_parts_not_analz]
    86                         setloop split_tac [expand_if]));
    87 
    88 (**** Authenticity properties obtained from NS2 ****)
    89 
    90 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
    91   is secret.  (Honest users generate fresh nonces.)*)
    92 goal thy 
    93  "!!evs. evs : ns_public                       \
    94 \ ==> Nonce NA ~: analz (sees lost Spy evs) -->           \
    95 \     Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
    96 \     Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (sees lost Spy evs)";
    97 by (analz_induct_tac 1);
    98 (*NS3*)
    99 by (fast_tac (!claset addSEs partsEs) 4);
   100 (*NS2*)
   101 by (fast_tac (!claset addSEs partsEs) 3);
   102 (*Fake*)
   103 by (best_tac (!claset addIs [analz_insertI]
   104                       addDs [impOfSubs analz_subset_parts,
   105                              impOfSubs Fake_parts_insert]
   106                       addss (!simpset)) 2);
   107 (*Base*)
   108 by (fast_tac (!claset addss (!simpset)) 1);
   109 bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
   110 
   111 
   112 (*Unicity for NS1: nonce NA identifies agents A and B*)
   113 goal thy 
   114  "!!evs. evs : ns_public                                                    \
   115 \ ==> Nonce NA ~: analz (sees lost Spy evs) -->                             \
   116 \     (EX A' B'. ALL A B.                                                   \
   117 \      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
   118 \      A=A' & B=B')";
   119 by (analz_induct_tac 1);
   120 (*NS1*)
   121 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
   122 by (expand_case_tac "NA = ?y" 3 THEN
   123     REPEAT (fast_tac (!claset addSEs partsEs) 3));
   124 (*Base*)
   125 by (fast_tac (!claset addss (!simpset)) 1);
   126 (*Fake*)
   127 by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
   128 by (step_tac (!claset addSIs [analz_insertI]) 1);
   129 by (ex_strip_tac 1);
   130 by (best_tac (!claset delrules [conjI]
   131                       addSDs [impOfSubs Fake_parts_insert]
   132                       addDs  [impOfSubs analz_subset_parts]
   133                       addss (!simpset)) 1);
   134 val lemma = result();
   135 
   136 goal thy 
   137  "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(sees lost Spy evs); \
   138 \           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \
   139 \           Nonce NA ~: analz (sees lost Spy evs);                            \
   140 \           evs : ns_public |]                                                \
   141 \        ==> A=A' & B=B'";
   142 by (prove_unique_tac lemma 1);
   143 qed "unique_NA";
   144 
   145 
   146 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
   147 goal thy 
   148  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
   149 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \
   150 \     --> Nonce NA ~: analz (sees lost Spy evs)";
   151 by (analz_induct_tac 1);
   152 (*NS3*)
   153 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   154                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
   155 (*NS1*)
   156 by (fast_tac (!claset addSEs partsEs
   157                       addSDs [Says_imp_sees_Spy' RS parts.Inj]
   158                       addIs  [impOfSubs analz_subset_parts]) 2);
   159 (*Fake*)
   160 by (spy_analz_tac 1);
   161 (*NS2*)
   162 by (Step_tac 1);
   163 by (fast_tac (!claset addSEs partsEs
   164                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   165 (*14 seconds.  Much slower still if one tries to prove all NS2 in one step.*)
   166 by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   167                       addDs  [unique_NA]) 1);
   168 bind_thm ("Spy_not_see_NA", result() RSN (2, rev_mp));
   169 
   170 
   171 (*Authentication for A: if she receives message 2 and has used NA
   172   to start a run, then B has sent message 2.*)
   173 goal thy 
   174  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]       \
   175 \ ==> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}         \
   176 \                                : parts (sees lost Spy evs) \
   177 \     --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \
   178 \     --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})         \
   179 \           : set_of_list evs";
   180 by (etac ns_public.induct 1);
   181 by (ALLGOALS Asm_simp_tac);
   182 (*NS1*)
   183 by (fast_tac (!claset addSEs partsEs
   184                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   185 (*Fake*)
   186 by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   187 by (fast_tac (!claset addss (!simpset)) 1);
   188 by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
   189 by (best_tac (!claset addSIs [disjI2]
   190                       addSDs [impOfSubs Fake_parts_insert]
   191                       addDs  [impOfSubs analz_subset_parts]
   192                       addss (!simpset)) 1);
   193 qed_spec_mp "NA_decrypt_imp_B_msg";
   194 
   195 (*Corollary: if A receives B's message NS2 and the nonce NA agrees
   196   then that message really originated with B.*)
   197 goal thy 
   198  "!!evs. [| Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   199 \             : set_of_list evs;\
   200 \           Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\
   201 \           A ~: lost;  B ~: lost;  evs : ns_public |]  \
   202 \        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   203 \              : set_of_list evs";
   204 by (fast_tac (!claset addSIs [NA_decrypt_imp_B_msg]
   205                       addEs  partsEs
   206                       addDs  [Says_imp_sees_Spy' RS parts.Inj]) 1);
   207 qed "A_trusts_NS2";
   208 
   209 (*If the encrypted message appears then it originated with Alice in NS1*)
   210 goal thy 
   211  "!!evs. evs : ns_public                   \
   212 \    ==> Nonce NA ~: analz (sees lost Spy evs) --> \
   213 \        Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \
   214 \        Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
   215 by (analz_induct_tac 1);
   216 (*Fake*)
   217 by (best_tac (!claset addSIs [disjI2]
   218                       addSDs [impOfSubs Fake_parts_insert]
   219                       addIs  [analz_insertI]
   220                       addDs  [impOfSubs analz_subset_parts]
   221                       addss (!simpset)) 2);
   222 (*Base*)
   223 by (fast_tac (!claset addss (!simpset)) 1);
   224 qed_spec_mp "B_trusts_NS1";
   225 
   226 
   227 
   228 (**** Authenticity properties obtained from NS2 ****)
   229 
   230 (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B 
   231   [unicity of B makes Lowe's fix work]
   232   [proof closely follows that for unique_NA] *)
   233 goal thy 
   234  "!!evs. evs : ns_public                                                    \
   235 \ ==> Nonce NB ~: analz (sees lost Spy evs) -->                             \
   236 \     (EX A' NA' B'. ALL A NA B.                                            \
   237 \      Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}   \
   238 \        : parts (sees lost Spy evs)  -->  A=A' & NA=NA' & B=B')";
   239 by (analz_induct_tac 1);
   240 (*NS2*)
   241 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
   242 by (expand_case_tac "NB = ?y" 3 THEN
   243     REPEAT (fast_tac (!claset addSEs partsEs) 3));
   244 (*Base*)
   245 by (fast_tac (!claset addss (!simpset)) 1);
   246 (*Fake*)
   247 by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
   248 by (step_tac (!claset addSIs [analz_insertI]) 1);
   249 by (ex_strip_tac 1);
   250 by (best_tac (!claset delrules [conjI]
   251                       addSDs [impOfSubs Fake_parts_insert]
   252                       addDs  [impOfSubs analz_subset_parts] 
   253                       addss (!simpset)) 1);
   254 val lemma = result();
   255 
   256 goal thy 
   257  "!!evs. [| Crypt(pubK A)  {|Nonce NA, Nonce NB, Agent B|}   \
   258 \             : parts(sees lost Spy evs);                    \
   259 \           Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
   260 \             : parts(sees lost Spy evs);                    \
   261 \           Nonce NB ~: analz (sees lost Spy evs);           \
   262 \           evs : ns_public |]                               \
   263 \        ==> A=A' & NA=NA' & B=B'";
   264 by (prove_unique_tac lemma 1);
   265 qed "unique_NB";
   266 
   267 
   268 (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
   269 goal thy 
   270  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
   271 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   272 \       : set_of_list evs \
   273 \     --> Nonce NB ~: analz (sees lost Spy evs)";
   274 by (analz_induct_tac 1);
   275 (*NS3*)
   276 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   277                       addDs  [unique_NB]) 4);
   278 (*NS1*)
   279 by (fast_tac (!claset addSEs partsEs
   280                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   281 (*Fake*)
   282 by (spy_analz_tac 1);
   283 (*NS2*)
   284 by (Step_tac 1);
   285 by (fast_tac (!claset addSEs partsEs
   286                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 3);
   287 by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   288                       addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
   289 by (fast_tac (!claset addIs  [impOfSubs analz_subset_parts]) 1);
   290 bind_thm ("Spy_not_see_NB", result() RSN (2, rev_mp));
   291 
   292 
   293 (*Matches only NS2, not NS1 (or NS3)*)
   294 val Says_imp_sees_Spy'' = 
   295     read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy';
   296 
   297 
   298 (*Authentication for B: if he receives message 3 and has used NB
   299   in message 2, then A has sent message 3.*)
   300 goal thy 
   301  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]       \
   302 \ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \
   303 \     --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   304 \       : set_of_list evs \
   305 \     --> Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
   306 by (etac ns_public.induct 1);
   307 by (ALLGOALS Asm_simp_tac);
   308 (*NS1*)
   309 by (fast_tac (!claset addSEs partsEs
   310                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   311 (*Fake*)
   312 by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   313 by (fast_tac (!claset addss (!simpset)) 1);
   314 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   315 by (best_tac (!claset addSIs [disjI2]
   316                       addSDs [impOfSubs Fake_parts_insert]
   317                       addDs  [impOfSubs analz_subset_parts] 
   318                       addss (!simpset)) 1);
   319 (*NS3*)
   320 by (Step_tac 1);
   321 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   322 by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
   323                       addDs  [unique_NB]) 1);
   324 qed_spec_mp "NB_decrypt_imp_A_msg";
   325 
   326 (*Corollary: if B receives message NS3 and the nonce NB agrees,
   327   then that message really originated with A.*)
   328 goal thy 
   329  "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs;    \
   330 \           Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   331 \             : set_of_list evs;                                       \
   332 \           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
   333 \        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
   334 by (fast_tac (!claset addSIs [NB_decrypt_imp_A_msg]
   335                       addEs  partsEs
   336                       addDs  [Says_imp_sees_Spy' RS parts.Inj]) 1);
   337 qed "B_trusts_NS3";
   338 
   339 
   340 (**** Overall guarantee for B*)
   341 
   342 (*If B receives NS3 and the nonce NB agrees with the nonce he joined with
   343   NA, then A initiated the run using NA.
   344   SAME PROOF AS NB_decrypt_imp_A_msg*)
   345 goal thy 
   346  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]       \
   347 \ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \
   348 \     --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   349 \       : set_of_list evs \
   350 \     --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
   351 by (etac ns_public.induct 1);
   352 by (ALLGOALS Asm_simp_tac);
   353 (*Fake, NS2, NS3*)
   354 (*NS1*)
   355 by (fast_tac (!claset addSEs partsEs
   356                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
   357 (*Fake*)
   358 by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   359 by (fast_tac (!claset addss (!simpset)) 1);
   360 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   361 by (best_tac (!claset addSIs [disjI2]
   362                       addDs [impOfSubs analz_subset_parts,
   363                              impOfSubs Fake_parts_insert]
   364                       addss (!simpset)) 1);
   365 (*NS3*)
   366 by (Step_tac 1);
   367 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   368 by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj]
   369                       addDs  [unique_NB]) 1);
   370 val lemma = result() RSN (2, rev_mp) RSN (2, rev_mp);
   371 
   372 goal thy 
   373  "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs;    \
   374 \           Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   375 \             : set_of_list evs;                                       \
   376 \           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
   377 \    ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs";
   378 by (fast_tac (!claset addSIs [lemma]
   379                       addEs  partsEs
   380                       addDs  [Says_imp_sees_Spy' RS parts.Inj]) 1);
   381 qed_spec_mp "B_trusts_protocol";
   382