src/HOL/Auth/OtwayRees_AN.ML
author paulson
Wed May 07 13:01:43 1997 +0200 (1997-05-07)
changeset 3121 cbb6c0c1c58a
parent 3102 4d01cdc119d2
child 3207 fe79ad367d77
permissions -rw-r--r--
Conversion to use blast_tac (with other improvements)
     1 (*  Title:      HOL/Auth/OtwayRees
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "otway" for the Otway-Rees protocol.
     7 
     8 Simplified version with minimal encryption but explicit messages
     9 
    10 From page 11 of
    11   Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
    12   IEEE Trans. SE 22 (1), 1996
    13 *)
    14 
    15 open OtwayRees_AN;
    16 
    17 proof_timing:=true;
    18 HOL_quantifiers := false;
    19 
    20 
    21 (*A "possibility property": there are traces that reach the end*)
    22 goal thy 
    23  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                               \
    24 \        ==> EX K. EX NA. EX evs: otway lost.                                 \
    25 \             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
    26 \             : set_of_list evs";
    27 by (REPEAT (resolve_tac [exI,bexI] 1));
    28 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    29 by possibility_tac;
    30 result();
    31 
    32 
    33 (**** Inductive proofs about otway ****)
    34 
    35 (*Monotonicity*)
    36 goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
    37 by (rtac subsetI 1);
    38 by (etac otway.induct 1);
    39 by (REPEAT_FIRST
    40     (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    41                               :: otway.intrs))));
    42 qed "otway_mono";
    43 
    44 (*Nobody sends themselves messages*)
    45 goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
    46 by (etac otway.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 goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
    56 \                X : analz (sees lost Spy evs)";
    57 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    58 qed "OR4_analz_sees_Spy";
    59 
    60 goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    61 \                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
    62 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    63 qed "Oops_parts_sees_Spy";
    64 
    65 (*OR4_analz_sees_Spy lets us treat those cases using the same 
    66   argument as for the Fake case.  This is possible for most, but not all,
    67   proofs, since Fake messages originate from the Spy. *)
    68 
    69 bind_thm ("OR4_parts_sees_Spy",
    70           OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    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     let val tac = forw_inst_tac [("lost","lost")] 
    77     in  etac otway.induct	   1 THEN 
    78         tac OR4_parts_sees_Spy     6 THEN
    79         tac Oops_parts_sees_Spy    7 THEN
    80 	prove_simple_subgoals_tac  1
    81     end;
    82 
    83 
    84 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    85     sends messages containing X! **)
    86 
    87 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    88 goal thy 
    89  "!!evs. evs : otway lost \
    90 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    91 by parts_induct_tac;
    92 by (Fake_parts_insert_tac 1);
    93 by (Blast_tac 1);
    94 qed "Spy_see_shrK";
    95 Addsimps [Spy_see_shrK];
    96 
    97 goal thy 
    98  "!!evs. evs : otway lost \
    99 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   100 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   101 qed "Spy_analz_shrK";
   102 Addsimps [Spy_analz_shrK];
   103 
   104 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   105 \                  evs : otway lost |] ==> A:lost";
   106 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   107 qed "Spy_see_shrK_D";
   108 
   109 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   110 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   111 
   112 
   113 (*Nobody can have used non-existent keys!*)
   114 goal thy "!!evs. evs : otway lost ==>          \
   115 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   116 by parts_induct_tac;
   117 (*Fake*)
   118 by (best_tac
   119       (!claset addIs [impOfSubs analz_subset_parts]
   120                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   121                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   122                unsafe_addss (!simpset)) 1);
   123 (*OR3*)
   124 by (Blast_tac 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 
   135 (*** Proofs involving analz ***)
   136 
   137 (*Describes the form of K and NA when the Server sends this message.*)
   138 goal thy 
   139  "!!evs. [| Says Server B                                           \
   140 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   141 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   142 \             : set_of_list evs;                                    \
   143 \           evs : otway lost |]                                     \
   144 \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   145 by (etac rev_mp 1);
   146 by (etac otway.induct 1);
   147 by (ALLGOALS Asm_simp_tac);
   148 by (Blast_tac 1);
   149 qed "Says_Server_message_form";
   150 
   151 
   152 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   153 val analz_sees_tac = 
   154     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   155     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   156     assume_tac 7 THEN
   157     REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   158 
   159 
   160 (****
   161  The following is to prove theorems of the form
   162 
   163   Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   164   Key K : analz (sees lost Spy evs)
   165 
   166  A more general formula must be proved inductively.
   167 ****)
   168 
   169 
   170 (** Session keys are not used to encrypt other session keys **)
   171 
   172 (*The equality makes the induction hypothesis easier to apply*)
   173 goal thy  
   174  "!!evs. evs : otway lost ==>                                         \
   175 \  ALL K KK. KK <= Compl (range shrK) -->                      \
   176 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   177 \            (K : KK | Key K : analz (sees lost Spy evs))";
   178 by (etac otway.induct 1);
   179 by analz_sees_tac;
   180 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   181 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   182 (*14 seconds*)
   183 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   184 (*OR4, Fake*) 
   185 by (EVERY (map spy_analz_tac [3,2]));
   186 (*Base*)
   187 by (Blast_tac 1);
   188 qed_spec_mp "analz_image_freshK";
   189 
   190 
   191 goal thy
   192  "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>             \
   193 \        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   194 \        (K = KAB | Key K : analz (sees lost Spy evs))";
   195 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   196 qed "analz_insert_freshK";
   197 
   198 
   199 (*** The Key K uniquely identifies the Server's  message. **)
   200 
   201 goal thy 
   202  "!!evs. evs : otway lost ==>                              \
   203 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   204 \       Says Server B \
   205 \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
   206 \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs  \
   207 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
   208 by (etac otway.induct 1);
   209 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   210 by (Step_tac 1);
   211 (*Remaining cases: OR3 and OR4*)
   212 by (ex_strip_tac 2);
   213 by (Blast_tac 2);
   214 by (expand_case_tac "K = ?y" 1);
   215 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   216 (*...we assume X is a recent message and handle this case by contradiction*)
   217 by (blast_tac (!claset addSEs sees_Spy_partsEs
   218                        delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
   219 val lemma = result();
   220 
   221 
   222 goal thy 
   223 "!!evs. [| Says Server B                                           \
   224 \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
   225 \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
   226 \           : set_of_list evs;                                     \
   227 \          Says Server B'                                          \
   228 \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
   229 \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
   230 \           : set_of_list evs;                                     \
   231 \          evs : otway lost |]                                     \
   232 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   233 by (prove_unique_tac lemma 1);
   234 qed "unique_session_keys";
   235 
   236 
   237 
   238 (**** Authenticity properties relating to NA ****)
   239 
   240 (*If the encrypted message appears then it originated with the Server!*)
   241 goal thy 
   242  "!!evs. [| A ~: lost;  evs : otway lost |]                 \
   243 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
   244 \      : parts (sees lost Spy evs)                          \
   245 \     --> (EX NB. Says Server B                                          \
   246 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   247 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   248 \                  : set_of_list evs)";
   249 by parts_induct_tac;
   250 by (Fake_parts_insert_tac 1);
   251 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   252 (*OR3*)
   253 by (Blast_tac 1);
   254 qed_spec_mp "NA_Crypt_imp_Server_msg";
   255 
   256 
   257 (*Corollary: if A receives B's OR4 message then it originated with the Server.
   258   Freshness may be inferred from nonce NA.*)
   259 goal thy 
   260  "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   261 \            : set_of_list evs;                                         \
   262 \           A ~: lost;  evs : otway lost |]                             \
   263 \        ==> EX NB. Says Server B                                       \
   264 \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
   265 \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   266 \                   : set_of_list evs";
   267 by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   268                       addEs  sees_Spy_partsEs) 1);
   269 qed "A_trusts_OR4";
   270 
   271 
   272 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   273     Does not in itself guarantee security: an attack could violate 
   274     the premises, e.g. by having A=Spy **)
   275 
   276 goal thy 
   277  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   278 \        ==> Says Server B                                                 \
   279 \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
   280 \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
   281 \            : set_of_list evs -->                                         \
   282 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   283 \            Key K ~: analz (sees lost Spy evs)";
   284 by (etac otway.induct 1);
   285 by analz_sees_tac;
   286 by (ALLGOALS
   287     (asm_simp_tac (!simpset addcongs [conj_cong] 
   288                             addsimps [not_parts_not_analz,
   289                                       analz_insert_freshK]
   290                             setloop split_tac [expand_if])));
   291 (*OR3*)
   292 by (blast_tac (!claset addSEs sees_Spy_partsEs
   293                        addIs [impOfSubs analz_subset_parts]) 2);
   294 (*Oops*) 
   295 by (blast_tac (!claset addDs [unique_session_keys]) 3);
   296 (*OR4, Fake*) 
   297 by (REPEAT_FIRST spy_analz_tac);
   298 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   299 
   300 goal thy 
   301  "!!evs. [| Says Server B                                           \
   302 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   303 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   304 \             : set_of_list evs;                                    \
   305 \           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
   306 \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   307 \        ==> Key K ~: analz (sees lost Spy evs)";
   308 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   309 by (blast_tac (!claset addSEs [lemma]) 1);
   310 qed "Spy_not_see_encrypted_key";
   311 
   312 
   313 goal thy 
   314  "!!evs. [| C ~: {A,B,Server};                                      \
   315 \           Says Server B                                           \
   316 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   317 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   318 \             : set_of_list evs;                                    \
   319 \           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
   320 \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   321 \        ==> Key K ~: analz (sees lost C evs)";
   322 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   323 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   324 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   325 by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
   326 qed "Agent_not_see_encrypted_key";
   327 
   328 
   329 (**** Authenticity properties relating to NB ****)
   330 
   331 (*If the encrypted message appears then it originated with the Server!*)
   332 goal thy 
   333  "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
   334 \    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                     \
   335 \         : parts (sees lost Spy evs)                                       \
   336 \        --> (EX NA. Says Server B                                          \
   337 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   338 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   339 \                     : set_of_list evs)";
   340 by parts_induct_tac;
   341 by (Fake_parts_insert_tac 1);
   342 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   343 (*OR3*)
   344 by (Blast_tac 1);
   345 qed_spec_mp "NB_Crypt_imp_Server_msg";
   346 
   347 
   348 (*Guarantee for B: if it gets a well-formed certificate then the Server
   349   has sent the correct message in round 3.*)
   350 goal thy 
   351  "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   352 \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   353 \            : set_of_list evs |]                                           \
   354 \        ==> EX NA. Says Server B                                           \
   355 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   356 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   357 \                     : set_of_list evs";
   358 by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   359                        addEs  sees_Spy_partsEs) 1);
   360 qed "B_trusts_OR3";