src/HOL/Auth/NS_Shared.ML
author paulson
Wed May 07 13:01:43 1997 +0200 (1997-05-07)
changeset 3121 cbb6c0c1c58a
parent 2637 e9b203f854ae
child 3441 6d2887123fa0
permissions -rw-r--r--
Conversion to use blast_tac (with other improvements)
     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_of_list 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_of_list 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_of_list 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_of_list 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_of_list 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_of_list 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_of_list 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 (*NS4, Fake*) 
   225 by (EVERY (map spy_analz_tac [3,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_of_list 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_of_list evs;                        \ 
   264 \           Says Server A'                                   \
   265 \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
   266 \                  : set_of_list 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_of_list evs -->                                    \
   280 \        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list 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 ([not_parts_not_analz, analz_insert_freshK] @ pushes)
   287                setloop split_tac [expand_if])));
   288 (*NS4, Fake*) 
   289 by (EVERY (map spy_analz_tac [4,1]));
   290 (*NS2*)
   291 by (blast_tac (!claset addSEs sees_Spy_partsEs
   292                        addIs [parts_insertI, impOfSubs analz_subset_parts]) 1);
   293 (*Oops*)
   294 by (blast_tac (!claset addDs [unique_session_keys]) 2);
   295 (*NS3*) (**LEVEL 6 **)
   296 by (step_tac (!claset delrules [impCE]) 1);
   297 by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1);
   298 by (assume_tac 2);
   299 by (blast_tac (!claset addSDs [Says_Crypt_not_lost]) 1);
   300 by (blast_tac (!claset addDs [unique_session_keys]) 1);
   301 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   302 
   303 
   304 (*Final version: Server's message in the most abstract form*)
   305 goal thy 
   306  "!!evs. [| Says Server A                                               \
   307 \            (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs;    \
   308 \           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs);  \
   309 \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
   310 \        |] ==> Key K ~: analz (sees lost Spy evs)";
   311 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   312 by (blast_tac (!claset addSDs [lemma]) 1);
   313 qed "Spy_not_see_encrypted_key";
   314 
   315 
   316 goal thy 
   317  "!!evs. [| C ~: {A,B,Server};                                          \
   318 \           Says Server A                                               \
   319 \            (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs;    \
   320 \           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs);  \
   321 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
   322 \        ==> Key K ~: analz (sees lost C evs)";
   323 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   324 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   325 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   326 by (REPEAT_FIRST (blast_tac (!claset addIs [ns_shared_mono RS subsetD])));
   327 qed "Agent_not_see_encrypted_key";
   328 
   329 
   330 
   331 (**** Guarantees available at various stages of protocol ***)
   332 
   333 A_trusts_NS2 RS conjunct2 RS Spy_not_see_encrypted_key;
   334 
   335 
   336 (*If the encrypted message appears then it originated with the Server*)
   337 goal thy
   338  "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees lost Spy evs); \
   339 \           B ~: lost;  evs : ns_shared lost |]                        \
   340 \         ==> EX NA. Says Server A                                     \
   341 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   342 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   343 \             : set_of_list evs";
   344 by (etac rev_mp 1);
   345 by parts_induct_tac;
   346 by (Fake_parts_insert_tac 1);
   347 (*Fake case*)
   348 by (ALLGOALS Blast_tac);
   349 qed "B_trusts_NS3";
   350 
   351 
   352 goal thy
   353  "!!evs. [| B ~: lost;  evs : ns_shared lost |]            \
   354 \        ==> Key K ~: analz (sees lost Spy evs) -->             \
   355 \            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   356 \            : set_of_list evs --> \
   357 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->            \
   358 \            Says B A (Crypt K (Nonce NB)) : set_of_list evs";
   359 by (etac ns_shared.induct 1);
   360 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   361 by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5);
   362 by (forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8);
   363 by (TRYALL (rtac impI));
   364 by (REPEAT_FIRST
   365     (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   366 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   367 (**LEVEL 7**)
   368 by (blast_tac (!claset addSDs [Crypt_Fake_parts_insert]
   369                        addDs [impOfSubs analz_subset_parts]) 1);
   370 by (Blast_tac 2);
   371 by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
   372 (*Subgoal 1: contradiction from the assumptions  
   373   Key K ~: used evsa  and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *)
   374 by (dtac Crypt_imp_invKey_keysFor 1);
   375 (**LEVEL 11**)
   376 by (Asm_full_simp_tac 1);
   377 by (rtac disjI1 1);
   378 by (thin_tac "?PP-->?QQ" 1);
   379 by (case_tac "Ba : lost" 1);
   380 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS B_trusts_NS3, 
   381 			      unique_session_keys]) 2);
   382 by (blast_tac (!claset addDs [Says_Crypt_lost]) 1);
   383 val lemma = result();
   384 
   385 goal thy
   386  "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
   387 \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   388 \           : set_of_list evs;                                        \
   389 \           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;  \
   390 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
   391 \        ==> Says B A (Crypt K (Nonce NB)) : set_of_list evs";
   392 by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
   393                        addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
   394 qed "A_trusts_NS4";