src/HOL/Auth/Yahalom2.thy
changeset 14207 f20fbb141673
parent 14200 d8598e24f8fa
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Fri Sep 26 10:32:26 2003 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Sep 26 10:34:28 2003 +0200
     1.3 @@ -2,18 +2,22 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   1996  University of Cambridge
     1.7 +*)
     1.8  
     1.9 +header{*The Yahalom Protocol, Variant 2*}
    1.10 +
    1.11 +theory Yahalom2 = Public:
    1.12 +
    1.13 +text{*
    1.14  This version trades encryption of NB for additional explicitness in YM3.
    1.15  Also in YM3, care is taken to make the two certificates distinct.
    1.16  
    1.17  From page 259 of
    1.18 -  Burrows, Abadi and Needham.  A Logic of Authentication.
    1.19 -  Proc. Royal Soc. 426 (1989)
    1.20 -*)
    1.21 +  Burrows, Abadi and Needham (1989).  A Logic of Authentication.
    1.22 +  Proc. Royal Soc. 426
    1.23  
    1.24 -header{*The Yahalom Protocol, Variant 2*}
    1.25 -
    1.26 -theory Yahalom2 = Shared:
    1.27 +This theory has the prototypical example of a secrecy relation, KeyCryptNonce.
    1.28 +*}
    1.29  
    1.30  consts  yahalom   :: "event list set"
    1.31  inductive "yahalom"
    1.32 @@ -89,7 +93,7 @@
    1.33                       THEN yahalom.YM2, THEN yahalom.Reception,
    1.34                       THEN yahalom.YM3, THEN yahalom.Reception,
    1.35                       THEN yahalom.YM4])
    1.36 -apply (possibility, simp add: used_Cons) 
    1.37 +apply (possibility, simp add: used_Cons)
    1.38  done
    1.39  
    1.40  lemma Gets_imp_Says:
    1.41 @@ -134,20 +138,26 @@
    1.42       "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> yahalom|] ==> A \<in> bad"
    1.43  by (blast dest: Spy_see_shrK)
    1.44  
    1.45 -(*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
    1.46 -lemma new_keys_not_used [rule_format, simp]:
    1.47 - "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
    1.48 +text{*Nobody can have used non-existent keys!  
    1.49 +    Needed to apply @{text analz_insert_Key}*}
    1.50 +lemma new_keys_not_used [simp]:
    1.51 +    "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|]
    1.52 +     ==> K \<notin> keysFor (parts (spies evs))"
    1.53 +apply (erule rev_mp)
    1.54  apply (erule yahalom.induct, force,
    1.55         frule_tac [6] YM4_parts_knows_Spy, simp_all)
    1.56  txt{*Fake*}
    1.57  apply (force dest!: keysFor_parts_insert)
    1.58 -txt{*YM3, YM4*}
    1.59 -apply blast+
    1.60 +txt{*YM3*}
    1.61 +apply blast
    1.62 +txt{*YM4*}
    1.63 +apply auto
    1.64 +apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj])
    1.65  done
    1.66  
    1.67  
    1.68 -(*Describes the form of K when the Server sends this message.  Useful for
    1.69 -  Oops as well as main secrecy property.*)
    1.70 +text{*Describes the form of K when the Server sends this message.  Useful for
    1.71 +  Oops as well as main secrecy property.*}
    1.72  lemma Says_Server_message_form:
    1.73       "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|}
    1.74            \<in> set evs;  evs \<in> yahalom |]
    1.75 @@ -171,8 +181,9 @@
    1.76     \<forall>K KK. KK <= - (range shrK) -->
    1.77            (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
    1.78            (K \<in> KK | Key K \<in> analz (knows Spy evs))"
    1.79 -apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
    1.80 -       drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
    1.81 +apply (erule yahalom.induct)
    1.82 +apply (frule_tac [8] Says_Server_message_form)
    1.83 +apply (drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
    1.84  done
    1.85  
    1.86  lemma analz_insert_freshK:
    1.87 @@ -214,7 +225,7 @@
    1.88  done
    1.89  
    1.90  
    1.91 -(*Final version*)
    1.92 +text{*Final version*}
    1.93  lemma Spy_not_see_encrypted_key:
    1.94       "[| Says Server A
    1.95              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
    1.96 @@ -227,12 +238,12 @@
    1.97  
    1.98  
    1.99  
   1.100 -text{*This form is an immediate consequence of the previous result.  It is 
   1.101 +text{*This form is an immediate consequence of the previous result.  It is
   1.102  similar to the assertions established by other methods.  It is equivalent
   1.103  to the previous result in that the Spy already has @{term analz} and
   1.104 -@{term synth} at his disposal.  However, the conclusion 
   1.105 +@{term synth} at his disposal.  However, the conclusion
   1.106  @{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases
   1.107 -other than Fake are trivial, while Fake requires 
   1.108 +other than Fake are trivial, while Fake requires
   1.109  @{term "Key K \<notin> analz (knows Spy evs)"}. *}
   1.110  lemma Spy_not_know_encrypted_key:
   1.111       "[| Says Server A
   1.112 @@ -247,8 +258,8 @@
   1.113  
   1.114  subsection{*Security Guarantee for A upon receiving YM3*}
   1.115  
   1.116 -(*If the encrypted message appears then it originated with the Server.
   1.117 -  May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   1.118 +text{*If the encrypted message appears then it originated with the Server.
   1.119 +  May now apply @{text Spy_not_see_encrypted_key}, subject to its conditions.*}
   1.120  lemma A_trusts_YM3:
   1.121       "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   1.122           A \<notin> bad;  evs \<in> yahalom |]
   1.123 @@ -263,7 +274,8 @@
   1.124  apply blast+
   1.125  done
   1.126  
   1.127 -(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   1.128 +text{*The obvious combination of @{text A_trusts_YM3} with 
   1.129 +@{text Spy_not_see_encrypted_key}*}
   1.130  theorem A_gets_good_key:
   1.131       "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   1.132           \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs;
   1.133 @@ -274,8 +286,8 @@
   1.134  
   1.135  subsection{*Security Guarantee for B upon receiving YM4*}
   1.136  
   1.137 -(*B knows, by the first part of A's message, that the Server distributed
   1.138 -  the key for A and B, and has associated it with NB.*)
   1.139 +text{*B knows, by the first part of A's message, that the Server distributed
   1.140 +  the key for A and B, and has associated it with NB.*}
   1.141  lemma B_trusts_YM4_shrK:
   1.142       "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
   1.143             \<in> parts (knows Spy evs);
   1.144 @@ -288,16 +300,16 @@
   1.145  apply (erule rev_mp)
   1.146  apply (erule yahalom.induct, force,
   1.147         frule_tac [6] YM4_parts_knows_Spy, simp_all)
   1.148 -(*Fake, YM3*)
   1.149 +txt{*Fake, YM3*}
   1.150  apply blast+
   1.151  done
   1.152  
   1.153  
   1.154 -(*With this protocol variant, we don't need the 2nd part of YM4 at all:
   1.155 -  Nonce NB is available in the first part.*)
   1.156 +text{*With this protocol variant, we don't need the 2nd part of YM4 at all:
   1.157 +  Nonce NB is available in the first part.*}
   1.158  
   1.159 -(*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   1.160 -  because we do not have to show that NB is secret. *)
   1.161 +text{*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   1.162 +  because we do not have to show that NB is secret. *}
   1.163  lemma B_trusts_YM4:
   1.164       "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},  X|}
   1.165             \<in> set evs;
   1.166 @@ -310,7 +322,8 @@
   1.167  by (blast dest!: B_trusts_YM4_shrK)
   1.168  
   1.169  
   1.170 -(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   1.171 +text{*The obvious combination of @{text B_trusts_YM4} with 
   1.172 +@{text Spy_not_see_encrypted_key}*}
   1.173  theorem B_gets_good_key:
   1.174       "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
   1.175             \<in> set evs;
   1.176 @@ -322,7 +335,7 @@
   1.177  
   1.178  subsection{*Authenticating B to A*}
   1.179  
   1.180 -(*The encryption in message YM2 tells us it cannot be faked.*)
   1.181 +text{*The encryption in message YM2 tells us it cannot be faked.*}
   1.182  lemma B_Said_YM2:
   1.183       "[| Crypt (shrK B) {|Agent A, Nonce NA|} \<in> parts (knows Spy evs);
   1.184           B \<notin> bad;  evs \<in> yahalom |]
   1.185 @@ -332,12 +345,12 @@
   1.186  apply (erule rev_mp)
   1.187  apply (erule yahalom.induct, force,
   1.188         frule_tac [6] YM4_parts_knows_Spy, simp_all)
   1.189 -(*Fake, YM2*)
   1.190 +txt{*Fake, YM2*}
   1.191  apply blast+
   1.192  done
   1.193  
   1.194  
   1.195 -(*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
   1.196 +text{*If the server sends YM3 then B sent YM2, perhaps with a different NB*}
   1.197  lemma YM3_auth_B_to_A_lemma:
   1.198       "[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
   1.199             \<in> set evs;
   1.200 @@ -347,7 +360,7 @@
   1.201                         \<in> set evs"
   1.202  apply (erule rev_mp)
   1.203  apply (erule yahalom.induct, simp_all)
   1.204 -(*Fake, YM2, YM3*)
   1.205 +txt{*Fake, YM2, YM3*}
   1.206  apply (blast dest!: B_Said_YM2)+
   1.207  done
   1.208  
   1.209 @@ -366,13 +379,13 @@
   1.210  
   1.211  text{*using the certificate @{term "Crypt K (Nonce NB)"}*}
   1.212  
   1.213 -(*Assuming the session key is secure, if both certificates are present then
   1.214 +text{*Assuming the session key is secure, if both certificates are present then
   1.215    A has said NB.  We can't be sure about the rest of A's message, but only
   1.216 -  NB matters for freshness.  Note that  Key K \<notin> analz (knows Spy evs)  must be
   1.217 -  the FIRST antecedent of the induction formula.*)
   1.218 +  NB matters for freshness.  Note that @{term "Key K \<notin> analz (knows Spy evs)"}
   1.219 +  must be the FIRST antecedent of the induction formula.*}
   1.220  
   1.221 -(*This lemma allows a use of unique_session_keys in the next proof,
   1.222 -  which otherwise is extremely slow.*)
   1.223 +text{*This lemma allows a use of @{text unique_session_keys} in the next proof,
   1.224 +  which otherwise is extremely slow.*}
   1.225  lemma secure_unique_session_keys:
   1.226       "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> analz (spies evs);
   1.227           Crypt (shrK A') {|Agent B', Key K, na'|} \<in> analz (spies evs);
   1.228 @@ -384,6 +397,7 @@
   1.229  lemma Auth_A_to_B_lemma [rule_format]:
   1.230       "evs \<in> yahalom
   1.231        ==> Key K \<notin> analz (knows Spy evs) -->
   1.232 +          K \<in> symKeys -->
   1.233            Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
   1.234            Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
   1.235              \<in> parts (knows Spy evs) -->
   1.236 @@ -392,13 +406,14 @@
   1.237  apply (erule yahalom.induct, force,
   1.238         frule_tac [6] YM4_parts_knows_Spy)
   1.239  apply (analz_mono_contra, simp_all)
   1.240 -(*Fake*)
   1.241 +txt{*Fake*}
   1.242  apply blast
   1.243 -(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   1.244 +txt{*YM3: by @{text new_keys_not_used}, the message
   1.245 +   @{term "Crypt K (Nonce NB)"} could not exist*}
   1.246  apply (force dest!: Crypt_imp_keysFor)
   1.247 -(*YM4: was Crypt K (Nonce NB) the very last message?  If so, apply unicity
   1.248 -  of session keys; if not, use ind. hyp.*)
   1.249 -apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys )
   1.250 +txt{*YM4: was   @{term "Crypt K (Nonce NB)"} the very last message?  If so, 
   1.251 +    apply unicity of session keys; if not, use the induction hypothesis*}
   1.252 +apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys)
   1.253  done
   1.254  
   1.255  
   1.256 @@ -409,7 +424,7 @@
   1.257       "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},
   1.258                    Crypt K (Nonce NB)|} \<in> set evs;
   1.259           (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs);
   1.260 -         A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   1.261 +         K \<in> symKeys;  A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   1.262        ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   1.263  by (blast intro: Auth_A_to_B_lemma
   1.264            dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK)