src/HOL/Auth/NS_Shared.ML
author paulson
Thu Jan 08 18:10:34 1998 +0100 (1998-01-08)
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4831 dae4d63a1318
permissions -rw-r--r--
Expressed most Oops rules using Notes instead of Says, and other tidying
     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 (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
   101 (*NS2, NS4, NS5*)
   102 by (ALLGOALS (Blast_tac));
   103 qed_spec_mp "new_keys_not_used";
   104 
   105 bind_thm ("new_keys_not_analzd",
   106           [analz_subset_parts RS keysFor_mono,
   107            new_keys_not_used] MRS contra_subsetD);
   108 
   109 Addsimps [new_keys_not_used, new_keys_not_analzd];
   110 
   111 
   112 (** Lemmas concerning the form of items passed in messages **)
   113 
   114 (*Describes the form of K, X and K' when the Server sends this message.*)
   115 goal thy 
   116  "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
   117 \           evs : ns_shared |]                           \
   118 \        ==> K ~: range shrK &                           \
   119 \            X = (Crypt (shrK B) {|Key K, Agent A|}) &   \
   120 \            K' = shrK A";
   121 by (etac rev_mp 1);
   122 by (etac ns_shared.induct 1);
   123 by Auto_tac;
   124 qed "Says_Server_message_form";
   125 
   126 
   127 (*If the encrypted message appears then it originated with the Server*)
   128 goal thy
   129  "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
   130 \           A ~: bad;  evs : ns_shared |]                                 \
   131 \         ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})    \
   132 \               : set evs";
   133 by (etac rev_mp 1);
   134 by (parts_induct_tac 1);
   135 by (Blast_tac 1);
   136 qed "A_trusts_NS2";
   137 
   138 
   139 goal thy
   140  "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
   141 \           A ~: bad;  evs : ns_shared |]                                 \
   142 \         ==> K ~: range shrK &  X = (Crypt (shrK B) {|Key K, Agent A|})";
   143 by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
   144 qed "cert_A_form";
   145 
   146 
   147 (*EITHER describes the form of X when the following message is sent, 
   148   OR     reduces it to the Fake case.
   149   Use Says_Server_message_form if applicable.*)
   150 goal thy 
   151  "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
   152 \              : set evs;                                                  \
   153 \           evs : ns_shared |]                                             \
   154 \        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
   155 \            | X : analz (spies evs)";
   156 by (case_tac "A : bad" 1);
   157 by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
   158                        addss (simpset())) 1);
   159 by (blast_tac (claset() addSDs [cert_A_form]) 1);
   160 qed "Says_S_message_form";
   161 
   162 
   163 (*For proofs involving analz.*)
   164 val analz_spies_tac = 
   165     forward_tac [Says_Server_message_form] 8 THEN
   166     forward_tac [Says_S_message_form] 5 THEN 
   167     REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
   168 
   169 
   170 (****
   171  The following is to prove theorems of the form
   172 
   173   Key K : analz (insert (Key KAB) (spies evs)) ==>
   174   Key K : analz (spies evs)
   175 
   176  A more general formula must be proved inductively.
   177 ****)
   178 
   179 
   180 (*NOT useful in this form, but it says that session keys are not used
   181   to encrypt messages containing other keys, in the actual protocol.
   182   We require that agents should behave like this subsequently also.*)
   183 goal thy 
   184  "!!evs. [| evs : ns_shared;  Kab ~: range shrK |] ==>  \
   185 \           (Crypt KAB X) : parts (spies evs) &         \
   186 \           Key K : parts {X} --> Key K : parts (spies evs)";
   187 by (parts_induct_tac 1);
   188 (*Fake*)
   189 by (blast_tac (claset() addSEs partsEs
   190                         addDs [impOfSubs parts_insert_subset_Un]) 1);
   191 (*Base, NS4 and NS5*)
   192 by Auto_tac;
   193 result();
   194 
   195 
   196 (** Session keys are not used to encrypt other session keys **)
   197 
   198 (*The equality makes the induction hypothesis easier to apply*)
   199 goal thy  
   200  "!!evs. evs : ns_shared ==>                             \
   201 \  ALL K KK. KK <= Compl (range shrK) -->                \
   202 \            (Key K : analz (Key``KK Un (spies evs))) =  \
   203 \            (K : KK | Key K : analz (spies evs))";
   204 by (etac ns_shared.induct 1);
   205 by analz_spies_tac;
   206 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   207 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   208 (*Takes 9 secs*)
   209 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   210 (*Fake*) 
   211 by (spy_analz_tac 1);
   212 qed_spec_mp "analz_image_freshK";
   213 
   214 
   215 goal thy
   216  "!!evs. [| evs : ns_shared;  KAB ~: range shrK |] ==>  \
   217 \        Key K : analz (insert (Key KAB) (spies evs)) = \
   218 \        (K = KAB | Key K : analz (spies evs))";
   219 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   220 qed "analz_insert_freshK";
   221 
   222 
   223 (** The session key K uniquely identifies the message **)
   224 
   225 goal thy 
   226  "!!evs. evs : ns_shared ==>                                               \
   227 \      EX A' NA' B' X'. ALL A NA B X.                                      \
   228 \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
   229 \       -->         A=A' & NA=NA' & B=B' & X=X'";
   230 by (etac ns_shared.induct 1);
   231 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   232 by Safe_tac;
   233 (*NS3*)
   234 by (ex_strip_tac 2);
   235 by (Blast_tac 2);
   236 (*NS2: it can't be a new key*)
   237 by (expand_case_tac "K = ?y" 1);
   238 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   239 by (Blast_tac 1);
   240 val lemma = result();
   241 
   242 (*In messages of this form, the session key uniquely identifies the rest*)
   243 goal thy 
   244  "!!evs. [| Says Server A                                               \
   245 \             (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs;     \ 
   246 \           Says Server A'                                              \
   247 \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
   248 \           evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";
   249 by (prove_unique_tac lemma 1);
   250 qed "unique_session_keys";
   251 
   252 
   253 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   254 
   255 goal thy 
   256  "!!evs. [| A ~: bad;  B ~: bad;  evs : ns_shared |]                   \
   257 \        ==> Says Server A                                             \
   258 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   259 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   260 \             : set evs -->                                            \
   261 \        (ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs) -->          \
   262 \        Key K ~: analz (spies evs)";
   263 by (etac ns_shared.induct 1);
   264 by analz_spies_tac;
   265 by (ALLGOALS 
   266     (asm_simp_tac 
   267      (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ 
   268 			  pushes @ expand_ifs))));
   269 (*Oops*)
   270 by (blast_tac (claset() addSDs [unique_session_keys]) 5);
   271 (*NS3, replay sub-case*) 
   272 by (Blast_tac 4);
   273 (*NS2*)
   274 by (Blast_tac 2);
   275 (*Fake*) 
   276 by (spy_analz_tac 1);
   277 (*NS3, Server sub-case*) (**LEVEL 6 **)
   278 by (clarify_tac (claset() delrules [impCE]) 1);
   279 by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
   280 by (assume_tac 2);
   281 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
   282 			       Crypt_Spy_analz_bad]) 1);
   283 by (blast_tac (claset() addDs [unique_session_keys]) 1);
   284 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   285 
   286 
   287 (*Final version: Server's message in the most abstract form*)
   288 goal thy 
   289  "!!evs. [| Says Server A                                        \
   290 \              (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;   \
   291 \           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;      \
   292 \           A ~: bad;  B ~: bad;  evs : ns_shared                \
   293 \        |] ==> Key K ~: analz (spies evs)";
   294 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   295 by (blast_tac (claset() addSDs [lemma]) 1);
   296 qed "Spy_not_see_encrypted_key";
   297 
   298 
   299 (**** Guarantees available at various stages of protocol ***)
   300 
   301 A_trusts_NS2 RS Spy_not_see_encrypted_key;
   302 
   303 
   304 (*If the encrypted message appears then it originated with the Server*)
   305 goal thy
   306  "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);     \
   307 \           B ~: bad;  evs : ns_shared |]                              \
   308 \         ==> EX NA. Says Server A                                     \
   309 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   310 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   311 \             : set evs";
   312 by (etac rev_mp 1);
   313 by (parts_induct_tac 1);
   314 by (ALLGOALS Blast_tac);
   315 qed "B_trusts_NS3";
   316 
   317 
   318 goal thy
   319  "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
   320 \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   321 \              : set evs;                                             \
   322 \           Key K ~: analz (spies evs);                               \
   323 \           evs : ns_shared |]                  \
   324 \        ==> Says B A (Crypt K (Nonce NB)) : set evs";
   325 by (etac rev_mp 1);
   326 by (etac rev_mp 1);
   327 by (etac rev_mp 1);
   328 by (parts_induct_tac 1);
   329 (*NS3*)
   330 by (Blast_tac 3);
   331 by (Blast_tac 1);
   332 (*NS2: contradiction from the assumptions  
   333   Key K ~: used evs2  and Crypt K (Nonce NB) : parts (spies evs2) *)
   334 by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
   335 			addSDs [Crypt_imp_keysFor]) 1);
   336 (**LEVEL 7**)
   337 (*NS4*)
   338 by (Clarify_tac 1);
   339 by (not_bad_tac "Ba" 1);
   340 by (blast_tac (claset() addDs [B_trusts_NS3, unique_session_keys]) 1);
   341 qed "A_trusts_NS4_lemma";
   342 
   343 
   344 (*This version no longer assumes that K is secure*)
   345 goal thy
   346  "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
   347 \           Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
   348 \           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;           \
   349 \           A ~: bad;  B ~: bad;  evs : ns_shared |]                  \
   350 \        ==> Says B A (Crypt K (Nonce NB)) : set evs";
   351 by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma]
   352 	         addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
   353 qed "A_trusts_NS4";
   354 
   355 
   356 (*If the session key has been used in NS4 then somebody has forwarded
   357   component X in some instance of NS4.  Perhaps an interesting property, 
   358   but not needed (after all) for the proofs below.*)
   359 goal thy
   360  "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);     \
   361 \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   362 \             : set evs;                                              \
   363 \           Key K ~: analz (spies evs);                               \
   364 \           evs : ns_shared |]                              \
   365 \        ==> EX A'. Says A' B X : set evs";
   366 by (etac rev_mp 1);
   367 by (etac rev_mp 1);
   368 by (etac rev_mp 1);
   369 by (parts_induct_tac 1);
   370 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   371 by (ALLGOALS Clarify_tac);
   372 by (Blast_tac 1);
   373 (**LEVEL 7**)
   374 (*NS2*)
   375 by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
   376 			addSDs [Crypt_imp_keysFor]) 1);
   377 (*NS4*)
   378 by (not_bad_tac "Ba" 1);
   379 by (Asm_full_simp_tac 1);
   380 by (forward_tac [Says_imp_spies RS parts.Inj RS B_trusts_NS3] 1);
   381 by (ALLGOALS Clarify_tac);
   382 by (blast_tac (claset() addDs [unique_session_keys]) 1);
   383 qed "NS4_implies_NS3";
   384 
   385 
   386 goal thy
   387  "!!evs. [| B ~: bad;  evs : ns_shared |]                              \
   388 \        ==> Key K ~: analz (spies evs) -->                            \
   389 \            Says Server A                                     \
   390 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   391 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   392 \             : set evs -->         \
   393 \            Says B A (Crypt K (Nonce NB))  : set evs -->  \
   394 \            Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs) --> \
   395 \            Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
   396 by (parts_induct_tac 1);
   397 (*NS4*)
   398 by (Blast_tac 4);
   399 (*NS3*)
   400 by (blast_tac (claset() addSDs [cert_A_form]) 3);
   401 (*NS2*)
   402 by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
   403 			addSDs [Crypt_imp_keysFor]) 2);
   404 by (Blast_tac 1);
   405 (**LEVEL 5**)
   406 (*NS5*)
   407 by (Clarify_tac 1);
   408 by (not_bad_tac "Aa" 1);
   409 by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1);
   410 val lemma = result();
   411 
   412 
   413 (*Very strong Oops condition reveals protocol's weakness*)
   414 goal thy
   415  "!!evs. [| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs);      \
   416 \           Says B A (Crypt K (Nonce NB))  : set evs;                \
   417 \           Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);   \
   418 \           ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs;       \
   419 \           A ~: bad;  B ~: bad;  evs : ns_shared |]                 \
   420 \        ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
   421 by (dtac B_trusts_NS3 1);
   422 by (ALLGOALS Clarify_tac);
   423 by (blast_tac (claset() addSIs [normalize_thm [RSspec, RSmp] lemma]
   424 	         addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
   425 qed "B_trusts_NS5";