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