src/HOL/Auth/NS_Shared.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_Shared
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
     7 
     8 From page 247 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    12 
    13 open NS_Shared;
    14 
    15 proof_timing:=true;
    16 HOL_quantifiers := false;
    17 
    18 (*Replacing the variable by a constant improves search speed by 50%!*)
    19 val Says_imp_sees_Spy' = read_instantiate [("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; A ~= Server; B ~= Server |]       \
    25 \        ==> EX N K. EX evs: ns_shared lost.          \
    26 \               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
    27 by (REPEAT (resolve_tac [exI,bexI] 1));
    28 by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
    29           ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
    30 by possibility_tac;
    31 result();
    32 
    33 
    34 (**** Inductive proofs about ns_shared ****)
    35 
    36 (*Monotonicity*)
    37 goal thy "!!evs. lost' <= lost ==> ns_shared lost' <= ns_shared lost";
    38 by (rtac subsetI 1);
    39 by (etac ns_shared.induct 1);
    40 by (REPEAT_FIRST
    41     (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    42                               :: ns_shared.intrs))));
    43 qed "ns_shared_mono";
    44 
    45 
    46 (*Nobody sends themselves messages*)
    47 goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set evs";
    48 by (etac ns_shared.induct 1);
    49 by (Auto_tac());
    50 qed_spec_mp "not_Says_to_self";
    51 Addsimps [not_Says_to_self];
    52 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    53 
    54 (*For reasoning about the encrypted portion of message NS3*)
    55 goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
    56 \                ==> X : parts (sees lost Spy evs)";
    57 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    58 qed "NS3_msg_in_parts_sees_Spy";
    59                               
    60 goal thy
    61     "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
    62 \           ==> K : parts (sees lost Spy evs)";
    63 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    64 qed "Oops_parts_sees_Spy";
    65 
    66 (*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    67   We instantiate the variable to "lost" since leaving it as a Var would
    68   interfere with simplification.*)
    69 val parts_induct_tac = 
    70     etac ns_shared.induct 1  THEN 
    71     dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5  THEN
    72     forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8  THEN
    73     prove_simple_subgoals_tac 1;
    74 
    75 
    76 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    77     sends messages containing X! **)
    78 
    79 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    80 goal thy 
    81  "!!evs. evs : ns_shared lost \
    82 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    83 by parts_induct_tac;
    84 by (Fake_parts_insert_tac 1);
    85 by (Blast_tac 1);
    86 qed "Spy_see_shrK";
    87 Addsimps [Spy_see_shrK];
    88 
    89 goal thy 
    90  "!!evs. evs : ns_shared lost \
    91 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    92 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    93 qed "Spy_analz_shrK";
    94 Addsimps [Spy_analz_shrK];
    95 
    96 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    97 \                  evs : ns_shared lost |] ==> A:lost";
    98 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    99 qed "Spy_see_shrK_D";
   100 
   101 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   102 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   103 
   104 
   105 (*Nobody can have used non-existent keys!*)
   106 goal thy "!!evs. evs : ns_shared lost ==>      \
   107 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   108 by parts_induct_tac;
   109 (*Fake*)
   110 by (best_tac
   111       (!claset addIs [impOfSubs analz_subset_parts]
   112                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   113                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   114                addss (!simpset)) 1);
   115 (*NS2, NS4, NS5*)
   116 by (ALLGOALS (blast_tac (!claset addSEs sees_Spy_partsEs)));
   117 qed_spec_mp "new_keys_not_used";
   118 
   119 bind_thm ("new_keys_not_analzd",
   120           [analz_subset_parts RS keysFor_mono,
   121            new_keys_not_used] MRS contra_subsetD);
   122 
   123 Addsimps [new_keys_not_used, new_keys_not_analzd];
   124 
   125 
   126 (** Lemmas concerning the form of items passed in messages **)
   127 
   128 (*Describes the form of K, X and K' when the Server sends this message.*)
   129 goal thy 
   130  "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
   131 \             : set evs;                                      \
   132 \           evs : ns_shared lost |]                           \
   133 \        ==> K ~: range shrK &                                \
   134 \            X = (Crypt (shrK B) {|Key K, Agent A|}) &        \
   135 \            K' = shrK A";
   136 by (etac rev_mp 1);
   137 by (etac ns_shared.induct 1);
   138 by (Auto_tac());
   139 qed "Says_Server_message_form";
   140 
   141 
   142 (*If the encrypted message appears then it originated with the Server*)
   143 goal thy
   144  "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|}                   \
   145 \            : parts (sees lost Spy evs);                              \
   146 \           A ~: lost;  evs : ns_shared lost |]                        \
   147 \         ==> X = (Crypt (shrK B) {|Key K, Agent A|}) &                \
   148 \             Says Server A                                            \
   149 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   150 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   151 \             : set evs";
   152 by (etac rev_mp 1);
   153 by parts_induct_tac;
   154 by (Fake_parts_insert_tac 1);
   155 by (Auto_tac());
   156 qed "A_trusts_NS2";
   157 
   158 
   159 (*EITHER describes the form of X when the following message is sent, 
   160   OR     reduces it to the Fake case.
   161   Use Says_Server_message_form if applicable.*)
   162 goal thy 
   163  "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
   164 \            : set evs;          evs : ns_shared lost |]                   \
   165 \        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
   166 \            | X : analz (sees lost Spy evs)";
   167 by (case_tac "A : lost" 1);
   168 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]
   169                       addss (!simpset)) 1);
   170 by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
   171 by (blast_tac (!claset addEs  partsEs
   172                       addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
   173 qed "Says_S_message_form";
   174 
   175 
   176 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   177 val analz_sees_tac = 
   178     forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
   179     forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN 
   180     REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
   181 
   182 
   183 (****
   184  The following is to prove theorems of the form
   185 
   186   Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   187   Key K : analz (sees lost Spy evs)
   188 
   189  A more general formula must be proved inductively.
   190 
   191 ****)
   192 
   193 
   194 (*NOT useful in this form, but it says that session keys are not used
   195   to encrypt messages containing other keys, in the actual protocol.
   196   We require that agents should behave like this subsequently also.*)
   197 goal thy 
   198  "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==>  \
   199 \           (Crypt KAB X) : parts (sees lost Spy evs) &      \
   200 \           Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   201 by parts_induct_tac;
   202 (*Deals with Faked messages*)
   203 by (blast_tac (!claset addSEs partsEs
   204                        addDs [impOfSubs parts_insert_subset_Un]) 1);
   205 (*Base, NS4 and NS5*)
   206 by (Auto_tac());
   207 result();
   208 
   209 
   210 (** Session keys are not used to encrypt other session keys **)
   211 
   212 (*The equality makes the induction hypothesis easier to apply*)
   213 goal thy  
   214  "!!evs. evs : ns_shared lost ==>                                \
   215 \  ALL K KK. KK <= Compl (range shrK) -->                        \
   216 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
   217 \            (K : KK | Key K : analz (sees lost Spy evs))";
   218 by (etac ns_shared.induct 1);
   219 by analz_sees_tac;
   220 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   221 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   222 (*Takes 24 secs*)
   223 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   224 (*Fake*) 
   225 by (spy_analz_tac 2);
   226 (*Base*)
   227 by (Blast_tac 1);
   228 qed_spec_mp "analz_image_freshK";
   229 
   230 
   231 goal thy
   232  "!!evs. [| evs : ns_shared lost;  KAB ~: range shrK |] ==>     \
   233 \        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   234 \        (K = KAB | Key K : analz (sees lost Spy evs))";
   235 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   236 qed "analz_insert_freshK";
   237 
   238 
   239 (** The session key K uniquely identifies the message **)
   240 
   241 goal thy 
   242  "!!evs. evs : ns_shared lost ==>                                        \
   243 \      EX A' NA' B' X'. ALL A NA B X.                                    \
   244 \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
   245 \       : set evs -->         A=A' & NA=NA' & B=B' & X=X'";
   246 by (etac ns_shared.induct 1);
   247 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   248 by (Step_tac 1);
   249 (*NS3*)
   250 by (ex_strip_tac 2);
   251 by (Blast_tac 2);
   252 (*NS2: it can't be a new key*)
   253 by (expand_case_tac "K = ?y" 1);
   254 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   255 by (blast_tac (!claset delrules [conjI]    (*prevent split-up into 4 subgoals*)
   256                       addSEs sees_Spy_partsEs) 1);
   257 val lemma = result();
   258 
   259 (*In messages of this form, the session key uniquely identifies the rest*)
   260 goal thy 
   261  "!!evs. [| Says Server A                                    \
   262 \             (Crypt (shrK A) {|NA, Agent B, Key K, X|})     \
   263 \                  : set evs;                                \ 
   264 \           Says Server A'                                   \
   265 \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
   266 \                  : set evs;                                \
   267 \           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
   268 by (prove_unique_tac lemma 1);
   269 qed "unique_session_keys";
   270 
   271 
   272 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   273 
   274 goal thy 
   275  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_shared lost |]            \
   276 \        ==> Says Server A                                             \
   277 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   278 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   279 \             : set evs -->                                            \
   280 \        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) -->         \
   281 \        Key K ~: analz (sees lost Spy evs)";
   282 by (etac ns_shared.induct 1);
   283 by analz_sees_tac;
   284 by (ALLGOALS 
   285     (asm_simp_tac 
   286      (!simpset addsimps ([analz_insert_eq, not_parts_not_analz, 
   287 			  analz_insert_freshK] @ pushes)
   288                setloop split_tac [expand_if])));
   289 (*Oops*)
   290 by (blast_tac (!claset addDs [unique_session_keys]) 5);
   291 (*NS4*) 
   292 by (Blast_tac 4);
   293 (*NS2*)
   294 by (blast_tac (!claset addSEs sees_Spy_partsEs
   295                        addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
   296 (*Fake*) 
   297 by (spy_analz_tac 1);
   298 (*NS3*) (**LEVEL 6 **)
   299 by (step_tac (!claset delrules [impCE]) 1);
   300 by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1);
   301 by (assume_tac 2);
   302 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
   303 			      Crypt_Spy_analz_lost]) 1);
   304 by (blast_tac (!claset addDs [unique_session_keys]) 1);
   305 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   306 
   307 
   308 (*Final version: Server's message in the most abstract form*)
   309 goal thy 
   310  "!!evs. [| Says Server A                                               \
   311 \            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
   312 \           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
   313 \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
   314 \        |] ==> Key K ~: analz (sees lost Spy evs)";
   315 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   316 by (blast_tac (!claset addSDs [lemma]) 1);
   317 qed "Spy_not_see_encrypted_key";
   318 
   319 
   320 goal thy 
   321  "!!evs. [| C ~: {A,B,Server};                                          \
   322 \           Says Server A                                               \
   323 \            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
   324 \           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
   325 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
   326 \        ==> Key K ~: analz (sees lost C evs)";
   327 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   328 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   329 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   330 by (REPEAT_FIRST (blast_tac (!claset addIs [ns_shared_mono RS subsetD])));
   331 qed "Agent_not_see_encrypted_key";
   332 
   333 
   334 
   335 (**** Guarantees available at various stages of protocol ***)
   336 
   337 A_trusts_NS2 RS conjunct2 RS Spy_not_see_encrypted_key;
   338 
   339 
   340 (*If the encrypted message appears then it originated with the Server*)
   341 goal thy
   342  "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees lost Spy evs); \
   343 \           B ~: lost;  evs : ns_shared lost |]                        \
   344 \         ==> EX NA. Says Server A                                     \
   345 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   346 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   347 \             : set evs";
   348 by (etac rev_mp 1);
   349 by parts_induct_tac;
   350 by (Fake_parts_insert_tac 1);
   351 (*Fake case*)
   352 by (ALLGOALS Blast_tac);
   353 qed "B_trusts_NS3";
   354 
   355 
   356 goal thy
   357  "!!evs. [| B ~: lost;  evs : ns_shared lost |]                        \
   358 \        ==> Key K ~: analz (sees lost Spy evs) -->                    \
   359 \            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   360 \            : set evs -->                                             \
   361 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->        \
   362 \            Says B A (Crypt K (Nonce NB)) : set evs";
   363 by (etac ns_shared.induct 1);
   364 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   365 by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5);
   366 by (forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8);
   367 by (TRYALL (rtac impI));
   368 by (REPEAT_FIRST
   369     (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   370 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   371 (**LEVEL 7**)
   372 by (blast_tac (!claset addSDs [Crypt_Fake_parts_insert]
   373                        addDs [impOfSubs analz_subset_parts]) 1);
   374 by (Blast_tac 2);
   375 by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
   376 (*Subgoal 1: contradiction from the assumptions  
   377   Key K ~: used evsa  and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *)
   378 by (dtac Crypt_imp_invKey_keysFor 1);
   379 (**LEVEL 11**)
   380 by (Asm_full_simp_tac 1);
   381 by (rtac disjI1 1);
   382 by (thin_tac "?PP-->?QQ" 1);
   383 by (case_tac "Ba : lost" 1);
   384 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS B_trusts_NS3, 
   385 			      unique_session_keys]) 2);
   386 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
   387 			      Crypt_Spy_analz_lost]) 1);
   388 val lemma = result();
   389 
   390 goal thy
   391  "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
   392 \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   393 \           : set evs;                                                \
   394 \           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;          \
   395 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
   396 \        ==> Says B A (Crypt K (Nonce NB)) : set evs";
   397 by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
   398                        addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
   399 qed "A_trusts_NS4";