src/HOL/Auth/Recur.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14207 f20fbb141673
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:      HOL/Auth/Recur
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 *)
     6 
     7 header{*The Otway-Bull Recursive Authentication Protocol*}
     8 
     9 theory Recur = Public:
    10 
    11 text{*End marker for message bundles*}
    12 syntax        END :: "msg"
    13 translations "END" == "Number 0"
    14 
    15 (*Two session keys are distributed to each agent except for the initiator,
    16         who receives one.
    17   Perhaps the two session keys could be bundled into a single message.
    18 *)
    19 consts     respond :: "event list => (msg*msg*key)set"
    20 inductive "respond evs" (*Server's response to the nested message*)
    21   intros
    22    One:  "Key KAB \<notin> used evs
    23           ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|},
    24                {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|},
    25                KAB)   \<in> respond evs"
    26 
    27     (*The most recent session key is passed up to the caller*)
    28    Cons: "[| (PA, RA, KAB) \<in> respond evs;
    29              Key KBC \<notin> used evs;  Key KBC \<notin> parts {RA};
    30              PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} |]
    31           ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|},
    32                {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
    33                  Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
    34                  RA|},
    35                KBC)
    36               \<in> respond evs"
    37 
    38 
    39 (*Induction over "respond" can be difficult due to the complexity of the
    40   subgoals.  Set "responses" captures the general form of certificates.
    41 *)
    42 consts     responses :: "event list => msg set"
    43 inductive "responses evs"
    44   intros
    45     (*Server terminates lists*)
    46    Nil:  "END \<in> responses evs"
    47 
    48    Cons: "[| RA \<in> responses evs;  Key KAB \<notin> used evs |]
    49           ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
    50                 RA|}  \<in> responses evs"
    51 
    52 
    53 consts     recur   :: "event list set"
    54 inductive "recur"
    55   intros
    56          (*Initial trace is empty*)
    57    Nil:  "[] \<in> recur"
    58 
    59          (*The spy MAY say anything he CAN say.  Common to
    60            all similar protocols.*)
    61    Fake: "[| evsf \<in> recur;  X \<in> synth (analz (knows Spy evsf)) |]
    62           ==> Says Spy B X  # evsf \<in> recur"
    63 
    64          (*Alice initiates a protocol run.
    65            END is a placeholder to terminate the nesting.*)
    66    RA1:  "[| evs1 \<in> recur;  Nonce NA \<notin> used evs1 |]
    67           ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
    68               # evs1 \<in> recur"
    69 
    70          (*Bob's response to Alice's message.  C might be the Server.
    71            We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
    72            it complicates proofs, so B may respond to any message at all!*)
    73    RA2:  "[| evs2 \<in> recur;  Nonce NB \<notin> used evs2;
    74              Says A' B PA \<in> set evs2 |]
    75           ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
    76               # evs2 \<in> recur"
    77 
    78          (*The Server receives Bob's message and prepares a response.*)
    79    RA3:  "[| evs3 \<in> recur;  Says B' Server PB \<in> set evs3;
    80              (PB,RB,K) \<in> respond evs3 |]
    81           ==> Says Server B RB # evs3 \<in> recur"
    82 
    83          (*Bob receives the returned message and compares the Nonces with
    84            those in the message he previously sent the Server.*)
    85    RA4:  "[| evs4 \<in> recur;
    86              Says B  C {|XH, Agent B, Agent C, Nonce NB,
    87                          XA, Agent A, Agent B, Nonce NA, P|} \<in> set evs4;
    88              Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
    89                          Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
    90                          RA|} \<in> set evs4 |]
    91           ==> Says B A RA # evs4 \<in> recur"
    92 
    93    (*No "oops" message can easily be expressed.  Each session key is
    94      associated--in two separate messages--with two nonces.  This is
    95      one try, but it isn't that useful.  Re domino attack, note that
    96      Recur.ML proves that each session key is secure provided the two
    97      peers are, even if there are compromised agents elsewhere in
    98      the chain.  Oops cases proved using parts_cut, Key_in_keysFor_parts,
    99      etc.
   100 
   101    Oops:  "[| evso \<in> recur;  Says Server B RB \<in> set evso;
   102 	      RB \<in> responses evs';  Key K \<in> parts {RB} |]
   103            ==> Notes Spy {|Key K, RB|} # evso \<in> recur"
   104   *)
   105 
   106 
   107 declare Says_imp_knows_Spy [THEN analz.Inj, dest]
   108 declare parts.Body  [dest]
   109 declare analz_into_parts [dest]
   110 declare Fake_parts_insert_in_Un  [dest]
   111 
   112 
   113 (** Possibility properties: traces that reach the end
   114         ONE theorem would be more elegant and faster!
   115         By induction on a list of agents (no repetitions)
   116 **)
   117 
   118 
   119 text{*Simplest case: Alice goes directly to the server*}
   120 lemma "Key K \<notin> used [] 
   121        ==> \<exists>NA. \<exists>evs \<in> recur.
   122               Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
   123                     END|}  \<in> set evs"
   124 apply (intro exI bexI)
   125 apply (rule_tac [2] recur.Nil [THEN recur.RA1, 
   126                              THEN recur.RA3 [OF _ _ respond.One]])
   127 apply (possibility, simp add: used_Cons) 
   128 done
   129 
   130 
   131 text{*Case two: Alice, Bob and the server*}
   132 lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K';
   133           Nonce NA \<notin> used []; Nonce NB \<notin> used []; NA < NB |]
   134        ==> \<exists>NA. \<exists>evs \<in> recur.
   135         Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
   136                    END|}  \<in> set evs"
   137 apply (intro exI bexI)
   138 apply (rule_tac [2] 
   139           recur.Nil
   140            [THEN recur.RA1 [of _ NA], 
   141 	    THEN recur.RA2 [of _ NB],
   142 	    THEN recur.RA3 [OF _ _ respond.One 
   143                                      [THEN respond.Cons [of _ _ K _ K']]],
   144 	    THEN recur.RA4], possibility)
   145 apply (auto simp add: used_Cons)
   146 done
   147 
   148 (*Case three: Alice, Bob, Charlie and the server Rather slow (5 seconds)*)
   149 lemma "[| Key K \<notin> used []; Key K' \<notin> used [];  
   150           Key K'' \<notin> used []; K \<noteq> K'; K' \<noteq> K''; K \<noteq> K'';
   151           Nonce NA \<notin> used []; Nonce NB \<notin> used []; Nonce NC \<notin> used []; 
   152           NA < NB; NB < NC |]
   153        ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
   154              Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
   155                         END|}  \<in> set evs"
   156 apply (intro exI bexI)
   157 apply (rule_tac [2] 
   158           recur.Nil [THEN recur.RA1, 
   159                      THEN recur.RA2, THEN recur.RA2,
   160                      THEN recur.RA3 
   161                           [OF _ _ respond.One 
   162                                   [THEN respond.Cons, THEN respond.Cons]],
   163                      THEN recur.RA4, THEN recur.RA4])
   164 apply (tactic "basic_possibility_tac")
   165 apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)")
   166 done
   167 
   168 
   169 lemma respond_imp_not_used: "(PA,RB,KAB) \<in> respond evs ==> Key KAB \<notin> used evs"
   170 by (erule respond.induct, simp_all)
   171 
   172 lemma Key_in_parts_respond [rule_format]:
   173    "[| Key K \<in> parts {RB};  (PB,RB,K') \<in> respond evs |] ==> Key K \<notin> used evs"
   174 apply (erule rev_mp, erule respond.induct)
   175 apply (auto dest: Key_not_used respond_imp_not_used)
   176 done
   177 
   178 text{*Simple inductive reasoning about responses*}
   179 lemma respond_imp_responses:
   180      "(PA,RB,KAB) \<in> respond evs ==> RB \<in> responses evs"
   181 apply (erule respond.induct)
   182 apply (blast intro!: respond_imp_not_used responses.intros)+
   183 done
   184 
   185 
   186 (** For reasoning about the encrypted portion of messages **)
   187 
   188 lemmas RA2_analz_spies = Says_imp_spies [THEN analz.Inj]
   189 
   190 lemma RA4_analz_spies:
   191      "Says C' B {|Crypt K X, X', RA|} \<in> set evs ==> RA \<in> analz (spies evs)"
   192 by blast
   193 
   194 
   195 (*RA2_analz... and RA4_analz... let us treat those cases using the same
   196   argument as for the Fake case.  This is possible for most, but not all,
   197   proofs: Fake does not invent new nonces (as in RA2), and of course Fake
   198   messages originate from the Spy. *)
   199 
   200 lemmas RA2_parts_spies =  RA2_analz_spies [THEN analz_into_parts]
   201 lemmas RA4_parts_spies =  RA4_analz_spies [THEN analz_into_parts]
   202 
   203 
   204 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
   205     sends messages containing X! **)
   206 
   207 (** Spy never sees another agent's shared key! (unless it's bad at start) **)
   208 
   209 lemma Spy_see_shrK [simp]:
   210      "evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   211 apply (erule recur.induct, auto)
   212 txt{*RA3.  It's ugly to call auto twice, but it seems necessary.*}
   213 apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
   214 done
   215 
   216 lemma Spy_analz_shrK [simp]:
   217      "evs \<in> recur ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   218 by auto
   219 
   220 lemma Spy_see_shrK_D [dest!]:
   221      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> recur|] ==> A \<in> bad"
   222 by (blast dest: Spy_see_shrK)
   223 
   224 
   225 (*** Proofs involving analz ***)
   226 
   227 (** Session keys are not used to encrypt other session keys **)
   228 
   229 (*Version for "responses" relation.  Handles case RA3 in the theorem below.
   230   Note that it holds for *any* set H (not just "spies evs")
   231   satisfying the inductive hypothesis.*)
   232 lemma resp_analz_image_freshK_lemma:
   233      "[| RB \<in> responses evs;
   234          \<forall>K KK. KK \<subseteq> - (range shrK) -->
   235                    (Key K \<in> analz (Key`KK Un H)) =
   236                    (K \<in> KK | Key K \<in> analz H) |]
   237      ==> \<forall>K KK. KK \<subseteq> - (range shrK) -->
   238                    (Key K \<in> analz (insert RB (Key`KK Un H))) =
   239                    (K \<in> KK | Key K \<in> analz (insert RB H))"
   240 apply (erule responses.induct)
   241 apply (simp_all del: image_insert
   242 	        add: analz_image_freshK_simps, auto)
   243 done 
   244 
   245 
   246 text{*Version for the protocol.  Proof is easy, thanks to the lemma.*}
   247 lemma raw_analz_image_freshK:
   248  "evs \<in> recur ==>
   249    \<forall>K KK. KK \<subseteq> - (range shrK) -->
   250           (Key K \<in> analz (Key`KK Un (spies evs))) =
   251           (K \<in> KK | Key K \<in> analz (spies evs))"
   252 apply (erule recur.induct)
   253 apply (drule_tac [4] RA2_analz_spies,
   254        drule_tac [5] respond_imp_responses,
   255        drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
   256 txt{*RA3*}
   257 apply (simp_all add: resp_analz_image_freshK_lemma)
   258 done
   259 
   260 
   261 (*Instance of the lemma with H replaced by (spies evs):
   262    [| RB \<in> responses evs;  evs \<in> recur; |]
   263    ==> KK \<subseteq> - (range shrK) -->
   264        Key K \<in> analz (insert RB (Key`KK Un spies evs)) =
   265        (K \<in> KK | Key K \<in> analz (insert RB (spies evs)))
   266 *)
   267 lemmas resp_analz_image_freshK =  
   268        resp_analz_image_freshK_lemma [OF _ raw_analz_image_freshK]
   269 
   270 lemma analz_insert_freshK:
   271      "[| evs \<in> recur;  KAB \<notin> range shrK |]
   272       ==> (Key K \<in> analz (insert (Key KAB) (spies evs))) =
   273           (K = KAB | Key K \<in> analz (spies evs))"
   274 by (simp del: image_insert
   275          add: analz_image_freshK_simps raw_analz_image_freshK)
   276 
   277 
   278 text{*Everything that's hashed is already in past traffic. *}
   279 lemma Hash_imp_body:
   280      "[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
   281          evs \<in> recur;  A \<notin> bad |] ==> X \<in> parts (spies evs)"
   282 apply (erule rev_mp)
   283 apply (erule recur.induct,
   284        drule_tac [6] RA4_parts_spies,
   285        drule_tac [5] respond_imp_responses,
   286        drule_tac [4] RA2_parts_spies)
   287 txt{*RA3 requires a further induction*}
   288 apply (erule_tac [5] responses.induct, simp_all)
   289 txt{*Fake*}
   290 apply (blast intro: parts_insertI)
   291 done
   292 
   293 
   294 (** The Nonce NA uniquely identifies A's message.
   295     This theorem applies to steps RA1 and RA2!
   296 
   297   Unicity is not used in other proofs but is desirable in its own right.
   298 **)
   299 
   300 lemma unique_NA:
   301   "[| Hash {|Key(shrK A), Agent A, B, NA, P|} \<in> parts (spies evs);
   302       Hash {|Key(shrK A), Agent A, B',NA, P'|} \<in> parts (spies evs);
   303       evs \<in> recur;  A \<notin> bad |]
   304     ==> B=B' & P=P'"
   305 apply (erule rev_mp, erule rev_mp)
   306 apply (erule recur.induct,
   307        drule_tac [5] respond_imp_responses)
   308 apply (force, simp_all)
   309 txt{*Fake*}
   310 apply blast
   311 apply (erule_tac [3] responses.induct)
   312 txt{*RA1,2: creation of new Nonce*}
   313 apply simp_all
   314 apply (blast dest!: Hash_imp_body)+
   315 done
   316 
   317 
   318 (*** Lemmas concerning the Server's response
   319       (relations "respond" and "responses")
   320 ***)
   321 
   322 lemma shrK_in_analz_respond [simp]:
   323      "[| RB \<in> responses evs;  evs \<in> recur |]
   324   ==> (Key (shrK B) \<in> analz (insert RB (spies evs))) = (B:bad)"
   325 apply (erule responses.induct)
   326 apply (simp_all del: image_insert
   327                 add: analz_image_freshK_simps resp_analz_image_freshK, auto) 
   328 done
   329 
   330 
   331 lemma resp_analz_insert_lemma:
   332      "[| Key K \<in> analz (insert RB H);
   333          \<forall>K KK. KK \<subseteq> - (range shrK) -->
   334                    (Key K \<in> analz (Key`KK Un H)) =
   335                    (K \<in> KK | Key K \<in> analz H);
   336          RB \<in> responses evs |]
   337      ==> (Key K \<in> parts{RB} | Key K \<in> analz H)"
   338 apply (erule rev_mp, erule responses.induct)
   339 apply (simp_all del: image_insert
   340              add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
   341 txt{*Simplification using two distinct treatments of "image"*}
   342 apply (simp add: parts_insert2, blast)
   343 done
   344 
   345 lemmas resp_analz_insert =
   346        resp_analz_insert_lemma [OF _ raw_analz_image_freshK]
   347 
   348 text{*The last key returned by respond indeed appears in a certificate*}
   349 lemma respond_certificate:
   350      "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \<in> respond evs
   351       ==> Crypt (shrK A) {|Key K, B, NA|} \<in> parts {RA}"
   352 apply (ind_cases "(X, RA, K) \<in> respond evs")
   353 apply simp_all
   354 done
   355 
   356 (*This unicity proof differs from all the others in the HOL/Auth directory.
   357   The conclusion isn't quite unicity but duplicity, in that there are two
   358   possibilities.  Also, the presence of two different matching messages in
   359   the inductive step complicates the case analysis.  Unusually for such proofs,
   360   the quantifiers appear to be necessary.*)
   361 lemma unique_lemma [rule_format]:
   362      "(PB,RB,KXY) \<in> respond evs ==>
   363       \<forall>A B N. Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB} -->
   364       (\<forall>A' B' N'. Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB} -->
   365       (A'=A & B'=B) | (A'=B & B'=A))"
   366 apply (erule respond.induct)
   367 apply (simp_all add: all_conj_distrib)
   368 apply (blast dest: respond_certificate)
   369 done
   370 
   371 lemma unique_session_keys:
   372      "[| Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB};
   373          Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB};
   374          (PB,RB,KXY) \<in> respond evs |]
   375       ==> (A'=A & B'=B) | (A'=B & B'=A)"
   376 by (rule unique_lemma, auto)
   377 
   378 
   379 (** Crucial secrecy property: Spy does not see the keys sent in msg RA3
   380     Does not in itself guarantee security: an attack could violate
   381     the premises, e.g. by having A=Spy **)
   382 
   383 lemma respond_Spy_not_see_session_key [rule_format]:
   384      "[| (PB,RB,KAB) \<in> respond evs;  evs \<in> recur |]
   385       ==> \<forall>A A' N. A \<notin> bad & A' \<notin> bad -->
   386           Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts{RB} -->
   387           Key K \<notin> analz (insert RB (spies evs))"
   388 apply (erule respond.induct)
   389 apply (frule_tac [2] respond_imp_responses)
   390 apply (frule_tac [2] respond_imp_not_used)
   391 apply (simp_all del: image_insert
   392                 add: analz_image_freshK_simps split_ifs shrK_in_analz_respond
   393                      resp_analz_image_freshK parts_insert2)
   394 txt{*Base case of respond*}
   395 apply blast
   396 txt{*Inductive step of respond*}
   397 apply (intro allI conjI impI, simp_all)
   398 txt{*by unicity, either @{term "B=Aa"} or @{term "B=A'"}, a contradiction
   399      if @{term "B \<in> bad"}*}   
   400 apply (blast dest: unique_session_keys respond_certificate)
   401 apply (blast dest!: respond_certificate)
   402 apply (blast dest!: resp_analz_insert)
   403 done
   404 
   405 
   406 lemma Spy_not_see_session_key:
   407      "[| Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts (spies evs);
   408          A \<notin> bad;  A' \<notin> bad;  evs \<in> recur |]
   409       ==> Key K \<notin> analz (spies evs)"
   410 apply (erule rev_mp)
   411 apply (erule recur.induct)
   412 apply (drule_tac [4] RA2_analz_spies,
   413        frule_tac [5] respond_imp_responses,
   414        drule_tac [6] RA4_analz_spies,
   415        simp_all add: split_ifs analz_insert_eq analz_insert_freshK)
   416 txt{*Fake*}
   417 apply spy_analz
   418 txt{*RA2*}
   419 apply blast 
   420 txt{*RA3 remains*}
   421 apply (simp add: parts_insert_spies)
   422 txt{*Now we split into two cases.  A single blast could do it, but it would take
   423   a CPU minute.*}
   424 apply (safe del: impCE)
   425 txt{*RA3, case 1: use lemma previously proved by induction*}
   426 apply (blast elim: rev_notE [OF _ respond_Spy_not_see_session_key])
   427 txt{*RA3, case 2: K is an old key*}
   428 apply (blast dest: resp_analz_insert dest: Key_in_parts_respond)
   429 txt{*RA4*}
   430 apply blast 
   431 done
   432 
   433 (**** Authenticity properties for Agents ****)
   434 
   435 text{*The response never contains Hashes*}
   436 lemma Hash_in_parts_respond:
   437      "[| Hash {|Key (shrK B), M|} \<in> parts (insert RB H);
   438          (PB,RB,K) \<in> respond evs |]
   439       ==> Hash {|Key (shrK B), M|} \<in> parts H"
   440 apply (erule rev_mp)
   441 apply (erule respond_imp_responses [THEN responses.induct], auto)
   442 done
   443 
   444 text{*Only RA1 or RA2 can have caused such a part of a message to appear.
   445   This result is of no use to B, who cannot verify the Hash.  Moreover,
   446   it can say nothing about how recent A's message is.  It might later be
   447   used to prove B's presence to A at the run's conclusion.*}
   448 lemma Hash_auth_sender [rule_format]:
   449      "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \<in> parts(spies evs);
   450          A \<notin> bad;  evs \<in> recur |]
   451       ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \<in> set evs"
   452 apply (unfold HPair_def)
   453 apply (erule rev_mp)
   454 apply (erule recur.induct,
   455        drule_tac [6] RA4_parts_spies,
   456        drule_tac [4] RA2_parts_spies,
   457        simp_all)
   458 txt{*Fake, RA3*}
   459 apply (blast dest: Hash_in_parts_respond)+
   460 done
   461 
   462 (** These two results subsume (for all agents) the guarantees proved
   463     separately for A and B in the Otway-Rees protocol.
   464 **)
   465 
   466 
   467 text{*Certificates can only originate with the Server.*}
   468 lemma Cert_imp_Server_msg:
   469      "[| Crypt (shrK A) Y \<in> parts (spies evs);
   470          A \<notin> bad;  evs \<in> recur |]
   471       ==> \<exists>C RC. Says Server C RC \<in> set evs  &
   472                    Crypt (shrK A) Y \<in> parts {RC}"
   473 apply (erule rev_mp, erule recur.induct, simp_all)
   474 txt{*Fake*}
   475 apply blast
   476 txt{*RA1*}
   477 apply blast
   478 txt{*RA2: it cannot be a new Nonce, contradiction.*}
   479 apply blast
   480 txt{*RA3.  Pity that the proof is so brittle: this step requires the rewriting,
   481        which however would break all other steps.*}
   482 apply (simp add: parts_insert_spies, blast)
   483 txt{*RA4*}
   484 apply blast
   485 done
   486 
   487 end