src/HOL/Auth/WooLam.thy
changeset 14207 f20fbb141673
parent 13507 febb8e5d2a9d
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Auth/WooLam.thy	Fri Sep 26 10:32:26 2003 +0200
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Fri Sep 26 10:34:28 2003 +0200
     1.3 @@ -2,19 +2,21 @@
     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 -Inductive relation "woolam" for the Woo-Lam protocol.
     1.9 -
    1.10 -Simplified version from page 11 of
    1.11 -  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
    1.12 -  IEEE Trans. S.E. 22(1), 1996, pages 6-15.
    1.13 -
    1.14 -Note: this differs from the Woo-Lam protocol discussed by Lowe in his paper
    1.15 -  Some New Attacks upon Security Protocols.
    1.16 -  Computer Security Foundations Workshop, 1996.
    1.17  *)
    1.18  
    1.19 -theory WooLam = Shared:
    1.20 +header{*The Woo-Lam Protocol*}
    1.21 +
    1.22 +theory WooLam = Public:
    1.23 +
    1.24 +text{*Simplified version from page 11 of
    1.25 +  Abadi and Needham (1996). 
    1.26 +  Prudent Engineering Practice for Cryptographic Protocols.
    1.27 +  IEEE Trans. S.E. 22(1), pages 6-15.
    1.28 +
    1.29 +Note: this differs from the Woo-Lam protocol discussed by Lowe (1996):
    1.30 +  Some New Attacks upon Security Protocols.
    1.31 +  Computer Security Foundations Workshop
    1.32 +*}
    1.33  
    1.34  consts  woolam  :: "event list set"
    1.35  inductive woolam
    1.36 @@ -87,8 +89,7 @@
    1.37  (*Spy never sees a good agent's shared key!*)
    1.38  lemma Spy_see_shrK [simp]:
    1.39       "evs \<in> woolam ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
    1.40 -apply (erule woolam.induct, force, simp_all, blast+)
    1.41 -done
    1.42 +by (erule woolam.induct, force, simp_all, blast+)
    1.43  
    1.44  lemma Spy_analz_shrK [simp]:
    1.45       "evs \<in> woolam ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
    1.46 @@ -108,8 +109,7 @@
    1.47       "[| Crypt (shrK A) (Nonce NB) \<in> parts (spies evs);
    1.48           A \<notin> bad;  evs \<in> woolam |]
    1.49        ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
    1.50 -apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.51 -done
    1.52 +by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.53  
    1.54  (*Guarantee for Server: if it gets a message containing a certificate from
    1.55    Alice, then she originated that certificate.  But we DO NOT know that B
    1.56 @@ -130,16 +130,14 @@
    1.57           evs \<in> woolam |]
    1.58        ==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
    1.59               \<in> set evs"
    1.60 -apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.61 -done
    1.62 +by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.63  
    1.64  (*If the encrypted message appears then it originated with the Server!*)
    1.65  lemma NB_Crypt_imp_Server_msg [rule_format]:
    1.66       "[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
    1.67           B \<notin> bad;  evs \<in> woolam |]
    1.68        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
    1.69 -apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.70 -done
    1.71 +by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.72  
    1.73  (*Guarantee for B.  If B gets the Server's certificate then A has encrypted
    1.74    the nonce using her key.  This event can be no older than the nonce itself.
    1.75 @@ -156,8 +154,7 @@
    1.76  lemma B_said_WL2:
    1.77       "[| Says B A (Nonce NB) \<in> set evs;  B \<noteq> Spy;  evs \<in> woolam |]
    1.78        ==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
    1.79 -apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.80 -done
    1.81 +by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.82  
    1.83  
    1.84  (**CANNOT be proved because A doesn't know where challenges come from...*)