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