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