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