src/HOL/Auth/Recur.thy
author paulson
Sat Aug 17 14:55:08 2002 +0200 (2002-08-17)
changeset 13507 febb8e5d2a9d
parent 11655 923e4d0d36d5
child 13922 75ae4244a596
permissions -rw-r--r--
tidying of Isar scripts
     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 Inductive relation "recur" for the Recursive Authentication protocol.
     7 *)
     8 
     9 theory Recur = Shared:
    10 
    11 (*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: 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: 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: 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: 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: 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 (*Simplest case: Alice goes directly to the server*)
   120 lemma "\<exists>K NA. \<exists>evs \<in> recur.
   121    Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
   122                    END|}  \<in> set evs"
   123 apply (intro exI bexI)
   124 apply (rule_tac [2] recur.Nil [THEN recur.RA1, 
   125                                THEN recur.RA3 [OF _ _ respond.One]], possibility)
   126 done
   127 
   128 
   129 (*Case two: Alice, Bob and the server*)
   130 lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
   131         Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
   132                    END|}  \<in> set evs"
   133 apply (cut_tac Nonce_supply2 Key_supply2, clarify)
   134 apply (intro exI bexI)
   135 apply (rule_tac [2] 
   136           recur.Nil [THEN recur.RA1, 
   137                      THEN recur.RA2,
   138                      THEN recur.RA3 [OF _ _ respond.One [THEN respond.Cons]],
   139                      THEN recur.RA4])
   140 apply (tactic "basic_possibility_tac")
   141 apply (tactic
   142       "DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
   143 done
   144 
   145 (*Case three: Alice, Bob, Charlie and the server
   146   Rather slow (16 seconds) to run every time...
   147 lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
   148         Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
   149                    END|}  \<in> set evs"
   150 apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1", clarify)
   151 apply (intro exI bexI)
   152 apply (rule_tac [2] 
   153           recur.Nil [THEN recur.RA1, 
   154                      THEN recur.RA2, THEN recur.RA2,
   155                      THEN recur.RA3 
   156                           [OF _ _ respond.One 
   157                                   [THEN respond.Cons, THEN respond.Cons]],
   158                      THEN recur.RA4, THEN recur.RA4])
   159 apply (tactic "basic_possibility_tac")
   160 apply (tactic
   161       "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 ORELSE \
   162 \                   eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
   163 done
   164 *)
   165 
   166 (**** Inductive proofs about recur ****)
   167 
   168 lemma respond_imp_not_used: "(PA,RB,KAB) \<in> respond evs ==> Key KAB \<notin> used evs"
   169 by (erule respond.induct, simp_all)
   170 
   171 lemma Key_in_parts_respond [rule_format]:
   172    "[| Key K \<in> parts {RB};  (PB,RB,K') \<in> respond evs |] ==> Key K \<notin> used evs"
   173 apply (erule rev_mp, erule respond.induct)
   174 apply (auto dest: Key_not_used respond_imp_not_used)
   175 done
   176 
   177 (*Simple inductive reasoning about responses*)
   178 lemma respond_imp_responses:
   179      "(PA,RB,KAB) \<in> respond evs ==> RB \<in> responses evs"
   180 apply (erule respond.induct)
   181 apply (blast intro!: respond_imp_not_used responses.intros)+
   182 done
   183 
   184 
   185 (** For reasoning about the encrypted portion of messages **)
   186 
   187 lemmas RA2_analz_spies = Says_imp_spies [THEN analz.Inj]
   188 
   189 lemma RA4_analz_spies:
   190      "Says C' B {|Crypt K X, X', RA|} \<in> set evs ==> RA \<in> analz (spies evs)"
   191 by blast
   192 
   193 
   194 (*RA2_analz... and RA4_analz... let us treat those cases using the same
   195   argument as for the Fake case.  This is possible for most, but not all,
   196   proofs: Fake does not invent new nonces (as in RA2), and of course Fake
   197   messages originate from the Spy. *)
   198 
   199 lemmas RA2_parts_spies =  RA2_analz_spies [THEN analz_into_parts]
   200 lemmas RA4_parts_spies =  RA4_analz_spies [THEN analz_into_parts]
   201 
   202 
   203 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
   204     sends messages containing X! **)
   205 
   206 (** Spy never sees another agent's shared key! (unless it's bad at start) **)
   207 
   208 lemma Spy_see_shrK [simp]:
   209      "evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   210 apply (erule recur.induct, auto)
   211 (*RA3.  It's ugly to call auto twice, but it seems necessary.*)
   212 apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
   213 done
   214 
   215 lemma Spy_analz_shrK [simp]:
   216      "evs \<in> recur ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   217 by auto
   218 
   219 lemma Spy_see_shrK_D [dest!]:
   220      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> recur|] ==> A \<in> bad"
   221 by (blast dest: Spy_see_shrK)
   222 
   223 
   224 (*** Proofs involving analz ***)
   225 
   226 (** Session keys are not used to encrypt other session keys **)
   227 
   228 (*Version for "responses" relation.  Handles case RA3 in the theorem below.
   229   Note that it holds for *any* set H (not just "spies evs")
   230   satisfying the inductive hypothesis.*)
   231 lemma resp_analz_image_freshK_lemma:
   232      "[| RB \<in> responses evs;
   233          \<forall>K KK. KK \<subseteq> - (range shrK) -->
   234                    (Key K \<in> analz (Key`KK Un H)) =
   235                    (K \<in> KK | Key K \<in> analz H) |]
   236      ==> \<forall>K KK. KK \<subseteq> - (range shrK) -->
   237                    (Key K \<in> analz (insert RB (Key`KK Un H))) =
   238                    (K \<in> KK | Key K \<in> analz (insert RB H))"
   239 by (erule responses.induct,
   240     simp_all del: image_insert
   241 	     add: analz_image_freshK_simps)
   242 
   243 
   244 (*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
   245 lemma raw_analz_image_freshK:
   246  "evs \<in> recur ==>
   247    \<forall>K KK. KK \<subseteq> - (range shrK) -->
   248           (Key K \<in> analz (Key`KK Un (spies evs))) =
   249           (K \<in> KK | Key K \<in> analz (spies evs))"
   250 apply (erule recur.induct)
   251 apply (drule_tac [4] RA2_analz_spies,
   252        drule_tac [5] respond_imp_responses,
   253        drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
   254 (*RA3*)
   255 apply (simp_all add: resp_analz_image_freshK_lemma)
   256 done
   257 
   258 
   259 (*Instance of the lemma with H replaced by (spies evs):
   260    [| RB \<in> responses evs;  evs \<in> recur; |]
   261    ==> KK \<subseteq> - (range shrK) -->
   262        Key K \<in> analz (insert RB (Key`KK Un spies evs)) =
   263        (K \<in> KK | Key K \<in> analz (insert RB (spies evs)))
   264 *)
   265 lemmas resp_analz_image_freshK =  
   266        resp_analz_image_freshK_lemma [OF _ raw_analz_image_freshK]
   267 
   268 lemma analz_insert_freshK:
   269      "[| evs \<in> recur;  KAB \<notin> range shrK |]
   270       ==> (Key K \<in> analz (insert (Key KAB) (spies evs))) =
   271           (K = KAB | Key K \<in> analz (spies evs))"
   272 by (simp del: image_insert
   273          add: analz_image_freshK_simps raw_analz_image_freshK)
   274 
   275 
   276 (*Everything that's hashed is already in past traffic. *)
   277 lemma Hash_imp_body:
   278      "[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
   279          evs \<in> recur;  A \<notin> bad |] ==> X \<in> parts (spies evs)"
   280 apply (erule rev_mp)
   281 apply (erule recur.induct,
   282        drule_tac [6] RA4_parts_spies,
   283        drule_tac [5] respond_imp_responses,
   284        drule_tac [4] RA2_parts_spies)
   285 (*RA3 requires a further induction*)
   286 apply (erule_tac [5] responses.induct, simp_all)
   287 (*Nil*)
   288 apply force
   289 (*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 (*Fake*)
   310 apply blast
   311 apply (erule_tac [3] responses.induct)
   312 (*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 by (erule responses.induct,
   326     simp_all del: image_insert
   327              add: analz_image_freshK_simps resp_analz_image_freshK)
   328 
   329 
   330 lemma resp_analz_insert_lemma:
   331      "[| Key K \<in> analz (insert RB H);
   332          \<forall>K KK. KK \<subseteq> - (range shrK) -->
   333                    (Key K \<in> analz (Key`KK Un H)) =
   334                    (K \<in> KK | Key K \<in> analz H);
   335          RB \<in> responses evs |]
   336      ==> (Key K \<in> parts{RB} | Key K \<in> analz H)"
   337 apply (erule rev_mp, erule responses.induct)
   338 apply (simp_all del: image_insert
   339              add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
   340 (*Simplification using two distinct treatments of "image"*)
   341 apply (simp add: parts_insert2, blast)
   342 done
   343 
   344 lemmas resp_analz_insert =
   345        resp_analz_insert_lemma [OF _ raw_analz_image_freshK]
   346 
   347 (*The last key returned by respond indeed appears in a certificate*)
   348 lemma respond_certificate:
   349      "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \<in> respond evs
   350       ==> Crypt (shrK A) {|Key K, B, NA|} \<in> parts {RA}"
   351 apply (ind_cases "(X, RA, K) \<in> respond evs")
   352 apply simp_all
   353 done
   354 
   355 (*This unicity proof differs from all the others in the HOL/Auth directory.
   356   The conclusion isn't quite unicity but duplicity, in that there are two
   357   possibilities.  Also, the presence of two different matching messages in
   358   the inductive step complicates the case analysis.  Unusually for such proofs,
   359   the quantifiers appear to be necessary.*)
   360 lemma unique_lemma [rule_format]:
   361      "(PB,RB,KXY) \<in> respond evs ==>
   362       \<forall>A B N. Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB} -->
   363       (\<forall>A' B' N'. Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB} -->
   364       (A'=A & B'=B) | (A'=B & B'=A))"
   365 apply (erule respond.induct)
   366 apply (simp_all add: all_conj_distrib)
   367 apply (blast dest: respond_certificate)
   368 done
   369 
   370 lemma unique_session_keys:
   371      "[| Crypt (shrK A) {|Key K, Agent B, N|} \<in> parts {RB};
   372          Crypt (shrK A') {|Key K, Agent B', N'|} \<in> parts {RB};
   373          (PB,RB,KXY) \<in> respond evs |]
   374       ==> (A'=A & B'=B) | (A'=B & B'=A)"
   375 by (rule unique_lemma, auto)
   376 
   377 
   378 (** Crucial secrecy property: Spy does not see the keys sent in msg RA3
   379     Does not in itself guarantee security: an attack could violate
   380     the premises, e.g. by having A=Spy **)
   381 
   382 lemma respond_Spy_not_see_session_key [rule_format]:
   383      "[| (PB,RB,KAB) \<in> respond evs;  evs \<in> recur |]
   384       ==> \<forall>A A' N. A \<notin> bad & A' \<notin> bad -->
   385           Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts{RB} -->
   386           Key K \<notin> analz (insert RB (spies evs))"
   387 apply (erule respond.induct)
   388 apply (frule_tac [2] respond_imp_responses)
   389 apply (frule_tac [2] respond_imp_not_used)
   390 apply (simp_all del: image_insert
   391                 add: analz_image_freshK_simps split_ifs shrK_in_analz_respond
   392                      resp_analz_image_freshK parts_insert2)
   393 apply (simp_all add: ex_disj_distrib)
   394 (** LEVEL 5 **)
   395 (*Base case of respond*)
   396 apply blast
   397 (*Inductive step of respond*)
   398 apply (intro allI conjI impI, simp_all)
   399 (*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*)
   400 apply (blast dest: unique_session_keys [OF _ 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 (*Base*)
   417 apply force
   418 (*Fake*)
   419 apply spy_analz
   420 (*RA2*)
   421 apply blast 
   422 (*RA3 remains*)
   423 apply (simp add: parts_insert_spies)
   424 (*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 (*RA3, case 1: use lemma previously proved by induction*)
   428 apply (blast elim: rev_notE [OF _ respond_Spy_not_see_session_key])
   429 (*RA3, case 2: K is an old key*)
   430 apply (blast dest: resp_analz_insert dest: Key_in_parts_respond)
   431 (*RA4*)
   432 apply blast 
   433 done
   434 
   435 (**** Authenticity properties for Agents ****)
   436 
   437 (*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 (*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 (*Nil*)
   461 apply force
   462 (*Fake, RA3*)
   463 apply (blast dest: Hash_in_parts_respond)+
   464 done
   465 
   466 (** These two results subsume (for all agents) the guarantees proved
   467     separately for A and B in the Otway-Rees protocol.
   468 **)
   469 
   470 
   471 (*Certificates can only originate with the Server.*)
   472 lemma Cert_imp_Server_msg:
   473      "[| Crypt (shrK A) Y \<in> parts (spies evs);
   474          A \<notin> bad;  evs \<in> recur |]
   475       ==> \<exists>C RC. Says Server C RC \<in> set evs  &
   476                    Crypt (shrK A) Y \<in> parts {RC}"
   477 apply (erule rev_mp, erule recur.induct, simp_all)
   478 (*Nil*)
   479 apply force
   480 (*Fake*)
   481 apply blast
   482 (*RA1*)
   483 apply blast
   484 (*RA2: it cannot be a new Nonce, contradiction.*)
   485 apply blast
   486 (*RA3*) (*Pity that the proof is so brittle: this step requires the rewriting,
   487           which however would break all other steps.*)
   488 apply (simp add: parts_insert_spies, blast)
   489 (*RA4*)
   490 apply blast
   491 done
   492 
   493 end