src/HOL/Auth/OtwayRees_AN.ML
author paulson
Fri Jul 04 17:34:55 1997 +0200 (1997-07-04)
changeset 3500 0d8ad2f192d8
parent 3466 30791e5a69c4
child 3516 470626799511
permissions -rw-r--r--
New constant "certificate"--just an abbreviation
     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 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 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 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 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                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 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 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   183 (*Fake*) 
   184 by (spy_analz_tac 2);
   185 (*Base*)
   186 by (Blast_tac 1);
   187 qed_spec_mp "analz_image_freshK";
   188 
   189 
   190 goal thy
   191  "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
   192 \        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
   193 \        (K = KAB | Key K : analz (sees lost Spy evs))";
   194 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   195 qed "analz_insert_freshK";
   196 
   197 
   198 (*** The Key K uniquely identifies the Server's  message. **)
   199 
   200 goal thy 
   201  "!!evs. evs : otway lost ==>                              \
   202 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   203 \       Says Server B                                      \
   204 \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},             \
   205 \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
   206 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
   207 by (etac otway.induct 1);
   208 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   209 by (Step_tac 1);
   210 (*Remaining cases: OR3 and OR4*)
   211 by (ex_strip_tac 2);
   212 by (Blast_tac 2);
   213 by (expand_case_tac "K = ?y" 1);
   214 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   215 (*...we assume X is a recent message and handle this case by contradiction*)
   216 by (blast_tac (!claset addSEs sees_Spy_partsEs
   217                        delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
   218 val lemma = result();
   219 
   220 
   221 goal thy 
   222 "!!evs. [| Says Server B                                           \
   223 \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
   224 \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
   225 \           : set evs;                                             \
   226 \          Says Server B'                                          \
   227 \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
   228 \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
   229 \           : set evs;                                             \
   230 \          evs : otway lost |]                                     \
   231 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   232 by (prove_unique_tac lemma 1);
   233 qed "unique_session_keys";
   234 
   235 
   236 
   237 (**** Authenticity properties relating to NA ****)
   238 
   239 (*If the encrypted message appears then it originated with the Server!*)
   240 goal thy 
   241  "!!evs. [| A ~: lost;  evs : otway lost |]                 \
   242 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
   243 \      : parts (sees lost Spy evs)                          \
   244 \     --> (EX NB. Says Server B                                          \
   245 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   246 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   247 \                  : set evs)";
   248 by parts_induct_tac;
   249 by (Fake_parts_insert_tac 1);
   250 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   251 (*OR3*)
   252 by (Blast_tac 1);
   253 qed_spec_mp "NA_Crypt_imp_Server_msg";
   254 
   255 
   256 (*Corollary: if A receives B's OR4 message then it originated with the Server.
   257   Freshness may be inferred from nonce NA.*)
   258 goal thy 
   259  "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   260 \            : set evs;                                                 \
   261 \           A ~: lost;  evs : otway lost |]                             \
   262 \        ==> EX NB. Says Server B                                       \
   263 \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
   264 \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   265 \                   : set evs";
   266 by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   267                       addEs  sees_Spy_partsEs) 1);
   268 qed "A_trusts_OR4";
   269 
   270 
   271 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   272     Does not in itself guarantee security: an attack could violate 
   273     the premises, e.g. by having A=Spy **)
   274 
   275 goal thy 
   276  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   277 \        ==> Says Server B                                                 \
   278 \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
   279 \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
   280 \            : set evs -->                                                 \
   281 \            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
   282 \            Key K ~: analz (sees lost Spy evs)";
   283 by (etac otway.induct 1);
   284 by analz_sees_tac;
   285 by (ALLGOALS
   286     (asm_simp_tac (!simpset addcongs [conj_cong] 
   287                             addsimps [analz_insert_eq, not_parts_not_analz, 
   288 				      analz_insert_freshK]
   289                             setloop split_tac [expand_if])));
   290 (*Oops*)
   291 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
   292 (*OR4*) 
   293 by (Blast_tac 3);
   294 (*OR3*)
   295 by (blast_tac (!claset addSEs sees_Spy_partsEs
   296                        addIs [impOfSubs analz_subset_parts]) 2);
   297 (*Fake*) 
   298 by (spy_analz_tac 1);
   299 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   300 
   301 goal thy 
   302  "!!evs. [| Says Server B                                           \
   303 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   304 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   305 \             : set evs;                                            \
   306 \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   307 \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   308 \        ==> Key K ~: analz (sees lost Spy evs)";
   309 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   310 by (blast_tac (!claset addSEs [lemma]) 1);
   311 qed "Spy_not_see_encrypted_key";
   312 
   313 
   314 goal thy 
   315  "!!evs. [| C ~: {A,B,Server};                                      \
   316 \           Says Server B                                           \
   317 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   318 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   319 \             : set evs;                                            \
   320 \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   321 \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   322 \        ==> Key K ~: analz (sees lost C evs)";
   323 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   324 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   325 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   326 by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
   327 qed "Agent_not_see_encrypted_key";
   328 
   329 
   330 (**** Authenticity properties relating to NB ****)
   331 
   332 (*If the encrypted message appears then it originated with the Server!*)
   333 goal thy 
   334  "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
   335 \    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                     \
   336 \         : parts (sees lost Spy evs)                                       \
   337 \        --> (EX NA. Says Server B                                          \
   338 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   339 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   340 \                     : set evs)";
   341 by parts_induct_tac;
   342 by (Fake_parts_insert_tac 1);
   343 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   344 (*OR3*)
   345 by (Blast_tac 1);
   346 qed_spec_mp "NB_Crypt_imp_Server_msg";
   347 
   348 
   349 (*Guarantee for B: if it gets a well-formed certificate then the Server
   350   has sent the correct message in round 3.*)
   351 goal thy 
   352  "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   353 \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   354 \            : set evs |]                                                   \
   355 \        ==> EX NA. Says Server B                                           \
   356 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   357 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   358 \                     : set evs";
   359 by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   360                        addEs  sees_Spy_partsEs) 1);
   361 qed "B_trusts_OR3";