src/HOL/Auth/Yahalom2.ML
author paulson
Wed May 07 13:01:43 1997 +0200 (1997-05-07)
changeset 3121 cbb6c0c1c58a
parent 2637 e9b203f854ae
child 3432 04412cfe6861
permissions -rw-r--r--
Conversion to use blast_tac (with other improvements)
     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 lost.          \
    24 \               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list 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 (*Monotonicity*)
    35 goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
    36 by (rtac subsetI 1);
    37 by (etac yahalom.induct 1);
    38 by (REPEAT_FIRST
    39     (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    40                               :: yahalom.intrs))));
    41 qed "yahalom_mono";
    42 
    43 
    44 (*Nobody sends themselves messages*)
    45 goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
    46 by (etac yahalom.induct 1);
    47 by (Auto_tac());
    48 qed_spec_mp "not_Says_to_self";
    49 Addsimps [not_Says_to_self];
    50 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    51 
    52 
    53 (** For reasoning about the encrypted portion of messages **)
    54 
    55 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    56 goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set_of_list evs ==> \
    57 \                X : analz (sees lost Spy evs)";
    58 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    59 qed "YM4_analz_sees_Spy";
    60 
    61 bind_thm ("YM4_parts_sees_Spy",
    62           YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    63 
    64 (*Relates to both YM4 and Oops*)
    65 goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
    66 \                  : set_of_list evs ==> \
    67 \                K : parts (sees lost Spy evs)";
    68 by (blast_tac (!claset addSEs partsEs
    69                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    70 qed "YM4_Key_parts_sees_Spy";
    71 
    72 (*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    73   We instantiate the variable to "lost" since leaving it as a Var would
    74   interfere with simplification.*)
    75 val parts_induct_tac = 
    76     etac yahalom.induct 1 THEN 
    77     forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
    78     forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
    79     prove_simple_subgoals_tac  1;
    80 
    81 
    82 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    83     sends messages containing X! **)
    84 
    85 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    86 goal thy 
    87  "!!evs. evs : yahalom lost \
    88 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    89 by parts_induct_tac;
    90 by (Fake_parts_insert_tac 1);
    91 by (Blast_tac 1);
    92 qed "Spy_see_shrK";
    93 Addsimps [Spy_see_shrK];
    94 
    95 goal thy 
    96  "!!evs. evs : yahalom lost \
    97 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    98 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    99 qed "Spy_analz_shrK";
   100 Addsimps [Spy_analz_shrK];
   101 
   102 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   103 \                  evs : yahalom lost |] ==> A:lost";
   104 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   105 qed "Spy_see_shrK_D";
   106 
   107 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   108 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   109 
   110 
   111 (*Nobody can have used non-existent keys!*)
   112 goal thy "!!evs. evs : yahalom lost ==>          \
   113 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   114 by parts_induct_tac;
   115 (*YM4: Key K is not fresh!*)
   116 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   117 (*YM3*)
   118 by (blast_tac (!claset addss (!simpset)) 2);
   119 (*Fake*)
   120 by (best_tac
   121       (!claset addIs [impOfSubs analz_subset_parts]
   122                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   123                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   124                addss (!simpset)) 1);
   125 qed_spec_mp "new_keys_not_used";
   126 
   127 bind_thm ("new_keys_not_analzd",
   128           [analz_subset_parts RS keysFor_mono,
   129            new_keys_not_used] MRS contra_subsetD);
   130 
   131 Addsimps [new_keys_not_used, new_keys_not_analzd];
   132 
   133 
   134 (*Describes the form of K when the Server sends this message.  Useful for
   135   Oops as well as main secrecy property.*)
   136 goal thy 
   137  "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
   138 \            : set_of_list evs;                                         \
   139 \           evs : yahalom lost |]                                       \
   140 \        ==> K ~: range shrK & A ~= B";
   141 by (etac rev_mp 1);
   142 by (etac yahalom.induct 1);
   143 by (ALLGOALS Asm_simp_tac);
   144 qed "Says_Server_message_form";
   145 
   146 
   147 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   148 val analz_sees_tac = 
   149     dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   150     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   151     assume_tac 7 THEN
   152     REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7);
   153 
   154 
   155 (****
   156  The following is to prove theorems of the form
   157 
   158           Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   159           Key K : analz (sees lost Spy evs)
   160 
   161  A more general formula must be proved inductively.
   162 
   163 ****)
   164 
   165 (** Session keys are not used to encrypt other session keys **)
   166 
   167 goal thy  
   168  "!!evs. evs : yahalom lost ==> \
   169 \  ALL K KK. KK <= Compl (range shrK) -->                      \
   170 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   171 \            (K : KK | Key K : analz (sees lost Spy evs))";
   172 by (etac yahalom.induct 1);
   173 by analz_sees_tac;
   174 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   175 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   176 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   177 (*Base*)
   178 by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   179 (*YM4, Fake*) 
   180 by (REPEAT (spy_analz_tac 1));
   181 qed_spec_mp "analz_image_freshK";
   182 
   183 goal thy
   184  "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
   185 \        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   186 \        (K = KAB | Key K : analz (sees lost Spy evs))";
   187 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   188 qed "analz_insert_freshK";
   189 
   190 
   191 (*** The Key K uniquely identifies the Server's  message. **)
   192 
   193 goal thy 
   194  "!!evs. evs : yahalom lost ==>                                     \
   195 \      EX A' B' NA' NB' X'. ALL A B NA NB X.                        \
   196 \          Says Server A                                            \
   197 \           {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, X|}        \
   198 \          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
   199 by (etac yahalom.induct 1);
   200 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   201 by (Step_tac 1);
   202 (*Remaining case: YM3*)
   203 by (expand_case_tac "K = ?y" 1);
   204 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   205 (*...we assume X is a recent message and handle this case by contradiction*)
   206 by (blast_tac (!claset addSEs sees_Spy_partsEs
   207                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
   208                       addss (!simpset addsimps [parts_insertI])) 1);
   209 val lemma = result();
   210 
   211 goal thy 
   212 "!!evs. [| Says Server A                                            \
   213 \           {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, X|}        \
   214 \           : set_of_list evs;                                      \
   215 \          Says Server A'                                           \
   216 \           {|NB', Crypt (shrK A') {|Agent B', Key K, NA'|}, X'|}   \
   217 \           : set_of_list evs;                                      \
   218 \          evs : yahalom lost |]                                    \
   219 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   220 by (prove_unique_tac lemma 1);
   221 qed "unique_session_keys";
   222 
   223 
   224 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   225 
   226 goal thy 
   227  "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                          \
   228 \           evs : yahalom lost |]                                    \
   229 \        ==> Says Server A                                           \
   230 \              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},          \
   231 \                    Crypt (shrK B) {|NB, Key K, Agent A|}|}         \
   232 \             : set_of_list evs -->                                  \
   233 \            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->     \
   234 \            Key K ~: analz (sees lost Spy evs)";
   235 by (etac yahalom.induct 1);
   236 by analz_sees_tac;
   237 by (ALLGOALS
   238     (asm_simp_tac 
   239      (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
   240                setloop split_tac [expand_if])));
   241 (*YM3*)
   242 by (blast_tac (!claset delrules [impCE]
   243                       addSEs sees_Spy_partsEs
   244                       addIs [impOfSubs analz_subset_parts]
   245                       addss (!simpset addsimps [parts_insert2])) 2);
   246 (*OR4, Fake*) 
   247 by (REPEAT_FIRST spy_analz_tac);
   248 (*Oops*)
   249 by (blast_tac (!claset addDs [unique_session_keys]) 1);
   250 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   251 
   252 
   253 (*Final version: Server's message in the most abstract form*)
   254 goal thy 
   255  "!!evs. [| Says Server A                                         \
   256 \              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},       \
   257 \                    Crypt (shrK B) {|NB, Key K, Agent A|}|}      \
   258 \           : set_of_list evs;                                    \
   259 \           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
   260 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   261 \        ==> Key K ~: analz (sees lost Spy evs)";
   262 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   263 by (blast_tac (!claset addSEs [lemma]) 1);
   264 qed "Spy_not_see_encrypted_key";
   265 
   266 
   267 goal thy 
   268  "!!evs. [| C ~: {A,B,Server};                                    \
   269 \           Says Server A                                         \
   270 \              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},       \
   271 \                    Crypt (shrK B) {|NB, Key K, Agent A|}|}      \
   272 \           : set_of_list evs;                                    \
   273 \           Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;      \
   274 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   275 \        ==> Key K ~: analz (sees lost C evs)";
   276 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   277 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   278 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   279 by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
   280 qed "Agent_not_see_encrypted_key";
   281 
   282 
   283 (*** Security Guarantees for A and B ***)
   284 
   285 (*If the encrypted message appears then it originated with the Server.*)
   286 goal thy
   287  "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA|}                \
   288 \            : parts (sees lost Spy evs);                              \
   289 \           A ~: lost;  evs : yahalom lost |]                          \
   290 \         ==> EX NB. Says Server A                                     \
   291 \                      {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},    \
   292 \                            Crypt (shrK B) {|NB, Key K, Agent A|}|}   \
   293 \                    : set_of_list evs";
   294 by (etac rev_mp 1);
   295 by parts_induct_tac;
   296 by (Fake_parts_insert_tac 1);
   297 by (Blast_tac 1);
   298 qed "A_trusts_YM3";
   299 
   300 
   301 (*B knows, by the first part of A's message, that the Server distributed 
   302   the key for A and B. *)
   303 goal thy 
   304  "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|}              \
   305 \            : parts (sees lost Spy evs);                            \
   306 \           B ~: lost;  evs : yahalom lost |]                        \
   307 \        ==> EX NA. Says Server A                                    \
   308 \                    {|Nonce NB,                                     \
   309 \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},  \
   310 \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
   311 \                       : set_of_list evs";
   312 by (etac rev_mp 1);
   313 by parts_induct_tac;
   314 by (Fake_parts_insert_tac 1);
   315 (*YM3*)
   316 by (Blast_tac 1);
   317 qed "B_trusts_YM4_shrK";
   318 
   319 (*With this variant we don't bother to use the 2nd part of YM4 at all, since
   320   Nonce NB is available in the first part.  However the 2nd part does assure B
   321   of A's existence.*)
   322 
   323 (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   324   because we do not have to show that NB is secret. *)
   325 goal thy 
   326  "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
   327 \                       Crypt K (Nonce NB)|} : set_of_list evs;         \
   328 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
   329 \        ==> EX NA. Says Server A                                       \
   330 \                    {|Nonce NB,                                        \
   331 \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},     \
   332 \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}    \
   333 \                   : set_of_list evs";
   334 by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
   335 by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
   336 qed "B_trusts_YM4";