src/HOL/Auth/NS_Shared.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2637 e9b203f854ae
child 3121 cbb6c0c1c58a
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     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                unsafe_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                       unsafe_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 **)
   245 
   246 goal thy 
   247  "!!evs. evs : ns_shared lost ==>                                        \
   248 \      EX A' NA' B' X'. ALL A NA B X.                                    \
   249 \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
   250 \       : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'";
   251 by (etac ns_shared.induct 1);
   252 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   253 by (Step_tac 1);
   254 (*NS3*)
   255 by (ex_strip_tac 2);
   256 by (Fast_tac 2);
   257 (*NS2: it can't be a new key*)
   258 by (expand_case_tac "K = ?y" 1);
   259 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   260 by (fast_tac (!claset delrules [conjI]    (*prevent split-up into 4 subgoals*)
   261                       addSEs sees_Spy_partsEs
   262                       addss (!simpset addsimps [parts_insertI])) 1);
   263 val lemma = result();
   264 
   265 (*In messages of this form, the session key uniquely identifies the rest*)
   266 goal thy 
   267  "!!evs. [| Says Server A                                    \
   268 \             (Crypt (shrK A) {|NA, Agent B, Key K, X|})     \
   269 \                  : set_of_list evs;                        \ 
   270 \           Says Server A'                                   \
   271 \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
   272 \                  : set_of_list evs;                        \
   273 \           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
   274 by (prove_unique_tac lemma 1);
   275 qed "unique_session_keys";
   276 
   277 
   278 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   279 
   280 goal thy 
   281  "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_shared lost |]            \
   282 \        ==> Says Server A                                             \
   283 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   284 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   285 \             : set_of_list evs -->                                    \
   286 \        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
   287 \        Key K ~: analz (sees lost Spy evs)";
   288 by (etac ns_shared.induct 1);
   289 by analz_Fake_tac;
   290 by (ALLGOALS 
   291     (asm_simp_tac 
   292      (!simpset addsimps ([not_parts_not_analz, analz_insert_freshK] @ pushes)
   293                setloop split_tac [expand_if])));
   294 (*NS4, Fake*) 
   295 by (EVERY (map spy_analz_tac [4,1]));
   296 (*NS2*)
   297 by (fast_tac (!claset addSEs sees_Spy_partsEs
   298                       addIs [parts_insertI, impOfSubs analz_subset_parts]
   299                       addss (!simpset)) 1);
   300 (*Oops*)
   301 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2);
   302 (*NS3*) (**LEVEL 6 **)
   303 by (step_tac (!claset delrules [impCE]) 1);
   304 by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1);
   305 by (assume_tac 2);
   306 by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1);
   307 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   308 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   309 
   310 
   311 (*Final version: Server's message in the most abstract form*)
   312 goal thy 
   313  "!!evs. [| Says Server A                                               \
   314 \            (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs;    \
   315 \           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs);  \
   316 \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
   317 \        |] ==> Key K ~: analz (sees lost Spy evs)";
   318 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   319 by (fast_tac (!claset addSEs [lemma]) 1);
   320 qed "Spy_not_see_encrypted_key";
   321 
   322 
   323 goal thy 
   324  "!!evs. [| C ~: {A,B,Server};                                          \
   325 \           Says Server A                                               \
   326 \            (Crypt K' {|NA, Agent B, Key K, X|}) : set_of_list evs;    \
   327 \           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs);  \
   328 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
   329 \        ==> Key K ~: analz (sees lost C evs)";
   330 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   331 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   332 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   333 by (REPEAT_FIRST (fast_tac (!claset addIs [ns_shared_mono RS subsetD])));
   334 qed "Agent_not_see_encrypted_key";
   335 
   336 
   337 
   338 (**** Guarantees available at various stages of protocol ***)
   339 
   340 A_trusts_NS2 RS conjunct2 RS Spy_not_see_encrypted_key;
   341 
   342 
   343 (*If the encrypted message appears then it originated with the Server*)
   344 goal thy
   345  "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees lost Spy evs); \
   346 \           B ~: lost;  evs : ns_shared lost |]                        \
   347 \         ==> EX NA. Says Server A                                     \
   348 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   349 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   350 \             : set_of_list evs";
   351 by (etac rev_mp 1);
   352 by (etac ns_shared.induct 1);
   353 by parts_Fake_tac;
   354 (*Fake case*)
   355 by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   356                       addDs  [impOfSubs analz_subset_parts]
   357                       addss  (!simpset)) 2);
   358 by (Auto_tac());
   359 qed "B_trusts_NS3";
   360 
   361 
   362 goal thy
   363  "!!evs. [| B ~: lost;  evs : ns_shared lost |]            \
   364 \        ==> Key K ~: analz (sees lost Spy evs) -->             \
   365 \            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   366 \            : set_of_list evs --> \
   367 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->            \
   368 \            Says B A (Crypt K (Nonce NB)) : set_of_list evs";
   369 by (etac ns_shared.induct 1);
   370 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   371 by parts_Fake_tac;
   372 by (TRYALL (rtac impI));
   373 by (REPEAT_FIRST
   374     (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   375 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   376 (**LEVEL 6**)
   377 by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
   378                       addDs [impOfSubs analz_subset_parts]) 1);
   379 by (Fast_tac 2);
   380 by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
   381 (*Subgoal 1: contradiction from the assumptions  
   382   Key K ~: used evsa  and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *)
   383 by (dtac Crypt_imp_invKey_keysFor 1);
   384 (**LEVEL 10**)
   385 by (Asm_full_simp_tac 1);
   386 by (rtac disjI1 1);
   387 by (thin_tac "?PP-->?QQ" 1);
   388 by (case_tac "Ba : lost" 1);
   389 by (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1);
   390 by (dtac (Says_imp_sees_Spy RS parts.Inj RS B_trusts_NS3) 1 THEN 
   391     REPEAT (assume_tac 1));
   392 by (best_tac (!claset addDs [unique_session_keys]) 1);
   393 val lemma = result();
   394 
   395 goal thy
   396  "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
   397 \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   398 \           : set_of_list evs;                                        \
   399 \           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;  \
   400 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
   401 \        ==> Says B A (Crypt K (Nonce NB)) : set_of_list evs";
   402 by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
   403                       addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
   404 qed "A_trusts_NS4";