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