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