tidying
authorpaulson
Wed Apr 09 12:52:45 2003 +0200 (2003-04-09)
changeset 139072bc462b99e70
parent 13906 eefdd6b14508
child 13908 4bdfa9f77254
tidying
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/OtwayRees.thy	Wed Apr 09 12:51:49 2003 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.thy	Wed Apr 09 12:52:45 2003 +0200
     1.3 @@ -3,18 +3,17 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1996  University of Cambridge
     1.6  
     1.7 -Inductive relation "otway" for the Otway-Rees protocol
     1.8 -extended by Gets primitive.
     1.9 -
    1.10 -Version that encrypts Nonce NB
    1.11  
    1.12  From page 244 of
    1.13    Burrows, Abadi and Needham.  A Logic of Authentication.
    1.14    Proc. Royal Soc. 426 (1989)
    1.15  *)
    1.16  
    1.17 +header{*Verifying the Otway-Rees protocol*}
    1.18 +
    1.19  theory OtwayRees = Shared:
    1.20  
    1.21 +text{*This is the original version, which encrypts Nonce NB.*}
    1.22  
    1.23  consts  otway   :: "event list set"
    1.24  inductive "otway"
    1.25 @@ -89,7 +88,7 @@
    1.26  declare Fake_parts_insert_in_Un  [dest]
    1.27  
    1.28  
    1.29 -(*A "possibility property": there are traces that reach the end*)
    1.30 +text{*A "possibility property": there are traces that reach the end*}
    1.31  lemma "B \<noteq> Server
    1.32        ==> \<exists>K. \<exists>evs \<in> otway.
    1.33               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
    1.34 @@ -98,7 +97,8 @@
    1.35  apply (rule_tac [2] otway.Nil
    1.36                      [THEN otway.OR1, THEN otway.Reception,
    1.37                       THEN otway.OR2, THEN otway.Reception,
    1.38 -                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
    1.39 +                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], 
    1.40 +       possibility)
    1.41  done
    1.42  
    1.43  lemma Gets_imp_Says [dest!]:
    1.44 @@ -138,9 +138,9 @@
    1.45  (*Spy never sees a good agent's shared key!*)
    1.46  lemma Spy_see_shrK [simp]:
    1.47       "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
    1.48 -apply (erule otway.induct, force,
    1.49 -       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    1.50 -done
    1.51 +by (erule otway.induct, force,
    1.52 +    drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    1.53 +
    1.54  
    1.55  lemma Spy_analz_shrK [simp]:
    1.56       "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
    1.57 @@ -151,7 +151,7 @@
    1.58  by (blast dest: Spy_see_shrK)
    1.59  
    1.60  
    1.61 -(*** Proofs involving analz ***)
    1.62 +subsection{*Towards Secrecy: Proofs Involving @{term analz}*}
    1.63  
    1.64  (*Describes the form of K and NA when the Server sends this message.  Also
    1.65    for Oops case.*)
    1.66 @@ -159,8 +159,7 @@
    1.67       "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
    1.68           evs \<in> otway |]
    1.69        ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
    1.70 -apply (erule rev_mp, erule otway.induct, simp_all, blast)
    1.71 -done
    1.72 +by (erule rev_mp, erule otway.induct, simp_all, blast)
    1.73  
    1.74  
    1.75  (****
    1.76 @@ -173,7 +172,7 @@
    1.77  ****)
    1.78  
    1.79  
    1.80 -(** Session keys are not used to encrypt other session keys **)
    1.81 +text{*Session keys are not used to encrypt other session keys*}
    1.82  
    1.83  (*The equality makes the induction hypothesis easier to apply*)
    1.84  lemma analz_image_freshK [rule_format]:
    1.85 @@ -209,7 +208,7 @@
    1.86  done
    1.87  
    1.88  
    1.89 -(**** Authenticity properties relating to NA ****)
    1.90 +subsection{*Authenticity properties relating to NA*}
    1.91  
    1.92  (*Only OR1 can have caused such a part of a message to appear.*)
    1.93  lemma Crypt_imp_OR1 [rule_format]:
    1.94 @@ -232,8 +231,7 @@
    1.95  by (blast dest: Crypt_imp_OR1)
    1.96  
    1.97  
    1.98 -(** The Nonce NA uniquely identifies A's message. **)
    1.99 -
   1.100 +text{*The Nonce NA uniquely identifies A's message*}
   1.101  lemma unique_NA:
   1.102       "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
   1.103           Crypt (shrK A) {|NA, Agent A, Agent C|} \<in> parts (knows Spy evs);
   1.104 @@ -316,7 +314,7 @@
   1.105  apply (blast dest: unique_session_keys)+
   1.106  done
   1.107  
   1.108 -lemma Spy_not_see_encrypted_key:
   1.109 +theorem Spy_not_see_encrypted_key:
   1.110       "[| Says Server B
   1.111            {|NA, Crypt (shrK A) {|NA, Key K|},
   1.112                  Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
   1.113 @@ -325,6 +323,22 @@
   1.114        ==> Key K \<notin> analz (knows Spy evs)"
   1.115  by (blast dest: Says_Server_message_form secrecy_lemma)
   1.116  
   1.117 +text{*This form is an immediate consequence of the previous result.  It is 
   1.118 +similar to the assertions established by other methods.  It is equivalent
   1.119 +to the previous result in that the Spy already has @{term analz} and
   1.120 +@{term synth} at his disposal.  However, the conclusion 
   1.121 +@{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases
   1.122 +other than Fake are trivial, while Fake requires 
   1.123 +@{term "Key K \<notin> analz (knows Spy evs)"}. *}
   1.124 +lemma Spy_not_know_encrypted_key:
   1.125 +     "[| Says Server B
   1.126 +          {|NA, Crypt (shrK A) {|NA, Key K|},
   1.127 +                Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
   1.128 +         Notes Spy {|NA, NB, Key K|} \<notin> set evs;
   1.129 +         A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
   1.130 +      ==> Key K \<notin> knows Spy evs"
   1.131 +by (blast dest: Spy_not_see_encrypted_key)
   1.132 +
   1.133  
   1.134  (*A's guarantee.  The Oops premise quantifies over NB because A cannot know
   1.135    what it is.*)
   1.136 @@ -339,7 +353,7 @@
   1.137  
   1.138  
   1.139  
   1.140 -(**** Authenticity properties relating to NB ****)
   1.141 +subsection{*Authenticity properties relating to NB*}
   1.142  
   1.143  (*Only OR2 can have caused such a part of a message to appear.  We do not
   1.144    know anything about X: it does NOT have to have the right form.*)
   1.145 @@ -356,8 +370,7 @@
   1.146  done
   1.147  
   1.148  
   1.149 -(** The Nonce NB uniquely identifies B's  message. **)
   1.150 -
   1.151 +text{*The Nonce NB uniquely identifies B's  message*}
   1.152  lemma unique_NB:
   1.153       "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts(knows Spy evs);
   1.154           Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \<in> parts(knows Spy evs);
   1.155 @@ -396,9 +409,9 @@
   1.156  done
   1.157  
   1.158  
   1.159 -(*Guarantee for B: if it gets a message with matching NB then the Server
   1.160 -  has sent the correct message.*)
   1.161 -lemma B_trusts_OR3:
   1.162 +text{*Guarantee for B: if it gets a message with matching NB then the Server
   1.163 +  has sent the correct message.*}
   1.164 +theorem B_trusts_OR3:
   1.165       "[| Says B Server {|NA, Agent A, Agent B, X',
   1.166                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
   1.167             \<in> set evs;
   1.168 @@ -438,10 +451,10 @@
   1.169  done
   1.170  
   1.171  
   1.172 -(*After getting and checking OR4, agent A can trust that B has been active.
   1.173 +text{*After getting and checking OR4, agent A can trust that B has been active.
   1.174    We could probably prove that X has the expected form, but that is not
   1.175 -  strictly necessary for authentication.*)
   1.176 -lemma A_auths_B:
   1.177 +  strictly necessary for authentication.*}
   1.178 +theorem A_auths_B:
   1.179       "[| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs;
   1.180           Says A  B {|NA, Agent A, Agent B,
   1.181                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
     2.1 --- a/src/HOL/Auth/Shared.thy	Wed Apr 09 12:51:49 2003 +0200
     2.2 +++ b/src/HOL/Auth/Shared.thy	Wed Apr 09 12:52:45 2003 +0200
     2.3 @@ -46,7 +46,7 @@
     2.4  method_setup analz_freshK = {*
     2.5      Method.no_args
     2.6       (Method.METHOD
     2.7 -      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, impI]),
     2.8 +      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
     2.9                            REPEAT_FIRST (rtac analz_image_freshK_lemma),
    2.10                            ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
    2.11      "for proving the Session Key Compromise theorem"
     3.1 --- a/src/HOL/Auth/Yahalom2.thy	Wed Apr 09 12:51:49 2003 +0200
     3.2 +++ b/src/HOL/Auth/Yahalom2.thy	Wed Apr 09 12:52:45 2003 +0200
     3.3 @@ -3,8 +3,6 @@
     3.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.5      Copyright   1996  University of Cambridge
     3.6  
     3.7 -Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
     3.8 -
     3.9  This version trades encryption of NB for additional explicitness in YM3.
    3.10  Also in YM3, care is taken to make the two certificates distinct.
    3.11  
    3.12 @@ -13,6 +11,8 @@
    3.13    Proc. Royal Soc. 426 (1989)
    3.14  *)
    3.15  
    3.16 +header{*Inductive Analysis of the Yahalom protocol, Variant 2*}
    3.17 +
    3.18  theory Yahalom2 = Shared:
    3.19  
    3.20  consts  yahalom   :: "event list set"
    3.21 @@ -79,7 +79,7 @@
    3.22  declare Fake_parts_insert_in_Un  [dest]
    3.23  declare analz_into_parts [dest]
    3.24  
    3.25 -(*A "possibility property": there are traces that reach the end*)
    3.26 +text{*A "possibility property": there are traces that reach the end*}
    3.27  lemma "\<exists>X NB K. \<exists>evs \<in> yahalom.
    3.28               Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
    3.29  apply (intro exI bexI)
    3.30 @@ -94,7 +94,7 @@
    3.31       "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
    3.32  by (erule rev_mp, erule yahalom.induct, auto)
    3.33  
    3.34 -(*Must be proved separately for each protocol*)
    3.35 +text{*Must be proved separately for each protocol*}
    3.36  lemma Gets_imp_knows_Spy:
    3.37       "[| Gets B X \<in> set evs; evs \<in> yahalom |]  ==> X \<in> knows Spy evs"
    3.38  by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
    3.39 @@ -102,11 +102,10 @@
    3.40  declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
    3.41  
    3.42  
    3.43 -(**** Inductive proofs about yahalom ****)
    3.44 +subsection{*Inductive Proofs*}
    3.45  
    3.46 -(** For reasoning about the encrypted portion of messages **)
    3.47 -
    3.48 -(*Lets us treat YM4 using a similar argument as for the Fake case.*)
    3.49 +text{*Result for reasoning about the encrypted portion of messages.
    3.50 +Lets us treat YM4 using a similar argument as for the Fake case.*}
    3.51  lemma YM4_analz_knows_Spy:
    3.52       "[| Gets A {|NB, Crypt (shrK A) Y, X|} \<in> set evs;  evs \<in> yahalom |]
    3.53        ==> X \<in> analz (knows Spy evs)"
    3.54 @@ -119,12 +118,11 @@
    3.55  (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
    3.56      sends messages containing X! **)
    3.57  
    3.58 -(*Spy never sees a good agent's shared key!*)
    3.59 +text{*Spy never sees a good agent's shared key!*}
    3.60  lemma Spy_see_shrK [simp]:
    3.61       "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
    3.62 -apply (erule yahalom.induct, force,
    3.63 -       drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
    3.64 -done
    3.65 +by (erule yahalom.induct, force,
    3.66 +    drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
    3.67  
    3.68  lemma Spy_analz_shrK [simp]:
    3.69       "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
    3.70 @@ -180,8 +178,7 @@
    3.71  by (simp only: analz_image_freshK analz_image_freshK_simps)
    3.72  
    3.73  
    3.74 -(*** The Key K uniquely identifies the Server's  message. **)
    3.75 -
    3.76 +text{*The Key K uniquely identifies the Server's  message*}
    3.77  lemma unique_session_keys:
    3.78       "[| Says Server A
    3.79            {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \<in> set evs;
    3.80 @@ -191,12 +188,12 @@
    3.81       ==> A=A' & B=B' & na=na' & nb=nb'"
    3.82  apply (erule rev_mp, erule rev_mp)
    3.83  apply (erule yahalom.induct, simp_all)
    3.84 -(*YM3, by freshness*)
    3.85 +txt{*YM3, by freshness*}
    3.86  apply blast
    3.87  done
    3.88  
    3.89  
    3.90 -(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
    3.91 +subsection{*Crucial Secrecy Property: Spy Does Not See Key @{term KAB}*}
    3.92  
    3.93  lemma secrecy_lemma:
    3.94       "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
    3.95 @@ -208,7 +205,7 @@
    3.96            Key K \<notin> analz (knows Spy evs)"
    3.97  apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
    3.98         drule_tac [6] YM4_analz_knows_Spy)
    3.99 -apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
   3.100 +apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)
   3.101  apply (blast dest: unique_session_keys)+  (*YM3, Oops*)
   3.102  done
   3.103  
   3.104 @@ -225,7 +222,26 @@
   3.105  by (blast dest: secrecy_lemma Says_Server_message_form)
   3.106  
   3.107  
   3.108 -(** Security Guarantee for A upon receiving YM3 **)
   3.109 +
   3.110 +text{*This form is an immediate consequence of the previous result.  It is 
   3.111 +similar to the assertions established by other methods.  It is equivalent
   3.112 +to the previous result in that the Spy already has @{term analz} and
   3.113 +@{term synth} at his disposal.  However, the conclusion 
   3.114 +@{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases
   3.115 +other than Fake are trivial, while Fake requires 
   3.116 +@{term "Key K \<notin> analz (knows Spy evs)"}. *}
   3.117 +lemma Spy_not_know_encrypted_key:
   3.118 +     "[| Says Server A
   3.119 +            {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
   3.120 +                  Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
   3.121 +         \<in> set evs;
   3.122 +         Notes Spy {|na, nb, Key K|} \<notin> set evs;
   3.123 +         A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   3.124 +      ==> Key K \<notin> knows Spy evs"
   3.125 +by (blast dest: Spy_not_see_encrypted_key)
   3.126 +
   3.127 +
   3.128 +subsection{*Security Guarantee for A upon receiving YM3*}
   3.129  
   3.130  (*If the encrypted message appears then it originated with the Server.
   3.131    May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
   3.132 @@ -239,12 +255,12 @@
   3.133  apply (erule rev_mp)
   3.134  apply (erule yahalom.induct, force,
   3.135         frule_tac [6] YM4_parts_knows_Spy, simp_all)
   3.136 -(*Fake, YM3*)
   3.137 +txt{*Fake, YM3*}
   3.138  apply blast+
   3.139  done
   3.140  
   3.141  (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
   3.142 -lemma A_gets_good_key:
   3.143 +theorem A_gets_good_key:
   3.144       "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
   3.145           \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs;
   3.146           A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   3.147 @@ -252,7 +268,7 @@
   3.148  by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
   3.149  
   3.150  
   3.151 -(** Security Guarantee for B upon receiving YM4 **)
   3.152 +subsection{*Security Guarantee for B upon receiving YM4*}
   3.153  
   3.154  (*B knows, by the first part of A's message, that the Server distributed
   3.155    the key for A and B, and has associated it with NB.*)
   3.156 @@ -291,7 +307,7 @@
   3.157  
   3.158  
   3.159  (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
   3.160 -lemma B_gets_good_key:
   3.161 +theorem B_gets_good_key:
   3.162       "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
   3.163             \<in> set evs;
   3.164           \<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs;
   3.165 @@ -300,7 +316,7 @@
   3.166  by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
   3.167  
   3.168  
   3.169 -(*** Authenticating B to A ***)
   3.170 +subsection{*Authenticating B to A*}
   3.171  
   3.172  (*The encryption in message YM2 tells us it cannot be faked.*)
   3.173  lemma B_Said_YM2:
   3.174 @@ -331,8 +347,8 @@
   3.175  apply (blast dest!: B_Said_YM2)+
   3.176  done
   3.177  
   3.178 -(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   3.179 -lemma YM3_auth_B_to_A:
   3.180 +text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*}
   3.181 +theorem YM3_auth_B_to_A:
   3.182       "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
   3.183             \<in> set evs;
   3.184           A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   3.185 @@ -342,8 +358,9 @@
   3.186  by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma)
   3.187  
   3.188  
   3.189 +subsection{*Authenticating A to B*}
   3.190  
   3.191 -(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   3.192 +text{*using the certificate @{term "Crypt K (Nonce NB)"}*}
   3.193  
   3.194  (*Assuming the session key is secure, if both certificates are present then
   3.195    A has said NB.  We can't be sure about the rest of A's message, but only
   3.196 @@ -381,10 +398,10 @@
   3.197  done
   3.198  
   3.199  
   3.200 -(*If B receives YM4 then A has used nonce NB (and therefore is alive).
   3.201 +text{*If B receives YM4 then A has used nonce NB (and therefore is alive).
   3.202    Moreover, A associates K with NB (thus is talking about the same run).
   3.203 -  Other premises guarantee secrecy of K.*)
   3.204 -lemma YM4_imp_A_Said_YM3 [rule_format]:
   3.205 +  Other premises guarantee secrecy of K.*}
   3.206 +theorem YM4_imp_A_Said_YM3 [rule_format]:
   3.207       "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},
   3.208                    Crypt K (Nonce NB)|} \<in> set evs;
   3.209           (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs);