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