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