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