src/HOL/Auth/OtwayRees_AN.ML
author paulson
Fri Jul 11 13:32:39 1997 +0200 (1997-07-11)
changeset 3516 470626799511
parent 3466 30791e5a69c4
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Removal of monotonicity reasoning involving "lost" and the theorem
Agent_not_see_encrypted_key, which (a) is never used and (b) becomes harder
to prove when Notes is available.
     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 (*Nobody sends themselves messages*)
    36 goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
    37 by (etac otway.induct 1);
    38 by (Auto_tac());
    39 qed_spec_mp "not_Says_to_self";
    40 Addsimps [not_Says_to_self];
    41 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    42 
    43 
    44 (** For reasoning about the encrypted portion of messages **)
    45 
    46 goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
    47 \                X : analz (sees lost Spy evs)";
    48 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    49 qed "OR4_analz_sees_Spy";
    50 
    51 goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    52 \                  : set evs ==> K : parts (sees lost Spy evs)";
    53 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    54 qed "Oops_parts_sees_Spy";
    55 
    56 (*OR4_analz_sees_Spy lets us treat those cases using the same 
    57   argument as for the Fake case.  This is possible for most, but not all,
    58   proofs, since Fake messages originate from the Spy. *)
    59 
    60 bind_thm ("OR4_parts_sees_Spy",
    61           OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    62 
    63 (*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    64   We instantiate the variable to "lost" since leaving it as a Var would
    65   interfere with simplification.*)
    66 val parts_induct_tac = 
    67     let val tac = forw_inst_tac [("lost","lost")] 
    68     in  etac otway.induct	   1 THEN 
    69         tac OR4_parts_sees_Spy     6 THEN
    70         tac Oops_parts_sees_Spy    7 THEN
    71 	prove_simple_subgoals_tac  1
    72     end;
    73 
    74 
    75 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    76     sends messages containing X! **)
    77 
    78 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    79 goal thy 
    80  "!!evs. evs : otway lost \
    81 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    82 by parts_induct_tac;
    83 by (Fake_parts_insert_tac 1);
    84 by (Blast_tac 1);
    85 qed "Spy_see_shrK";
    86 Addsimps [Spy_see_shrK];
    87 
    88 goal thy 
    89  "!!evs. evs : otway lost \
    90 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    91 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    92 qed "Spy_analz_shrK";
    93 Addsimps [Spy_analz_shrK];
    94 
    95 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    96 \                  evs : otway lost |] ==> A:lost";
    97 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    98 qed "Spy_see_shrK_D";
    99 
   100 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   101 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   102 
   103 
   104 (*Nobody can have used non-existent keys!*)
   105 goal thy "!!evs. evs : otway lost ==>          \
   106 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   107 by parts_induct_tac;
   108 (*Fake*)
   109 by (best_tac
   110       (!claset addIs [impOfSubs analz_subset_parts]
   111                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   112                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   113                addss (!simpset)) 1);
   114 (*OR3*)
   115 by (Blast_tac 1);
   116 qed_spec_mp "new_keys_not_used";
   117 
   118 bind_thm ("new_keys_not_analzd",
   119           [analz_subset_parts RS keysFor_mono,
   120            new_keys_not_used] MRS contra_subsetD);
   121 
   122 Addsimps [new_keys_not_used, new_keys_not_analzd];
   123 
   124 
   125 
   126 (*** Proofs involving analz ***)
   127 
   128 (*Describes the form of K and NA when the Server sends this message.*)
   129 goal thy 
   130  "!!evs. [| Says Server B                                           \
   131 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   132 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   133 \             : set evs;                                            \
   134 \           evs : otway lost |]                                     \
   135 \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   136 by (etac rev_mp 1);
   137 by (etac otway.induct 1);
   138 by (ALLGOALS Asm_simp_tac);
   139 by (Blast_tac 1);
   140 qed "Says_Server_message_form";
   141 
   142 
   143 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   144 val analz_sees_tac = 
   145     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   146     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   147     assume_tac 7 THEN
   148     REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   149 
   150 
   151 (****
   152  The following is to prove theorems of the form
   153 
   154   Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   155   Key K : analz (sees lost Spy evs)
   156 
   157  A more general formula must be proved inductively.
   158 ****)
   159 
   160 
   161 (** Session keys are not used to encrypt other session keys **)
   162 
   163 (*The equality makes the induction hypothesis easier to apply*)
   164 goal thy  
   165  "!!evs. evs : otway lost ==>                                    \
   166 \  ALL K KK. KK <= Compl (range shrK) -->                        \
   167 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
   168 \            (K : KK | Key K : analz (sees lost Spy evs))";
   169 by (etac otway.induct 1);
   170 by analz_sees_tac;
   171 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   172 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   173 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   174 (*Fake*) 
   175 by (spy_analz_tac 2);
   176 (*Base*)
   177 by (Blast_tac 1);
   178 qed_spec_mp "analz_image_freshK";
   179 
   180 
   181 goal thy
   182  "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
   183 \        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
   184 \        (K = KAB | Key K : analz (sees lost Spy evs))";
   185 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   186 qed "analz_insert_freshK";
   187 
   188 
   189 (*** The Key K uniquely identifies the Server's  message. **)
   190 
   191 goal thy 
   192  "!!evs. evs : otway lost ==>                              \
   193 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   194 \       Says Server B                                      \
   195 \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},             \
   196 \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
   197 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
   198 by (etac otway.induct 1);
   199 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   200 by (Step_tac 1);
   201 (*Remaining cases: OR3 and OR4*)
   202 by (ex_strip_tac 2);
   203 by (Blast_tac 2);
   204 by (expand_case_tac "K = ?y" 1);
   205 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   206 (*...we assume X is a recent message and handle this case by contradiction*)
   207 by (blast_tac (!claset addSEs sees_Spy_partsEs
   208                        delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
   209 val lemma = result();
   210 
   211 
   212 goal thy 
   213 "!!evs. [| Says Server B                                           \
   214 \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
   215 \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
   216 \           : set evs;                                             \
   217 \          Says Server B'                                          \
   218 \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
   219 \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
   220 \           : set evs;                                             \
   221 \          evs : otway lost |]                                     \
   222 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   223 by (prove_unique_tac lemma 1);
   224 qed "unique_session_keys";
   225 
   226 
   227 
   228 (**** Authenticity properties relating to NA ****)
   229 
   230 (*If the encrypted message appears then it originated with the Server!*)
   231 goal thy 
   232  "!!evs. [| A ~: lost;  evs : otway lost |]                 \
   233 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
   234 \      : parts (sees lost Spy evs)                          \
   235 \     --> (EX NB. Says Server B                                          \
   236 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   237 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   238 \                  : set evs)";
   239 by parts_induct_tac;
   240 by (Fake_parts_insert_tac 1);
   241 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   242 (*OR3*)
   243 by (Blast_tac 1);
   244 qed_spec_mp "NA_Crypt_imp_Server_msg";
   245 
   246 
   247 (*Corollary: if A receives B's OR4 message then it originated with the Server.
   248   Freshness may be inferred from nonce NA.*)
   249 goal thy 
   250  "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   251 \            : set evs;                                                 \
   252 \           A ~: lost;  evs : otway lost |]                             \
   253 \        ==> EX NB. Says Server B                                       \
   254 \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
   255 \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   256 \                   : set evs";
   257 by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   258                       addEs  sees_Spy_partsEs) 1);
   259 qed "A_trusts_OR4";
   260 
   261 
   262 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   263     Does not in itself guarantee security: an attack could violate 
   264     the premises, e.g. by having A=Spy **)
   265 
   266 goal thy 
   267  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   268 \        ==> Says Server B                                                 \
   269 \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
   270 \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
   271 \            : set evs -->                                                 \
   272 \            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
   273 \            Key K ~: analz (sees lost Spy evs)";
   274 by (etac otway.induct 1);
   275 by analz_sees_tac;
   276 by (ALLGOALS
   277     (asm_simp_tac (!simpset addcongs [conj_cong] 
   278                             addsimps [analz_insert_eq, not_parts_not_analz, 
   279 				      analz_insert_freshK]
   280                             setloop split_tac [expand_if])));
   281 (*Oops*)
   282 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
   283 (*OR4*) 
   284 by (Blast_tac 3);
   285 (*OR3*)
   286 by (blast_tac (!claset addSEs sees_Spy_partsEs
   287                        addIs [impOfSubs analz_subset_parts]) 2);
   288 (*Fake*) 
   289 by (spy_analz_tac 1);
   290 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   291 
   292 goal thy 
   293  "!!evs. [| Says Server B                                           \
   294 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   295 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   296 \             : set evs;                                            \
   297 \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   298 \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   299 \        ==> Key K ~: analz (sees lost Spy evs)";
   300 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   301 by (blast_tac (!claset addSEs [lemma]) 1);
   302 qed "Spy_not_see_encrypted_key";
   303 
   304 
   305 (**** Authenticity properties relating to NB ****)
   306 
   307 (*If the encrypted message appears then it originated with the Server!*)
   308 goal thy 
   309  "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
   310 \    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                     \
   311 \         : parts (sees lost Spy evs)                                       \
   312 \        --> (EX NA. Says Server B                                          \
   313 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   314 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   315 \                     : set evs)";
   316 by parts_induct_tac;
   317 by (Fake_parts_insert_tac 1);
   318 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   319 (*OR3*)
   320 by (Blast_tac 1);
   321 qed_spec_mp "NB_Crypt_imp_Server_msg";
   322 
   323 
   324 (*Guarantee for B: if it gets a well-formed certificate then the Server
   325   has sent the correct message in round 3.*)
   326 goal thy 
   327  "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   328 \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   329 \            : set evs |]                                                   \
   330 \        ==> EX NA. Says Server B                                           \
   331 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   332 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   333 \                     : set evs";
   334 by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   335                        addEs  sees_Spy_partsEs) 1);
   336 qed "B_trusts_OR3";