src/HOL/Auth/Yahalom2.ML
author paulson
Tue Nov 11 11:16:18 1997 +0100 (1997-11-11)
changeset 4198 c63639beeff1
parent 4153 e534c4c32d54
child 4199 2b9fc1f08886
permissions -rw-r--r--
Fixed spelling error
     1 (*  Title:      HOL/Auth/Yahalom2
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
     7 
     8 This version trades encryption of NB for additional explicitness in YM3.
     9 
    10 From page 259 of
    11   Burrows, Abadi and Needham.  A Logic of Authentication.
    12   Proc. Royal Soc. 426 (1989)
    13 *)
    14 
    15 open Yahalom2;
    16 
    17 proof_timing:=true;
    18 HOL_quantifiers := false;
    19 
    20 (*A "possibility property": there are traces that reach the end*)
    21 goal thy 
    22  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    23 \        ==> EX X NB K. EX evs: yahalom.          \
    24 \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    25 by (REPEAT (resolve_tac [exI,bexI] 1));
    26 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
    27           yahalom.YM4) 2);
    28 by possibility_tac;
    29 result();
    30 
    31 
    32 (**** Inductive proofs about yahalom ****)
    33 
    34 (*Nobody sends themselves messages*)
    35 goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
    36 by (etac yahalom.induct 1);
    37 by (Auto_tac());
    38 qed_spec_mp "not_Says_to_self";
    39 Addsimps [not_Says_to_self];
    40 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    41 
    42 
    43 (** For reasoning about the encrypted portion of messages **)
    44 
    45 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    46 goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \
    47 \                X : analz (spies evs)";
    48 by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    49 qed "YM4_analz_spies";
    50 
    51 bind_thm ("YM4_parts_spies",
    52           YM4_analz_spies RS (impOfSubs analz_subset_parts));
    53 
    54 (*Relates to both YM4 and Oops*)
    55 goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
    56 \                K : parts (spies evs)";
    57 by (blast_tac (claset() addSEs partsEs
    58                        addSDs [Says_imp_spies RS parts.Inj]) 1);
    59 qed "YM4_Key_parts_spies";
    60 
    61 (*For proving the easier theorems about X ~: parts (spies evs).*)
    62 fun parts_spies_tac i = 
    63     forward_tac [YM4_Key_parts_spies] (i+6) THEN
    64     forward_tac [YM4_parts_spies] (i+5)     THEN
    65     prove_simple_subgoals_tac  i;
    66 
    67 (*Induction for regularity theorems.  If induction formula has the form
    68    X ~: analz (spies evs) --> ... then it shortens the proof by discarding
    69    needless information about analz (insert X (spies evs))  *)
    70 fun parts_induct_tac i = 
    71     etac yahalom.induct i
    72     THEN 
    73     REPEAT (FIRSTGOAL analz_mono_contra_tac)
    74     THEN  parts_spies_tac i;
    75 
    76 
    77 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    78     sends messages containing X! **)
    79 
    80 (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    81 goal thy 
    82  "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    83 by (parts_induct_tac 1);
    84 by (Fake_parts_insert_tac 1);
    85 by (Blast_tac 1);
    86 qed "Spy_see_shrK";
    87 Addsimps [Spy_see_shrK];
    88 
    89 goal thy 
    90  "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    91 by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    92 qed "Spy_analz_shrK";
    93 Addsimps [Spy_analz_shrK];
    94 
    95 goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
    96 \                  evs : yahalom |] ==> A:bad";
    97 by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
    98 qed "Spy_see_shrK_D";
    99 
   100 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   101 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   102 
   103 
   104 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   105 goal thy "!!evs. evs : yahalom ==>          \
   106 \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   107 by (parts_induct_tac 1);
   108 (*YM4: Key K is not fresh!*)
   109 by (blast_tac (claset() addSEs spies_partsEs) 3);
   110 (*YM3*)
   111 by (blast_tac (claset() addss (simpset())) 2);
   112 (*Fake*)
   113 by (best_tac
   114       (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   115                addIs  [impOfSubs analz_subset_parts]
   116                addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
   117                addss  (simpset())) 1);
   118 qed_spec_mp "new_keys_not_used";
   119 
   120 bind_thm ("new_keys_not_analzd",
   121           [analz_subset_parts RS keysFor_mono,
   122            new_keys_not_used] MRS contra_subsetD);
   123 
   124 Addsimps [new_keys_not_used, new_keys_not_analzd];
   125 
   126 (*Describes the form of K when the Server sends this message.  Useful for
   127   Oops as well as main secrecy property.*)
   128 goal thy 
   129  "!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
   130 \            : set evs;                                            \
   131 \           evs : yahalom |]                                       \
   132 \        ==> K ~: range shrK & A ~= B";
   133 by (etac rev_mp 1);
   134 by (etac yahalom.induct 1);
   135 by (ALLGOALS Asm_simp_tac);
   136 qed "Says_Server_message_form";
   137 
   138 
   139 (*For proofs involving analz.*)
   140 val analz_spies_tac = 
   141     dtac YM4_analz_spies 6 THEN
   142     forward_tac [Says_Server_message_form] 7 THEN
   143     assume_tac 7 THEN
   144     REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7);
   145 
   146 
   147 (****
   148  The following is to prove theorems of the form
   149 
   150           Key K : analz (insert (Key KAB) (spies evs)) ==>
   151           Key K : analz (spies evs)
   152 
   153  A more general formula must be proved inductively.
   154 
   155 ****)
   156 
   157 (** Session keys are not used to encrypt other session keys **)
   158 
   159 goal thy  
   160  "!!evs. evs : yahalom ==>                                  \
   161 \  ALL K KK. KK <= Compl (range shrK) -->                   \
   162 \            (Key K : analz (Key``KK Un (spies evs))) =  \
   163 \            (K : KK | Key K : analz (spies evs))";
   164 by (etac yahalom.induct 1);
   165 by analz_spies_tac;
   166 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   167 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   168 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   169 (*Fake*) 
   170 by (spy_analz_tac 2);
   171 (*Base*)
   172 by (Blast_tac 1);
   173 qed_spec_mp "analz_image_freshK";
   174 
   175 goal thy
   176  "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>        \
   177 \        Key K : analz (insert (Key KAB) (spies evs)) =  \
   178 \        (K = KAB | Key K : analz (spies evs))";
   179 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   180 qed "analz_insert_freshK";
   181 
   182 
   183 (*** The Key K uniquely identifies the Server's  message. **)
   184 
   185 goal thy 
   186  "!!evs. evs : yahalom ==>                                     \
   187 \      EX A' B' na' nb' X'. ALL A B na nb X.                   \
   188 \          Says Server A                                       \
   189 \           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}   \
   190 \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
   191 by (etac yahalom.induct 1);
   192 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   193 by (Clarify_tac 1);
   194 (*Remaining case: YM3*)
   195 by (expand_case_tac "K = ?y" 1);
   196 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   197 (*...we assume X is a recent message and handle this case by contradiction*)
   198 by (blast_tac (claset() addSEs spies_partsEs
   199                        delrules [conjI]    (*prevent split-up into 4 subgoals*)
   200                        addss (simpset() addsimps [parts_insertI])) 1);
   201 val lemma = result();
   202 
   203 goal thy 
   204 "!!evs. [| Says Server A                                            \
   205 \            {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \
   206 \          Says Server A'                                           \
   207 \            {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} : set evs; \
   208 \          evs : yahalom |]                                         \
   209 \       ==> A=A' & B=B' & na=na' & nb=nb'";
   210 by (prove_unique_tac lemma 1);
   211 qed "unique_session_keys";
   212 
   213 
   214 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   215 
   216 goal thy 
   217  "!!evs. [| A ~: bad;  B ~: bad;  A ~= B;                     \
   218 \           evs : yahalom |]                                    \
   219 \        ==> Says Server A                                      \
   220 \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},     \
   221 \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}    \
   222 \             : set evs -->                                     \
   223 \            Says A Spy {|na, nb, Key K|} ~: set evs -->        \
   224 \            Key K ~: analz (spies evs)";
   225 by (etac yahalom.induct 1);
   226 by analz_spies_tac;
   227 by (ALLGOALS
   228     (asm_simp_tac 
   229      (simpset() addsimps expand_ifs
   230 	       addsimps [analz_insert_eq, analz_insert_freshK]
   231                addsplits [expand_if])));
   232 (*Oops*)
   233 by (blast_tac (claset() addDs [unique_session_keys]) 3);
   234 (*YM3*)
   235 by (blast_tac (claset() delrules [impCE]
   236                        addSEs spies_partsEs
   237                        addIs [impOfSubs analz_subset_parts]) 2);
   238 (*Fake*) 
   239 by (spy_analz_tac 1);
   240 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   241 
   242 
   243 (*Final version*)
   244 goal thy 
   245  "!!evs. [| Says Server A                                    \
   246 \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},  \
   247 \                    Crypt (shrK B) {|nb, Key K, Agent A|}|} \
   248 \           : set evs;                                       \
   249 \           Says A Spy {|na, nb, Key K|} ~: set evs;         \
   250 \           A ~: bad;  B ~: bad;  evs : yahalom |]         \
   251 \        ==> Key K ~: analz (spies evs)";
   252 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   253 by (blast_tac (claset() addSEs [lemma]) 1);
   254 qed "Spy_not_see_encrypted_key";
   255 
   256 
   257 (** Security Guarantee for A upon receiving YM3 **)
   258 
   259 (*If the encrypted message appears then it originated with the Server.
   260   May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   261 goal thy
   262  "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|}                      \
   263 \            : parts (spies evs);                                   \
   264 \           A ~: bad;  evs : yahalom |]                               \
   265 \         ==> EX nb. Says Server A                                     \
   266 \                      {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
   267 \                            Crypt (shrK B) {|nb, Key K, Agent A|}|}   \
   268 \                    : set evs";
   269 by (etac rev_mp 1);
   270 by (parts_induct_tac 1);
   271 by (Fake_parts_insert_tac 1);
   272 by (Blast_tac 1);
   273 qed "A_trusts_YM3";
   274 
   275 
   276 (** Security Guarantee for B upon receiving YM4 **)
   277 
   278 (*B knows, by the first part of A's message, that the Server distributed 
   279   the key for A and B, and has associated it with NB. *)
   280 goal thy 
   281  "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|} : parts (spies evs); \
   282 \           B ~: bad;  evs : yahalom |]                             \
   283 \        ==> EX NA. Says Server A                                    \
   284 \                    {|Nonce NB,                                     \
   285 \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},  \
   286 \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
   287 \                       : set evs";
   288 by (etac rev_mp 1);
   289 by (parts_induct_tac 1);
   290 by (Fake_parts_insert_tac 1);
   291 (*YM3*)
   292 by (Blast_tac 1);
   293 qed "B_trusts_YM4_shrK";
   294 
   295 
   296 (*With this protocol variant, we don't need the 2nd part of YM4 at all:
   297   Nonce NB is available in the first part.*)
   298 
   299 (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   300   because we do not have to show that NB is secret. *)
   301 goal thy 
   302  "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
   303 \             : set evs;                                                 \
   304 \           A ~: bad;  B ~: bad;  evs : yahalom |]                     \
   305 \        ==> EX NA. Says Server A                                        \
   306 \                    {|Nonce NB,                                         \
   307 \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},      \
   308 \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}     \
   309 \                   : set evs";
   310 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
   311 by (blast_tac (claset() addSDs [B_trusts_YM4_shrK]) 1);
   312 qed "B_trusts_YM4";
   313 
   314 
   315 
   316 (*** Authenticating B to A ***)
   317 
   318 (*The encryption in message YM2 tells us it cannot be faked.*)
   319 goal thy 
   320  "!!evs. evs : yahalom                                                  \
   321 \  ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs) -->  \
   322 \      B ~: bad -->                                                    \
   323 \      (EX NB. Says B Server {|Agent B, Nonce NB,                       \
   324 \                              Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
   325 \         : set evs)";
   326 by (parts_induct_tac 1);
   327 by (Fake_parts_insert_tac 1);
   328 (*YM2*)
   329 by (Blast_tac 1);
   330 bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   331 
   332 (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
   333 goal thy 
   334  "!!evs. evs : yahalom                                                   \
   335 \  ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
   336 \         : set evs -->                                                  \
   337 \      B ~: bad -->                                                     \
   338 \      (EX nb'. Says B Server {|Agent B, nb',                            \
   339 \                               Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
   340 \                 : set evs)";
   341 by (etac yahalom.induct 1);
   342 by (ALLGOALS Asm_simp_tac);
   343 (*YM3*)
   344 by (blast_tac (claset() addSDs [B_Said_YM2]
   345 		       addSEs [MPair_parts]
   346 		       addDs [Says_imp_spies RS parts.Inj]) 3);
   347 (*Fake, YM2*)
   348 by (ALLGOALS Blast_tac);
   349 val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   350 
   351 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   352 goal thy
   353  "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
   354 \             : set evs;                                                    \
   355 \           A ~: bad;  B ~: bad;  evs : yahalom |]                   \
   356 \   ==> EX nb'. Says B Server                                               \
   357 \                    {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   358 \                 : set evs";
   359 by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]
   360 		       addEs spies_partsEs) 1);
   361 qed "YM3_auth_B_to_A";
   362 
   363 
   364 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   365 
   366 (*Assuming the session key is secure, if both certificates are present then
   367   A has said NB.  We can't be sure about the rest of A's message, but only
   368   NB matters for freshness.*)  
   369 goal thy 
   370  "!!evs. evs : yahalom                                        \
   371 \        ==> Key K ~: analz (spies evs) -->                \
   372 \            Crypt K (Nonce NB) : parts (spies evs) -->    \
   373 \            Crypt (shrK B) {|Nonce NB, Key K, Agent A|}      \
   374 \              : parts (spies evs) -->                     \
   375 \            B ~: bad -->                                    \
   376 \            (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   377 by (parts_induct_tac 1);
   378 (*Fake*)
   379 by (Fake_parts_insert_tac 1);
   380 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   381 by (fast_tac (claset() addSDs [Crypt_imp_invKey_keysFor] addss (simpset())) 1); 
   382 (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   383 by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   384 (*yes: apply unicity of session keys*)
   385 by (not_bad_tac "Aa" 1);
   386 by (blast_tac (claset() addSEs [MPair_parts]
   387                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   388 		       addDs  [Says_imp_spies RS parts.Inj,
   389 			       unique_session_keys]) 1);
   390 val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   391 
   392 (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   393   Moreover, A associates K with NB (thus is talking about the same run).
   394   Other premises guarantee secrecy of K.*)
   395 goal thy 
   396  "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
   397 \                       Crypt K (Nonce NB)|} : set evs;                 \
   398 \           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
   399 \           A ~: bad;  B ~: bad;  evs : yahalom |]                    \
   400 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   401 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
   402 by (dtac B_trusts_YM4_shrK 1);
   403 by Safe_tac;
   404 by (rtac lemma 1);
   405 by (rtac Spy_not_see_encrypted_key 2);
   406 by (REPEAT_FIRST assume_tac);
   407 by (ALLGOALS (blast_tac (claset() addSEs [MPair_parts]
   408 			         addDs [Says_imp_spies RS parts.Inj])));
   409 qed_spec_mp "YM4_imp_A_Said_YM3";