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