src/HOL/Auth/Yahalom2.thy
changeset 13907 2bc462b99e70
parent 13507 febb8e5d2a9d
child 13926 6e62e5357a10
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Wed Apr 09 12:51:49 2003 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Wed Apr 09 12:52:45 2003 +0200
     1.3 @@ -3,8 +3,6 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1996  University of Cambridge
     1.6  
     1.7 -Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
     1.8 -
     1.9  This version trades encryption of NB for additional explicitness in YM3.
    1.10  Also in YM3, care is taken to make the two certificates distinct.
    1.11  
    1.12 @@ -13,6 +11,8 @@
    1.13    Proc. Royal Soc. 426 (1989)
    1.14  *)
    1.15  
    1.16 +header{*Inductive Analysis of the Yahalom protocol, Variant 2*}
    1.17 +
    1.18  theory Yahalom2 = Shared:
    1.19  
    1.20  consts  yahalom   :: "event list set"
    1.21 @@ -79,7 +79,7 @@
    1.22  declare Fake_parts_insert_in_Un  [dest]
    1.23  declare analz_into_parts [dest]
    1.24  
    1.25 -(*A "possibility property": there are traces that reach the end*)
    1.26 +text{*A "possibility property": there are traces that reach the end*}
    1.27  lemma "\<exists>X NB K. \<exists>evs \<in> yahalom.
    1.28               Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
    1.29  apply (intro exI bexI)
    1.30 @@ -94,7 +94,7 @@
    1.31       "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
    1.32  by (erule rev_mp, erule yahalom.induct, auto)
    1.33  
    1.34 -(*Must be proved separately for each protocol*)
    1.35 +text{*Must be proved separately for each protocol*}
    1.36  lemma Gets_imp_knows_Spy:
    1.37       "[| Gets B X \<in> set evs; evs \<in> yahalom |]  ==> X \<in> knows Spy evs"
    1.38  by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
    1.39 @@ -102,11 +102,10 @@
    1.40  declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
    1.41  
    1.42  
    1.43 -(**** Inductive proofs about yahalom ****)
    1.44 +subsection{*Inductive Proofs*}
    1.45  
    1.46 -(** For reasoning about the encrypted portion of messages **)
    1.47 -
    1.48 -(*Lets us treat YM4 using a similar argument as for the Fake case.*)
    1.49 +text{*Result for reasoning about the encrypted portion of messages.
    1.50 +Lets us treat YM4 using a similar argument as for the Fake case.*}
    1.51  lemma YM4_analz_knows_Spy:
    1.52       "[| Gets A {|NB, Crypt (shrK A) Y, X|} \<in> set evs;  evs \<in> yahalom |]
    1.53        ==> X \<in> analz (knows Spy evs)"
    1.54 @@ -119,12 +118,11 @@
    1.55  (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
    1.56      sends messages containing X! **)
    1.57  
    1.58 -(*Spy never sees a good agent's shared key!*)
    1.59 +text{*Spy never sees a good agent's shared key!*}
    1.60  lemma Spy_see_shrK [simp]:
    1.61       "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
    1.62 -apply (erule yahalom.induct, force,
    1.63 -       drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
    1.64 -done
    1.65 +by (erule yahalom.induct, force,
    1.66 +    drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
    1.67  
    1.68  lemma Spy_analz_shrK [simp]:
    1.69       "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
    1.70 @@ -180,8 +178,7 @@
    1.71  by (simp only: analz_image_freshK analz_image_freshK_simps)
    1.72  
    1.73  
    1.74 -(*** The Key K uniquely identifies the Server's  message. **)
    1.75 -
    1.76 +text{*The Key K uniquely identifies the Server's  message*}
    1.77  lemma unique_session_keys:
    1.78       "[| Says Server A
    1.79            {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \<in> set evs;
    1.80 @@ -191,12 +188,12 @@
    1.81       ==> A=A' & B=B' & na=na' & nb=nb'"
    1.82  apply (erule rev_mp, erule rev_mp)
    1.83  apply (erule yahalom.induct, simp_all)
    1.84 -(*YM3, by freshness*)
    1.85 +txt{*YM3, by freshness*}
    1.86  apply blast
    1.87  done
    1.88  
    1.89  
    1.90 -(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
    1.91 +subsection{*Crucial Secrecy Property: Spy Does Not See Key @{term KAB}*}
    1.92  
    1.93  lemma secrecy_lemma:
    1.94       "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
    1.95 @@ -208,7 +205,7 @@
    1.96            Key K \<notin> analz (knows Spy evs)"
    1.97  apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
    1.98         drule_tac [6] YM4_analz_knows_Spy)
    1.99 -apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
   1.100 +apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)
   1.101  apply (blast dest: unique_session_keys)+  (*YM3, Oops*)
   1.102  done
   1.103  
   1.104 @@ -225,7 +222,26 @@
   1.105  by (blast dest: secrecy_lemma Says_Server_message_form)
   1.106  
   1.107  
   1.108 -(** Security Guarantee for A upon receiving YM3 **)
   1.109 +
   1.110 +text{*This form is an immediate consequence of the previous result.  It is 
   1.111 +similar to the assertions established by other methods.  It is equivalent
   1.112 +to the previous result in that the Spy already has @{term analz} and
   1.113 +@{term synth} at his disposal.  However, the conclusion 
   1.114 +@{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases
   1.115 +other than Fake are trivial, while Fake requires 
   1.116 +@{term "Key K \<notin> analz (knows Spy evs)"}. *}
   1.117 +lemma Spy_not_know_encrypted_key:
   1.118 +     "[| Says Server A
   1.119 +            {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   1.120 +                  Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   1.121 +         \<in> set evs;
   1.122 +         Notes Spy {|na, nb, Key K|} \<notin> set evs;
   1.123 +         A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   1.124 +      ==> Key K \<notin> knows Spy evs"
   1.125 +by (blast dest: Spy_not_see_encrypted_key)
   1.126 +
   1.127 +
   1.128 +subsection{*Security Guarantee for A upon receiving YM3*}
   1.129  
   1.130  (*If the encrypted message appears then it originated with the Server.
   1.131    May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   1.132 @@ -239,12 +255,12 @@
   1.133  apply (erule rev_mp)
   1.134  apply (erule yahalom.induct, force,
   1.135         frule_tac [6] YM4_parts_knows_Spy, simp_all)
   1.136 -(*Fake, YM3*)
   1.137 +txt{*Fake, YM3*}
   1.138  apply blast+
   1.139  done
   1.140  
   1.141  (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   1.142 -lemma A_gets_good_key:
   1.143 +theorem A_gets_good_key:
   1.144       "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   1.145           \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs;
   1.146           A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   1.147 @@ -252,7 +268,7 @@
   1.148  by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
   1.149  
   1.150  
   1.151 -(** Security Guarantee for B upon receiving YM4 **)
   1.152 +subsection{*Security Guarantee for B upon receiving YM4*}
   1.153  
   1.154  (*B knows, by the first part of A's message, that the Server distributed
   1.155    the key for A and B, and has associated it with NB.*)
   1.156 @@ -291,7 +307,7 @@
   1.157  
   1.158  
   1.159  (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   1.160 -lemma B_gets_good_key:
   1.161 +theorem B_gets_good_key:
   1.162       "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
   1.163             \<in> set evs;
   1.164           \<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs;
   1.165 @@ -300,7 +316,7 @@
   1.166  by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
   1.167  
   1.168  
   1.169 -(*** Authenticating B to A ***)
   1.170 +subsection{*Authenticating B to A*}
   1.171  
   1.172  (*The encryption in message YM2 tells us it cannot be faked.*)
   1.173  lemma B_Said_YM2:
   1.174 @@ -331,8 +347,8 @@
   1.175  apply (blast dest!: B_Said_YM2)+
   1.176  done
   1.177  
   1.178 -(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   1.179 -lemma YM3_auth_B_to_A:
   1.180 +text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*}
   1.181 +theorem YM3_auth_B_to_A:
   1.182       "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
   1.183             \<in> set evs;
   1.184           A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   1.185 @@ -342,8 +358,9 @@
   1.186  by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma)
   1.187  
   1.188  
   1.189 +subsection{*Authenticating A to B*}
   1.190  
   1.191 -(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   1.192 +text{*using the certificate @{term "Crypt K (Nonce NB)"}*}
   1.193  
   1.194  (*Assuming the session key is secure, if both certificates are present then
   1.195    A has said NB.  We can't be sure about the rest of A's message, but only
   1.196 @@ -381,10 +398,10 @@
   1.197  done
   1.198  
   1.199  
   1.200 -(*If B receives YM4 then A has used nonce NB (and therefore is alive).
   1.201 +text{*If B receives YM4 then A has used nonce NB (and therefore is alive).
   1.202    Moreover, A associates K with NB (thus is talking about the same run).
   1.203 -  Other premises guarantee secrecy of K.*)
   1.204 -lemma YM4_imp_A_Said_YM3 [rule_format]:
   1.205 +  Other premises guarantee secrecy of K.*}
   1.206 +theorem YM4_imp_A_Said_YM3 [rule_format]:
   1.207       "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},
   1.208                    Crypt K (Nonce NB)|} \<in> set evs;
   1.209           (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs);