src/HOL/Auth/OtwayRees_AN.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2891 d8f254ad1ab9
child 3102 4d01cdc119d2
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     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 (fast_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 (fast_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 (*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    73   harder to complete, since simplification does less for us.*)
    74 val parts_Fake_tac = 
    75     forw_inst_tac [("lost","lost")] OR4_parts_sees_Spy 6 THEN
    76     forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 7;
    77 
    78 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    79 fun parts_induct_tac i = SELECT_GOAL
    80     (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
    81              (*Fake message*)
    82              TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    83                                            impOfSubs Fake_parts_insert]
    84                                     addss (!simpset)) 2)) THEN
    85      (*Base case*)
    86      fast_tac (!claset addss (!simpset)) 1 THEN
    87      ALLGOALS Asm_simp_tac) i;
    88 
    89 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    90     sends messages containing X! **)
    91 
    92 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    93 goal thy 
    94  "!!evs. evs : otway lost \
    95 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    96 by (parts_induct_tac 1);
    97 by (Auto_tac());
    98 qed "Spy_see_shrK";
    99 Addsimps [Spy_see_shrK];
   100 
   101 goal thy 
   102  "!!evs. evs : otway lost \
   103 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   104 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   105 qed "Spy_analz_shrK";
   106 Addsimps [Spy_analz_shrK];
   107 
   108 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   109 \                  evs : otway lost |] ==> A:lost";
   110 by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
   111 qed "Spy_see_shrK_D";
   112 
   113 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   114 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   115 
   116 
   117 (*Nobody can have used non-existent keys!*)
   118 goal thy "!!evs. evs : otway lost ==>          \
   119 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   120 by (parts_induct_tac 1);
   121 (*Fake*)
   122 by (best_tac
   123       (!claset addIs [impOfSubs analz_subset_parts]
   124                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   125                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   126                unsafe_addss (!simpset)) 1);
   127 (*OR3*)
   128 by (fast_tac (!claset addss (!simpset)) 1);
   129 qed_spec_mp "new_keys_not_used";
   130 
   131 bind_thm ("new_keys_not_analzd",
   132           [analz_subset_parts RS keysFor_mono,
   133            new_keys_not_used] MRS contra_subsetD);
   134 
   135 Addsimps [new_keys_not_used, new_keys_not_analzd];
   136 
   137 
   138 
   139 (*** Proofs involving analz ***)
   140 
   141 (*Describes the form of K and NA when the Server sends this message.*)
   142 goal thy 
   143  "!!evs. [| Says Server B                                           \
   144 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   145 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   146 \             : set_of_list evs;                                    \
   147 \           evs : otway lost |]                                     \
   148 \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   149 by (etac rev_mp 1);
   150 by (etac otway.induct 1);
   151 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   152 qed "Says_Server_message_form";
   153 
   154 
   155 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   156 val analz_Fake_tac = 
   157     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   158     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   159     assume_tac 7 THEN
   160     REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   161 
   162 
   163 (****
   164  The following is to prove theorems of the form
   165 
   166   Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   167   Key K : analz (sees lost Spy evs)
   168 
   169  A more general formula must be proved inductively.
   170 ****)
   171 
   172 
   173 (** Session keys are not used to encrypt other session keys **)
   174 
   175 (*The equality makes the induction hypothesis easier to apply*)
   176 goal thy  
   177  "!!evs. evs : otway 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 otway.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 (*14 seconds*)
   186 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   187 (*OR4, Fake*) 
   188 by (EVERY (map spy_analz_tac [3,2]));
   189 (*Base*)
   190 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   191 qed_spec_mp "analz_image_freshK";
   192 
   193 
   194 goal thy
   195  "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>             \
   196 \        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   197 \        (K = KAB | Key K : analz (sees lost Spy evs))";
   198 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   199 qed "analz_insert_freshK";
   200 
   201 
   202 (*** The Key K uniquely identifies the Server's  message. **)
   203 
   204 goal thy 
   205  "!!evs. evs : otway lost ==>                              \
   206 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   207 \       Says Server B \
   208 \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
   209 \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs  \
   210 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
   211 by (etac otway.induct 1);
   212 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   213 by (Step_tac 1);
   214 (*Remaining cases: OR3 and OR4*)
   215 by (ex_strip_tac 2);
   216 by (Fast_tac 2);
   217 by (expand_case_tac "K = ?y" 1);
   218 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   219 (*...we assume X is a recent message and handle this case by contradiction*)
   220 by (fast_tac (!claset addSEs sees_Spy_partsEs
   221                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
   222                       addss (!simpset addsimps [parts_insertI])) 1);
   223 val lemma = result();
   224 
   225 
   226 goal thy 
   227 "!!evs. [| 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 \          Says Server B'                                          \
   232 \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
   233 \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
   234 \           : set_of_list evs;                                     \
   235 \          evs : otway lost |]                                     \
   236 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   237 by (prove_unique_tac lemma 1);
   238 qed "unique_session_keys";
   239 
   240 
   241 
   242 (**** Authenticity properties relating to NA ****)
   243 
   244 (*If the encrypted message appears then it originated with the Server!*)
   245 goal thy 
   246  "!!evs. [| A ~: lost;  evs : otway lost |]                 \
   247 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
   248 \      : parts (sees lost Spy evs)                          \
   249 \     --> (EX NB. Says Server B                                          \
   250 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   251 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   252 \                  : set_of_list evs)";
   253 by (parts_induct_tac 1);
   254 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   255 (*OR3*)
   256 by (Fast_tac 1);
   257 qed_spec_mp "NA_Crypt_imp_Server_msg";
   258 
   259 
   260 (*Corollary: if A receives B's OR4 message then it originated with the Server.
   261   Freshness may be inferred from nonce NA.*)
   262 goal thy 
   263  "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   264 \            : set_of_list evs;                                         \
   265 \           A ~: lost;  evs : otway lost |]                             \
   266 \        ==> EX NB. Says Server B                                       \
   267 \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
   268 \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   269 \                   : set_of_list evs";
   270 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   271                       addEs  sees_Spy_partsEs) 1);
   272 qed "A_trusts_OR4";
   273 
   274 
   275 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   276     Does not in itself guarantee security: an attack could violate 
   277     the premises, e.g. by having A=Spy **)
   278 
   279 goal thy 
   280  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   281 \        ==> Says Server B                                                 \
   282 \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
   283 \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
   284 \            : set_of_list evs -->                                         \
   285 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   286 \            Key K ~: analz (sees lost Spy evs)";
   287 by (etac otway.induct 1);
   288 by analz_Fake_tac;
   289 by (ALLGOALS
   290     (asm_simp_tac (!simpset addcongs [conj_cong] 
   291                             addsimps [not_parts_not_analz,
   292                                       analz_insert_freshK]
   293                             setloop split_tac [expand_if])));
   294 (*OR3*)
   295 by (fast_tac (!claset delrules [impCE]
   296                       addSEs sees_Spy_partsEs
   297                       addIs [impOfSubs analz_subset_parts]
   298                       addss (!simpset addsimps [parts_insert2])) 2);
   299 (*Oops*) 
   300 by (best_tac (!claset addDs [unique_session_keys] unsafe_addss (!simpset)) 3);
   301 (*OR4, Fake*) 
   302 by (REPEAT_FIRST spy_analz_tac);
   303 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   304 
   305 goal thy 
   306  "!!evs. [| Says Server B                                           \
   307 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   308 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   309 \             : set_of_list evs;                                    \
   310 \           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
   311 \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   312 \        ==> Key K ~: analz (sees lost Spy evs)";
   313 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   314 by (blast_tac (!claset addSEs [lemma]) 1);
   315 qed "Spy_not_see_encrypted_key";
   316 
   317 
   318 goal thy 
   319  "!!evs. [| C ~: {A,B,Server};                                      \
   320 \           Says Server B                                           \
   321 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   322 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   323 \             : set_of_list evs;                                    \
   324 \           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
   325 \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   326 \        ==> Key K ~: analz (sees lost C evs)";
   327 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   328 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   329 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   330 by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
   331 qed "Agent_not_see_encrypted_key";
   332 
   333 
   334 (**** Authenticity properties relating to NB ****)
   335 
   336 (*If the encrypted message appears then it originated with the Server!*)
   337 goal thy 
   338  "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
   339 \    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                     \
   340 \         : parts (sees lost Spy evs)                                       \
   341 \        --> (EX NA. Says Server B                                          \
   342 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   343 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   344 \                     : set_of_list evs)";
   345 by (parts_induct_tac 1);
   346 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   347 (*OR3*)
   348 by (Fast_tac 1);
   349 qed_spec_mp "NB_Crypt_imp_Server_msg";
   350 
   351 
   352 (*Guarantee for B: if it gets a well-formed certificate then the Server
   353   has sent the correct message in round 3.*)
   354 goal thy 
   355  "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   356 \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   357 \            : set_of_list evs |]                                           \
   358 \        ==> EX NA. Says Server B                                           \
   359 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   360 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   361 \                     : set_of_list evs";
   362 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   363                       addEs  sees_Spy_partsEs) 1);
   364 qed "B_trusts_OR3";