src/HOL/Auth/Yahalom2.ML
author paulson
Thu Jan 08 18:10:34 1998 +0100 (1998-01-08)
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4598 649bf14debe7
permissions -rw-r--r--
Expressed most Oops rules using Notes instead of Says, and other tidying
     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 set proof_timing;
    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 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
    96 	Spy_analz_shrK RSN (2, rev_iffD1)];
    97 
    98 
    99 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   100 goal thy "!!evs. evs : yahalom ==>          \
   101 \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   102 by (parts_induct_tac 1);
   103 (*YM4: Key K is not fresh!*)
   104 by (blast_tac (claset() addSEs spies_partsEs) 3);
   105 (*YM3*)
   106 by (blast_tac (claset() addss (simpset())) 2);
   107 (*Fake*)
   108 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
   109 qed_spec_mp "new_keys_not_used";
   110 
   111 bind_thm ("new_keys_not_analzd",
   112           [analz_subset_parts RS keysFor_mono,
   113            new_keys_not_used] MRS contra_subsetD);
   114 
   115 Addsimps [new_keys_not_used, new_keys_not_analzd];
   116 
   117 (*Describes the form of K when the Server sends this message.  Useful for
   118   Oops as well as main secrecy property.*)
   119 goal thy 
   120  "!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
   121 \            : set evs;                                            \
   122 \           evs : yahalom |]                                       \
   123 \        ==> K ~: range shrK & A ~= B";
   124 by (etac rev_mp 1);
   125 by (etac yahalom.induct 1);
   126 by (ALLGOALS Asm_simp_tac);
   127 qed "Says_Server_message_form";
   128 
   129 
   130 (*For proofs involving analz.*)
   131 val analz_spies_tac = 
   132     dtac YM4_analz_spies 6 THEN
   133     forward_tac [Says_Server_message_form] 7 THEN
   134     assume_tac 7 THEN
   135     REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7);
   136 
   137 
   138 (****
   139  The following is to prove theorems of the form
   140 
   141           Key K : analz (insert (Key KAB) (spies evs)) ==>
   142           Key K : analz (spies evs)
   143 
   144  A more general formula must be proved inductively.
   145 
   146 ****)
   147 
   148 (** Session keys are not used to encrypt other session keys **)
   149 
   150 goal thy  
   151  "!!evs. evs : yahalom ==>                                  \
   152 \  ALL K KK. KK <= Compl (range shrK) -->                   \
   153 \            (Key K : analz (Key``KK Un (spies evs))) =  \
   154 \            (K : KK | Key K : analz (spies evs))";
   155 by (etac yahalom.induct 1);
   156 by analz_spies_tac;
   157 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   158 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   159 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   160 (*Fake*) 
   161 by (spy_analz_tac 1);
   162 qed_spec_mp "analz_image_freshK";
   163 
   164 goal thy
   165  "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>        \
   166 \        Key K : analz (insert (Key KAB) (spies evs)) =  \
   167 \        (K = KAB | Key K : analz (spies evs))";
   168 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   169 qed "analz_insert_freshK";
   170 
   171 
   172 (*** The Key K uniquely identifies the Server's  message. **)
   173 
   174 goal thy 
   175  "!!evs. evs : yahalom ==>                                     \
   176 \      EX A' B' na' nb' X'. ALL A B na nb X.                   \
   177 \          Says Server A                                       \
   178 \           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}   \
   179 \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
   180 by (etac yahalom.induct 1);
   181 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   182 by (Clarify_tac 1);
   183 (*Remaining case: YM3*)
   184 by (expand_case_tac "K = ?y" 1);
   185 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   186 (*...we assume X is a recent message and handle this case by contradiction*)
   187 by (blast_tac (claset() addSEs spies_partsEs
   188                         delrules [conjI]    (*prevent splitup into 4 subgoals*)
   189                         addss (simpset() addsimps [parts_insertI])) 1);
   190 val lemma = result();
   191 
   192 goal thy 
   193 "!!evs. [| Says Server A                                            \
   194 \            {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \
   195 \          Says Server A'                                           \
   196 \            {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} : set evs; \
   197 \          evs : yahalom |]                                         \
   198 \       ==> A=A' & B=B' & na=na' & nb=nb'";
   199 by (prove_unique_tac lemma 1);
   200 qed "unique_session_keys";
   201 
   202 
   203 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   204 
   205 goal thy 
   206  "!!evs. [| A ~: bad;  B ~: bad;  A ~= B;                     \
   207 \           evs : yahalom |]                                    \
   208 \        ==> Says Server A                                      \
   209 \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},     \
   210 \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}    \
   211 \             : set evs -->                                     \
   212 \            Notes Spy {|na, nb, Key K|} ~: set evs -->         \
   213 \            Key K ~: analz (spies evs)";
   214 by (etac yahalom.induct 1);
   215 by analz_spies_tac;
   216 by (ALLGOALS
   217     (asm_simp_tac 
   218      (simpset() addsimps expand_ifs
   219 	        addsimps [analz_insert_eq, analz_insert_freshK]
   220                 addsplits [expand_if])));
   221 (*Oops*)
   222 by (blast_tac (claset() addDs [unique_session_keys]) 3);
   223 (*YM3*)
   224 by (blast_tac (claset() delrules [impCE]
   225                         addSEs spies_partsEs
   226                         addIs [impOfSubs analz_subset_parts]) 2);
   227 (*Fake*) 
   228 by (spy_analz_tac 1);
   229 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   230 
   231 
   232 (*Final version*)
   233 goal thy 
   234  "!!evs. [| Says Server A                                    \
   235 \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},  \
   236 \                    Crypt (shrK B) {|nb, Key K, Agent A|}|} \
   237 \           : set evs;                                       \
   238 \           Notes Spy {|na, nb, Key K|} ~: set evs;          \
   239 \           A ~: bad;  B ~: bad;  evs : yahalom |]           \
   240 \        ==> Key K ~: analz (spies evs)";
   241 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   242 by (blast_tac (claset() addSEs [lemma]) 1);
   243 qed "Spy_not_see_encrypted_key";
   244 
   245 
   246 (** Security Guarantee for A upon receiving YM3 **)
   247 
   248 (*If the encrypted message appears then it originated with the Server.
   249   May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   250 goal thy
   251  "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|}                      \
   252 \            : parts (spies evs);                                      \
   253 \           A ~: bad;  evs : yahalom |]                                \
   254 \         ==> EX nb. Says Server A                                     \
   255 \                      {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
   256 \                            Crypt (shrK B) {|nb, Key K, Agent A|}|}   \
   257 \                    : set evs";
   258 by (etac rev_mp 1);
   259 by (parts_induct_tac 1);
   260 by (Fake_parts_insert_tac 1);
   261 by (Blast_tac 1);
   262 qed "A_trusts_YM3";
   263 
   264 
   265 (** Security Guarantee for B upon receiving YM4 **)
   266 
   267 (*B knows, by the first part of A's message, that the Server distributed 
   268   the key for A and B, and has associated it with NB. *)
   269 goal thy 
   270  "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|} : parts (spies evs); \
   271 \           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) {|Nonce NB, Key K, Agent A|}|} \
   276 \                       : set evs";
   277 by (etac rev_mp 1);
   278 by (parts_induct_tac 1);
   279 by (Fake_parts_insert_tac 1);
   280 (*YM3*)
   281 by (Blast_tac 1);
   282 qed "B_trusts_YM4_shrK";
   283 
   284 
   285 (*With this protocol variant, we don't need the 2nd part of YM4 at all:
   286   Nonce NB is available in the first part.*)
   287 
   288 (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   289   because we do not have to show that NB is secret. *)
   290 goal thy 
   291  "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
   292 \             : set evs;                                                 \
   293 \           A ~: bad;  B ~: bad;  evs : yahalom |]                     \
   294 \        ==> EX NA. Says Server A                                        \
   295 \                    {|Nonce NB,                                         \
   296 \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},      \
   297 \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}     \
   298 \                   : set evs";
   299 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
   300 by (blast_tac (claset() addSDs [B_trusts_YM4_shrK]) 1);
   301 qed "B_trusts_YM4";
   302 
   303 
   304 
   305 (*** Authenticating B to A ***)
   306 
   307 (*The encryption in message YM2 tells us it cannot be faked.*)
   308 goal thy 
   309  "!!evs. evs : yahalom                                                  \
   310 \  ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs) -->  \
   311 \      B ~: bad -->                                                    \
   312 \      (EX NB. Says B Server {|Agent B, Nonce NB,                       \
   313 \                              Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
   314 \         : set evs)";
   315 by (parts_induct_tac 1);
   316 by (Fake_parts_insert_tac 1);
   317 (*YM2*)
   318 by (Blast_tac 1);
   319 bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   320 
   321 (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
   322 goal thy 
   323  "!!evs. evs : yahalom                                                   \
   324 \  ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
   325 \         : set evs -->                                                  \
   326 \      B ~: bad -->                                                     \
   327 \      (EX nb'. Says B Server {|Agent B, nb',                            \
   328 \                               Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
   329 \                 : set evs)";
   330 by (etac yahalom.induct 1);
   331 by (ALLGOALS Asm_simp_tac);
   332 (*YM3*)
   333 by (blast_tac (claset() addSDs [B_Said_YM2]
   334  		        addSEs [MPair_parts]
   335 	 	        addDs [Says_imp_spies RS parts.Inj]) 3);
   336 (*Fake, YM2*)
   337 by (ALLGOALS Blast_tac);
   338 val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   339 
   340 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   341 goal thy
   342  "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
   343 \             : set evs;                                                    \
   344 \           A ~: bad;  B ~: bad;  evs : yahalom |]                   \
   345 \   ==> EX nb'. Says B Server                                               \
   346 \                    {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   347 \                 : set evs";
   348 by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]
   349 		        addEs spies_partsEs) 1);
   350 qed "YM3_auth_B_to_A";
   351 
   352 
   353 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   354 
   355 (*Assuming the session key is secure, if both certificates are present then
   356   A has said NB.  We can't be sure about the rest of A's message, but only
   357   NB matters for freshness.*)  
   358 goal thy 
   359  "!!evs. evs : yahalom                                        \
   360 \        ==> Key K ~: analz (spies evs) -->                \
   361 \            Crypt K (Nonce NB) : parts (spies evs) -->    \
   362 \            Crypt (shrK B) {|Nonce NB, Key K, Agent A|}      \
   363 \              : parts (spies evs) -->                     \
   364 \            B ~: bad -->                                    \
   365 \            (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   366 by (parts_induct_tac 1);
   367 (*Fake*)
   368 by (Fake_parts_insert_tac 1);
   369 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   370 by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
   371 (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   372 by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
   373 (*yes: apply unicity of session keys*)
   374 by (not_bad_tac "Aa" 1);
   375 by (blast_tac (claset() addSEs [MPair_parts]
   376 			addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   377 			addDs  [Says_imp_spies RS parts.Inj,
   378 				unique_session_keys]) 1);
   379 val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   380 
   381 (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   382   Moreover, A associates K with NB (thus is talking about the same run).
   383   Other premises guarantee secrecy of K.*)
   384 goal thy 
   385  "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
   386 \                       Crypt K (Nonce NB)|} : set evs;                 \
   387 \           (ALL NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
   388 \           A ~: bad;  B ~: bad;  evs : yahalom |]                    \
   389 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   390 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
   391 by (dtac B_trusts_YM4_shrK 1);
   392 by Safe_tac;
   393 by (rtac lemma 1);
   394 by (rtac Spy_not_see_encrypted_key 2);
   395 by (REPEAT_FIRST assume_tac);
   396 by (ALLGOALS (blast_tac (claset() addSEs [MPair_parts]
   397 			          addDs [Says_imp_spies RS parts.Inj])));
   398 qed_spec_mp "YM4_imp_A_Said_YM3";