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