src/HOL/Auth/OtwayRees_AN.ML
author paulson
Mon Jul 14 12:47:21 1997 +0200 (1997-07-14)
changeset 3519 ab0a9fbed4c0
parent 3516 470626799511
child 3543 82f33248d89d
permissions -rw-r--r--
Changing "lost" from a parameter of protocol definitions to a constant.

Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
theorem was never used, and its original proof was also broken
the introduction of the "Notes" constructor.
     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] 
   272                             addsimps [analz_insert_eq, not_parts_not_analz, 
   273 				      analz_insert_freshK]
   274                             setloop split_tac [expand_if])));
   275 (*Oops*)
   276 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
   277 (*OR4*) 
   278 by (Blast_tac 3);
   279 (*OR3*)
   280 by (blast_tac (!claset addSEs sees_Spy_partsEs
   281                        addIs [impOfSubs analz_subset_parts]) 2);
   282 (*Fake*) 
   283 by (spy_analz_tac 1);
   284 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   285 
   286 goal thy 
   287  "!!evs. [| Says Server B                                           \
   288 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   289 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   290 \             : set evs;                                            \
   291 \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   292 \           A ~: lost;  B ~: lost;  evs : otway |]                  \
   293 \        ==> Key K ~: analz (sees Spy evs)";
   294 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   295 by (blast_tac (!claset addSEs [lemma]) 1);
   296 qed "Spy_not_see_encrypted_key";
   297 
   298 
   299 (**** Authenticity properties relating to NB ****)
   300 
   301 (*If the encrypted message appears then it originated with the Server!*)
   302 goal thy 
   303  "!!evs. [| B ~: lost;  evs : otway |]                                 \
   304 \    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                \
   305 \         : parts (sees Spy evs)                                       \
   306 \        --> (EX NA. 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 evs)";
   310 by (parts_induct_tac 1);
   311 by (Fake_parts_insert_tac 1);
   312 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   313 (*OR3*)
   314 by (Blast_tac 1);
   315 qed_spec_mp "NB_Crypt_imp_Server_msg";
   316 
   317 
   318 (*Guarantee for B: if it gets a well-formed certificate then the Server
   319   has sent the correct message in round 3.*)
   320 goal thy 
   321  "!!evs. [| B ~: lost;  evs : otway;                                        \
   322 \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   323 \            : set evs |]                                                   \
   324 \        ==> EX NA. Says Server B                                           \
   325 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   326 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   327 \                     : set evs";
   328 by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   329                        addEs  sees_Spy_partsEs) 1);
   330 qed "B_trusts_OR3";