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