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