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