src/HOL/Auth/Kerberos_BAN.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/Kerberos_BAN
     2     ID:         $Id$
     3     Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Tidied and converted to Isar by lcp.
     7 *)
     8 
     9 header{*The Kerberos Protocol, BAN Version*}
    10 
    11 theory Kerberos_BAN = Public:
    12 
    13 text{*From page 251 of
    14   Burrows, Abadi and Needham (1989).  A Logic of Authentication.
    15   Proc. Royal Soc. 426
    16 
    17   Confidentiality (secrecy) and authentication properties rely on
    18   temporal checks: strong guarantees in a little abstracted - but
    19   very realistic - model.
    20 *}
    21 
    22 (* Temporal modelization: session keys can be leaked
    23                           ONLY when they have expired *)
    24 
    25 syntax
    26     CT :: "event list=>nat"
    27     Expired :: "[nat, event list] => bool"
    28     RecentAuth :: "[nat, event list] => bool"
    29 
    30 consts
    31 
    32     (*Duration of the session key*)
    33     SesKeyLife   :: nat
    34 
    35     (*Duration of the authenticator*)
    36     AutLife :: nat
    37 
    38 text{*The ticket should remain fresh for two journeys on the network at least*}
    39 specification (SesKeyLife)
    40   SesKeyLife_LB [iff]: "2 \<le> SesKeyLife"
    41     by blast
    42 
    43 text{*The authenticator only for one journey*}
    44 specification (AutLife)
    45   AutLife_LB [iff]:    "Suc 0 \<le> AutLife"
    46     by blast
    47 
    48 
    49 translations
    50    "CT" == "length "
    51 
    52    "Expired T evs" == "SesKeyLife + T < CT evs"
    53 
    54    "RecentAuth T evs" == "CT evs \<le> AutLife + T"
    55 
    56 consts  kerberos_ban   :: "event list set"
    57 inductive "kerberos_ban"
    58  intros
    59 
    60    Nil:  "[] \<in> kerberos_ban"
    61 
    62    Fake: "[| evsf \<in> kerberos_ban;  X \<in> synth (analz (spies evsf)) |]
    63 	  ==> Says Spy B X # evsf \<in> kerberos_ban"
    64 
    65 
    66    Kb1:  "[| evs1 \<in> kerberos_ban |]
    67 	  ==> Says A Server {|Agent A, Agent B|} # evs1
    68 		\<in>  kerberos_ban"
    69 
    70 
    71    Kb2:  "[| evs2 \<in> kerberos_ban;  Key KAB \<notin> used evs2;  KAB \<in> symKeys;
    72 	     Says A' Server {|Agent A, Agent B|} \<in> set evs2 |]
    73 	  ==> Says Server A
    74 		(Crypt (shrK A)
    75 		   {|Number (CT evs2), Agent B, Key KAB,
    76 		    (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|})
    77 		# evs2 \<in> kerberos_ban"
    78 
    79 
    80    Kb3:  "[| evs3 \<in> kerberos_ban;
    81 	     Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
    82 	       \<in> set evs3;
    83 	     Says A Server {|Agent A, Agent B|} \<in> set evs3;
    84 	     ~ Expired Ts evs3 |]
    85 	  ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |}
    86 	       # evs3 \<in> kerberos_ban"
    87 
    88 
    89    Kb4:  "[| evs4 \<in> kerberos_ban;
    90 	     Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}),
    91 			 (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
    92 	     ~ Expired Ts evs4;  RecentAuth Ta evs4 |]
    93 	  ==> Says B A (Crypt K (Number Ta)) # evs4
    94 		\<in> kerberos_ban"
    95 
    96 	(*Old session keys may become compromised*)
    97    Oops: "[| evso \<in> kerberos_ban;
    98 	     Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
    99 	       \<in> set evso;
   100 	     Expired Ts evso |]
   101 	  ==> Notes Spy {|Number Ts, Key K|} # evso \<in> kerberos_ban"
   102 
   103 
   104 declare Says_imp_knows_Spy [THEN parts.Inj, dest]
   105 declare parts.Body [dest]
   106 declare analz_into_parts [dest]
   107 declare Fake_parts_insert_in_Un [dest]
   108 
   109 text{*A "possibility property": there are traces that reach the end.*}
   110 lemma "[|Key K \<notin> used []; K \<in> symKeys|]
   111        ==> \<exists>Timestamp. \<exists>evs \<in> kerberos_ban.
   112              Says B A (Crypt K (Number Timestamp))
   113                   \<in> set evs"
   114 apply (cut_tac SesKeyLife_LB)
   115 apply (intro exI bexI)
   116 apply (rule_tac [2]
   117            kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2,
   118                              THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4])
   119 apply (possibility, simp_all (no_asm_simp) add: used_Cons)
   120 done
   121 
   122 
   123 (**** Inductive proofs about kerberos_ban ****)
   124 
   125 text{*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*}
   126 lemma Kb3_msg_in_parts_spies:
   127      "Says S A (Crypt KA {|Timestamp, B, K, X|}) \<in> set evs
   128       ==> X \<in> parts (spies evs)"
   129 by blast
   130 
   131 lemma Oops_parts_spies:
   132      "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \<in> set evs
   133       ==> K \<in> parts (spies evs)"
   134 by blast
   135 
   136 
   137 text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
   138 lemma Spy_see_shrK [simp]:
   139      "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   140 apply (erule kerberos_ban.induct)
   141 apply (frule_tac [7] Oops_parts_spies)
   142 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast+)
   143 done
   144 
   145 
   146 lemma Spy_analz_shrK [simp]:
   147      "evs \<in> kerberos_ban ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   148 by auto
   149 
   150 lemma Spy_see_shrK_D [dest!]:
   151      "[| Key (shrK A) \<in> parts (spies evs);
   152                 evs \<in> kerberos_ban |] ==> A:bad"
   153 by (blast dest: Spy_see_shrK)
   154 
   155 lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D,  dest!]
   156 
   157 
   158 text{*Nobody can have used non-existent keys!*}
   159 lemma new_keys_not_used [simp]:
   160     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerberos_ban|]
   161      ==> K \<notin> keysFor (parts (spies evs))"
   162 apply (erule rev_mp)
   163 apply (erule kerberos_ban.induct)
   164 apply (frule_tac [7] Oops_parts_spies)
   165 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
   166 txt{*Fake*}
   167 apply (force dest!: keysFor_parts_insert)
   168 txt{*Kb2, Kb3, Kb4*}
   169 apply (force dest!: analz_shrK_Decrypt)+
   170 done
   171 
   172 subsection{* Lemmas concerning the form of items passed in messages *}
   173 
   174 text{*Describes the form of K, X and K' when the Server sends this message.*}
   175 lemma Says_Server_message_form:
   176      "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})
   177          \<in> set evs; evs \<in> kerberos_ban |]
   178       ==> K \<notin> range shrK &
   179           X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) &
   180           K' = shrK A"
   181 apply (erule rev_mp)
   182 apply (erule kerberos_ban.induct, auto)
   183 done
   184 
   185 
   186 text{*If the encrypted message appears then it originated with the Server
   187   PROVIDED that A is NOT compromised!
   188 
   189   This shows implicitly the FRESHNESS OF THE SESSION KEY to A
   190 *}
   191 lemma A_trusts_K_by_Kb2:
   192      "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}
   193            \<in> parts (spies evs);
   194          A \<notin> bad;  evs \<in> kerberos_ban |]
   195        ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
   196              \<in> set evs"
   197 apply (erule rev_mp)
   198 apply (erule kerberos_ban.induct)
   199 apply (frule_tac [7] Oops_parts_spies)
   200 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast)
   201 done
   202 
   203 
   204 text{*If the TICKET appears then it originated with the Server*}
   205 text{*FRESHNESS OF THE SESSION KEY to B*}
   206 lemma B_trusts_K_by_Kb3:
   207      "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \<in> parts (spies evs);
   208          B \<notin> bad;  evs \<in> kerberos_ban |]
   209        ==> Says Server A
   210             (Crypt (shrK A) {|Number Ts, Agent B, Key K,
   211                           Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})
   212            \<in> set evs"
   213 apply (erule rev_mp)
   214 apply (erule kerberos_ban.induct)
   215 apply (frule_tac [7] Oops_parts_spies)
   216 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast)
   217 done
   218 
   219 
   220 text{*EITHER describes the form of X when the following message is sent,
   221   OR     reduces it to the Fake case.
   222   Use @{text Says_Server_message_form} if applicable.*}
   223 lemma Says_S_message_form:
   224      "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
   225             \<in> set evs;
   226          evs \<in> kerberos_ban |]
   227  ==> (K \<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))
   228           | X \<in> analz (spies evs)"
   229 apply (case_tac "A \<in> bad")
   230 apply (force dest!: Says_imp_spies [THEN analz.Inj])
   231 apply (frule Says_imp_spies [THEN parts.Inj])
   232 apply (blast dest!: A_trusts_K_by_Kb2 Says_Server_message_form)
   233 done
   234 
   235 
   236 
   237 (****
   238  The following is to prove theorems of the form
   239 
   240   Key K \<in> analz (insert (Key KAB) (spies evs)) ==>
   241   Key K \<in> analz (spies evs)
   242 
   243  A more general formula must be proved inductively.
   244 
   245 ****)
   246 
   247 text{* Session keys are not used to encrypt other session keys *}
   248 lemma analz_image_freshK [rule_format (no_asm)]:
   249      "evs \<in> kerberos_ban ==>
   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 kerberos_ban.induct)
   254 apply (drule_tac [7] Says_Server_message_form)
   255 apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz, auto) 
   256 done
   257 
   258 
   259 lemma analz_insert_freshK:
   260      "[| evs \<in> kerberos_ban;  KAB \<notin> range shrK |] ==>
   261       (Key K \<in> analz (insert (Key KAB) (spies evs))) =
   262       (K = KAB | Key K \<in> analz (spies evs))"
   263 by (simp only: analz_image_freshK analz_image_freshK_simps)
   264 
   265 
   266 text{* The session key K uniquely identifies the message *}
   267 lemma unique_session_keys:
   268      "[| Says Server A
   269            (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \<in> set evs;
   270          Says Server A'
   271           (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \<in> set evs;
   272          evs \<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'"
   273 apply (erule rev_mp)
   274 apply (erule rev_mp)
   275 apply (erule kerberos_ban.induct)
   276 apply (frule_tac [7] Oops_parts_spies)
   277 apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
   278 txt{*Kb2: it can't be a new key*}
   279 apply blast
   280 done
   281 
   282 
   283 text{* Lemma: the session key sent in msg Kb2 would be EXPIRED
   284     if the spy could see it! *}
   285 
   286 lemma lemma2 [rule_format (no_asm)]:
   287      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban |]
   288   ==> Says Server A
   289           (Crypt (shrK A) {|Number Ts, Agent B, Key K,
   290                             Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})
   291          \<in> set evs -->
   292       Key K \<in> analz (spies evs) --> Expired Ts evs"
   293 apply (erule kerberos_ban.induct)
   294 apply (frule_tac [7] Says_Server_message_form)
   295 apply (frule_tac [5] Says_S_message_form [THEN disjE])
   296 apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes)
   297 txt{*Fake*}
   298 apply spy_analz
   299 txt{*Kb2*}
   300 apply (blast intro: parts_insertI less_SucI)
   301 txt{*Kb3*}
   302 apply (case_tac "Aa \<in> bad")
   303  prefer 2 apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys)
   304 apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI)
   305 txt{*Oops: PROOF FAILED if addIs below*}
   306 apply (blast dest: unique_session_keys intro!: less_SucI)
   307 done
   308 
   309 
   310 text{*Confidentiality for the Server: Spy does not see the keys sent in msg Kb2
   311 as long as they have not expired.*}
   312 lemma Confidentiality_S:
   313      "[| Says Server A
   314           (Crypt K' {|Number T, Agent B, Key K, X|}) \<in> set evs;
   315          ~ Expired T evs;
   316          A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban
   317       |] ==> Key K \<notin> analz (spies evs)"
   318 apply (frule Says_Server_message_form, assumption)
   319 apply (blast intro: lemma2)
   320 done
   321 
   322 (**** THE COUNTERPART OF CONFIDENTIALITY
   323       [|...; Expired Ts evs; ...|] ==> Key K \<in> analz (spies evs)
   324       WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove!   ****)
   325 
   326 
   327 text{*Confidentiality for Alice*}
   328 lemma Confidentiality_A:
   329      "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \<in> parts (spies evs);
   330          ~ Expired T evs;
   331          A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban
   332       |] ==> Key K \<notin> analz (spies evs)"
   333 by (blast dest!: A_trusts_K_by_Kb2 Confidentiality_S)
   334 
   335 
   336 text{*Confidentiality for Bob*}
   337 lemma Confidentiality_B:
   338      "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|}
   339           \<in> parts (spies evs);
   340         ~ Expired Tk evs;
   341         A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban
   342       |] ==> Key K \<notin> analz (spies evs)"
   343 by (blast dest!: B_trusts_K_by_Kb3 Confidentiality_S)
   344 
   345 
   346 lemma lemma_B [rule_format]:
   347      "[| B \<notin> bad;  evs \<in> kerberos_ban |]
   348       ==> Key K \<notin> analz (spies evs) -->
   349           Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
   350           \<in> set evs -->
   351           Crypt K (Number Ta) \<in> parts (spies evs) -->
   352           Says B A (Crypt K (Number Ta)) \<in> set evs"
   353 apply (erule kerberos_ban.induct)
   354 apply (frule_tac [7] Oops_parts_spies)
   355 apply (frule_tac [5] Says_S_message_form)
   356 apply (drule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra)
   357 apply (simp_all (no_asm_simp) add: all_conj_distrib)
   358 txt{*Fake*}
   359 apply blast
   360 txt{*Kb2*} 
   361 apply (force dest: Crypt_imp_invKey_keysFor)
   362 txt{*Kb4*}
   363 apply (blast dest: B_trusts_K_by_Kb3 unique_session_keys
   364                    Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad)
   365 done
   366 
   367 
   368 text{*Authentication of B to A*}
   369 lemma Authentication_B:
   370      "[| Crypt K (Number Ta) \<in> parts (spies evs);
   371          Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}
   372          \<in> parts (spies evs);
   373          ~ Expired Ts evs;
   374          A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban |]
   375       ==> Says B A (Crypt K (Number Ta)) \<in> set evs"
   376 by (blast dest!: A_trusts_K_by_Kb2
   377           intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE])
   378 
   379 lemma lemma_A [rule_format]:
   380      "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
   381       ==>
   382          Key K \<notin> analz (spies evs) -->
   383          Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
   384          \<in> set evs -->
   385           Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs) -->
   386          Says A B {|X, Crypt K {|Agent A, Number Ta|}|}
   387              \<in> set evs"
   388 apply (erule kerberos_ban.induct)
   389 apply (frule_tac [7] Oops_parts_spies)
   390 apply (frule_tac [5] Says_S_message_form)
   391 apply (frule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra)
   392 apply (simp_all (no_asm_simp) add: all_conj_distrib)
   393 txt{*Fake*}
   394 apply blast
   395 txt{*Kb2*}
   396 apply (force dest: Crypt_imp_invKey_keysFor)
   397 txt{*Kb3*}
   398 apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys)
   399 done
   400 
   401 text{*Authentication of A to B*}
   402 lemma Authentication_A:
   403      "[| Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs);
   404          Crypt (shrK B) {|Number Ts, Agent A, Key K|}
   405          \<in> parts (spies evs);
   406          ~ Expired Ts evs;
   407          A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos_ban |]
   408       ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|},
   409                      Crypt K {|Agent A, Number Ta|}|} \<in> set evs"
   410 by (blast dest!: B_trusts_K_by_Kb3
   411           intro!: lemma_A
   412           elim!: Confidentiality_S [THEN [2] rev_notE])
   413 
   414 end