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