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