Removal of the Key_supply axiom (affects many possbility proofs) and minor
authorpaulson
Tue Sep 23 15:41:33 2003 +0200 (2003-09-23)
changeset 14200d8598e24f8fa
parent 14199 d3b8d972a488
child 14201 7ad7ab89c402
Removal of the Key_supply axiom (affects many possbility proofs) and minor
changes
src/HOL/Auth/CertifiedEmail.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/KerberosIV.thy
src/HOL/Auth/Kerberos_BAN.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Recur.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.thy
src/HOL/Auth/Yahalom_Bad.thy
     1.1 --- a/src/HOL/Auth/CertifiedEmail.thy	Tue Sep 23 15:40:27 2003 +0200
     1.2 +++ b/src/HOL/Auth/CertifiedEmail.thy	Tue Sep 23 15:41:33 2003 +0200
     1.3 @@ -93,14 +93,15 @@
     1.4  declare analz_into_parts [dest]
     1.5  
     1.6  (*A "possibility property": there are traces that reach the end*)
     1.7 -lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
     1.8 +lemma "[| Key K \<notin> used []; K \<in> symKeys |] ==> 
     1.9 +       \<exists>S2TTP. \<exists>evs \<in> certified_mail.
    1.10             Says TTP S (Crypt (priSK TTP) S2TTP) \<in> set evs"
    1.11 -apply (rule bexE [OF Key_supply1]) 
    1.12  apply (intro exI bexI)
    1.13  apply (rule_tac [2] certified_mail.Nil
    1.14                      [THEN certified_mail.CM1, THEN certified_mail.Reception,
    1.15                       THEN certified_mail.CM2, 
    1.16 -                     THEN certified_mail.CM3], possibility, possibility, auto) 
    1.17 +                     THEN certified_mail.CM3]) 
    1.18 +apply (possibility, auto) 
    1.19  done
    1.20  
    1.21  
     2.1 --- a/src/HOL/Auth/Event.thy	Tue Sep 23 15:40:27 2003 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Tue Sep 23 15:41:33 2003 +0200
     2.3 @@ -35,13 +35,10 @@
     2.4  
     2.5  text{*Spy has access to his own key for spoof messages, but Server is secure*}
     2.6  specification (bad)
     2.7 -  bad_properties: "Spy \<in> bad & Server \<notin> bad"
     2.8 +  Spy_in_bad     [iff]: "Spy \<in> bad"
     2.9 +  Server_not_bad [iff]: "Server \<notin> bad"
    2.10      by (rule exI [of _ "{Spy}"], simp)
    2.11  
    2.12 -lemmas Spy_in_bad = bad_properties [THEN conjunct1, iff]
    2.13 -lemmas Server_not_bad = bad_properties [THEN conjunct2, iff]
    2.14 -
    2.15 -
    2.16  primrec
    2.17    knows_Nil:   "knows A [] = initState A"
    2.18    knows_Cons:
    2.19 @@ -111,8 +108,8 @@
    2.20       "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
    2.21  by simp
    2.22  
    2.23 -text{*The point of letting the Spy see "bad" agents' notes is to prevent
    2.24 -  redundant case-splits on whether A=Spy and whether A:bad*}
    2.25 +text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits
    2.26 +      on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*}
    2.27  lemma knows_Spy_Notes [simp]:
    2.28       "knows Spy (Notes A X # evs) =  
    2.29            (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
     3.1 --- a/src/HOL/Auth/KerberosIV.thy	Tue Sep 23 15:40:27 2003 +0200
     3.2 +++ b/src/HOL/Auth/KerberosIV.thy	Tue Sep 23 15:41:33 2003 +0200
     3.3 @@ -242,9 +242,10 @@
     3.4  
     3.5  (*---------------------------------------------------------------------*)
     3.6  
     3.7 -declare Says_imp_knows_Spy [THEN parts.Inj, dest] parts.Body [dest]
     3.8 -declare analz_subset_parts [THEN subsetD, dest]
     3.9 -declare Fake_parts_insert [THEN subsetD, dest]
    3.10 +declare Says_imp_knows_Spy [THEN parts.Inj, dest] 
    3.11 +declare parts.Body [dest]
    3.12 +declare analz_into_parts [dest]
    3.13 +declare Fake_parts_insert_in_Un [dest]
    3.14  
    3.15  
    3.16  subsection{*Lemmas about Lists*}
    3.17 @@ -294,31 +295,27 @@
    3.18     ev \<noteq> Says Kas A (Crypt (shrK A) {|akey, Agent Peer, Tk,       
    3.19                (Crypt (shrK Peer) {|Agent A, Agent Peer, akey, Tk|})|}))  
    3.20         ==> AuthKeys (ev # evs) = AuthKeys evs"
    3.21 -apply (unfold AuthKeys_def, auto)
    3.22 -done
    3.23 +by (unfold AuthKeys_def, auto)
    3.24  
    3.25  lemma AuthKeys_insert: 
    3.26    "AuthKeys  
    3.27       (Says Kas A (Crypt (shrK A) {|Key K, Agent Peer, Number Tk,  
    3.28        (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K, Number Tk|})|}) # evs)  
    3.29         = insert K (AuthKeys evs)"
    3.30 -apply (unfold AuthKeys_def, auto)
    3.31 -done
    3.32 +by (unfold AuthKeys_def, auto)
    3.33  
    3.34  lemma AuthKeys_simp: 
    3.35     "K \<in> AuthKeys  
    3.36      (Says Kas A (Crypt (shrK A) {|Key K', Agent Peer, Number Tk,  
    3.37       (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K', Number Tk|})|}) # evs)  
    3.38          ==> K = K' | K \<in> AuthKeys evs"
    3.39 -apply (unfold AuthKeys_def, auto)
    3.40 -done
    3.41 +by (unfold AuthKeys_def, auto)
    3.42  
    3.43  lemma AuthKeysI: 
    3.44     "Says Kas A (Crypt (shrK A) {|Key K, Agent Tgs, Number Tk,  
    3.45       (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key K, Number Tk|})|}) \<in> set evs  
    3.46          ==> K \<in> AuthKeys evs"
    3.47 -apply (unfold AuthKeys_def, auto)
    3.48 -done
    3.49 +by (unfold AuthKeys_def, auto)
    3.50  
    3.51  lemma AuthKeys_used: "K \<in> AuthKeys evs ==> Key K \<in> used evs"
    3.52  by (simp add: AuthKeys_def, blast)
    3.53 @@ -344,8 +341,7 @@
    3.54  lemma K5_msg_in_parts_spies:
    3.55       "Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|}) 
    3.56                 \<in> set evs ==> ServTicket \<in> parts (spies evs)"
    3.57 -apply blast
    3.58 -done
    3.59 +by blast
    3.60  
    3.61  lemma Oops_range_spies2:
    3.62       "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})  
    3.63 @@ -358,8 +354,7 @@
    3.64  lemma Says_ticket_in_parts_spies:
    3.65       "Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \<in> set evs  
    3.66        ==> Ticket \<in> parts (spies evs)"
    3.67 -apply blast
    3.68 -done
    3.69 +by blast
    3.70  
    3.71  
    3.72  (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    3.73 @@ -980,8 +975,7 @@
    3.74           ~ ExpirAuth Tk evs;
    3.75           A \<notin> bad;  evs \<in> kerberos |]
    3.76        ==> Key AuthKey \<notin> analz (spies evs)"
    3.77 -apply (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
    3.78 -done
    3.79 +by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
    3.80  
    3.81  
    3.82  subsection{* Guarantees for Tgs *}
    3.83 @@ -1261,8 +1255,8 @@
    3.84           ~ ExpirAuth Tk evs; A \<notin> bad; evs \<in> kerberos |]
    3.85   ==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
    3.86         \<in> set evs"
    3.87 -apply (blast dest: A_trusts_AuthKey Confidentiality_Auth_A A_trusts_K4_bis)
    3.88 -done
    3.89 +by (blast dest: A_trusts_AuthKey Confidentiality_Auth_A A_trusts_K4_bis)
    3.90 +
    3.91  text{*Note: requires a temporal check*}
    3.92  
    3.93  
    3.94 @@ -1422,8 +1416,7 @@
    3.95           ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;
    3.96           A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
    3.97        ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
    3.98 -apply (blast dest!: Confidentiality_B B_Knows_B_Knows_ServKey_lemma)
    3.99 -done
   3.100 +by (blast dest!: Confidentiality_B B_Knows_B_Knows_ServKey_lemma)
   3.101  
   3.102  lemma B_Knows_B_Knows_ServKey_refined:
   3.103       "[| Says B A (Crypt ServKey (Number Ta)) \<in> set evs;
   3.104 @@ -1432,9 +1425,7 @@
   3.105           ~ ExpirServ Tt evs;
   3.106           A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
   3.107        ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
   3.108 -apply (blast dest!: Confidentiality_B_refined B_Knows_B_Knows_ServKey_lemma)
   3.109 -done
   3.110 -
   3.111 +by (blast dest!: Confidentiality_B_refined B_Knows_B_Knows_ServKey_lemma)
   3.112  
   3.113  lemma A_Knows_B_Knows_ServKey:
   3.114       "[| Crypt ServKey (Number Ta) \<in> parts (spies evs);
   3.115 @@ -1445,8 +1436,7 @@
   3.116           ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;
   3.117           A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
   3.118        ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
   3.119 -apply (blast dest!: B_Authenticity Confidentiality_Serv_A B_Knows_B_Knows_ServKey_lemma)
   3.120 -done
   3.121 +by (blast dest!: B_Authenticity Confidentiality_Serv_A B_Knows_B_Knows_ServKey_lemma)
   3.122  
   3.123  lemma K3_imp_K2:
   3.124       "[| Says A Tgs
   3.125 @@ -1525,8 +1515,7 @@
   3.126           ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;
   3.127           B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos |]
   3.128     ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs"
   3.129 -apply (blast dest!: Confidentiality_Serv_A A_Knows_A_Knows_ServKey_lemma)
   3.130 -done
   3.131 +by (blast dest!: Confidentiality_Serv_A A_Knows_A_Knows_ServKey_lemma)
   3.132  
   3.133  lemma B_Knows_A_Knows_ServKey:
   3.134       "[| Crypt ServKey {|Agent A, Number Ta|} \<in> parts (spies evs);
   3.135 @@ -1539,8 +1528,7 @@
   3.136           ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;
   3.137           B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos |]
   3.138     ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs"
   3.139 -apply (blast dest: A_Authenticity Confidentiality_B A_Knows_A_Knows_ServKey_lemma)
   3.140 -done
   3.141 +by (blast dest: A_Authenticity Confidentiality_B A_Knows_A_Knows_ServKey_lemma)
   3.142  
   3.143  
   3.144  lemma B_Knows_A_Knows_ServKey_refined:
   3.145 @@ -1550,7 +1538,6 @@
   3.146           ~ ExpirServ Tt evs;
   3.147           B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerberos |]
   3.148     ==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs"
   3.149 -apply (blast dest: A_Authenticity_refined Confidentiality_B_refined A_Knows_A_Knows_ServKey_lemma)
   3.150 -done
   3.151 +by (blast dest: A_Authenticity_refined Confidentiality_B_refined A_Knows_A_Knows_ServKey_lemma)
   3.152  
   3.153  end
     4.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Tue Sep 23 15:40:27 2003 +0200
     4.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Tue Sep 23 15:41:33 2003 +0200
     4.3 @@ -100,20 +100,22 @@
     4.4  	  ==> Notes Spy {|Number Ts, Key K|} # evso \<in> kerberos_ban"
     4.5  
     4.6  
     4.7 -declare Says_imp_knows_Spy [THEN parts.Inj, dest] parts.Body [dest]
     4.8 -declare analz_subset_parts [THEN subsetD, dest]
     4.9 -declare Fake_parts_insert [THEN subsetD, dest]
    4.10 +declare Says_imp_knows_Spy [THEN parts.Inj, dest] 
    4.11 +declare parts.Body [dest]
    4.12 +declare analz_into_parts [dest]
    4.13 +declare Fake_parts_insert_in_Un [dest]
    4.14  
    4.15  (*A "possibility property": there are traces that reach the end.*)
    4.16 -lemma "\<exists>Timestamp K. \<exists>evs \<in> kerberos_ban.     
    4.17 +lemma "Key K \<notin> used []
    4.18 +       ==> \<exists>Timestamp. \<exists>evs \<in> kerberos_ban.     
    4.19               Says B A (Crypt K (Number Timestamp))  
    4.20                    \<in> set evs"
    4.21  apply (cut_tac SesKeyLife_LB)
    4.22  apply (intro exI bexI)
    4.23  apply (rule_tac [2] 
    4.24             kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2, 
    4.25 -                             THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4], possibility)
    4.26 -apply (simp_all (no_asm_simp))
    4.27 +                             THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4])
    4.28 +apply (possibility, simp_all (no_asm_simp) add: used_Cons)
    4.29  done
    4.30  
    4.31  
     5.1 --- a/src/HOL/Auth/Message.thy	Tue Sep 23 15:40:27 2003 +0200
     5.2 +++ b/src/HOL/Auth/Message.thy	Tue Sep 23 15:41:33 2003 +0200
     5.3 @@ -39,13 +39,13 @@
     5.4    agent = Server | Friend nat | Spy
     5.5  
     5.6  datatype
     5.7 -     msg = Agent  agent	    (*Agent names*)
     5.8 -         | Number nat       (*Ordinary integers, timestamps, ...*)
     5.9 -         | Nonce  nat       (*Unguessable nonces*)
    5.10 -         | Key    key       (*Crypto keys*)
    5.11 -	 | Hash   msg       (*Hashing*)
    5.12 -	 | MPair  msg msg   (*Compound messages*)
    5.13 -	 | Crypt  key msg   (*Encryption, public- or shared-key*)
    5.14 +     msg = Agent  agent	    --{*Agent names*}
    5.15 +         | Number nat       --{*Ordinary integers, timestamps, ...*}
    5.16 +         | Nonce  nat       --{*Unguessable nonces*}
    5.17 +         | Key    key       --{*Crypto keys*}
    5.18 +	 | Hash   msg       --{*Hashing*}
    5.19 +	 | MPair  msg msg   --{*Compound messages*}
    5.20 +	 | Crypt  key msg   --{*Encryption, public- or shared-key*}
    5.21  
    5.22  
    5.23  (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
    5.24 @@ -69,7 +69,7 @@
    5.25    keysFor :: "msg set => key set"
    5.26    "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
    5.27  
    5.28 -(** Inductive definition of all "parts" of a message.  **)
    5.29 +subsubsection{*Inductive definition of all "parts" of a message.  *}
    5.30  
    5.31  consts  parts   :: "msg set => msg set"
    5.32  inductive "parts H"
    5.33 @@ -81,7 +81,7 @@
    5.34  
    5.35  
    5.36  (*Monotonicity*)
    5.37 -lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
    5.38 +lemma parts_mono: "G\<subseteq>H ==> parts(G) \<subseteq> parts(H)"
    5.39  apply auto
    5.40  apply (erule parts.induct) 
    5.41  apply (auto dest: Fst Snd Body) 
    5.42 @@ -99,7 +99,7 @@
    5.43  by auto
    5.44  
    5.45  
    5.46 -(** Inverse of keys **)
    5.47 +subsubsection{*Inverse of keys *}
    5.48  
    5.49  lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
    5.50  apply safe
    5.51 @@ -142,8 +142,7 @@
    5.52  
    5.53  lemma keysFor_insert_Crypt [simp]: 
    5.54      "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
    5.55 -apply (unfold keysFor_def, auto)
    5.56 -done
    5.57 +by (unfold keysFor_def, auto)
    5.58  
    5.59  lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
    5.60  by (unfold keysFor_def, auto)
    5.61 @@ -183,7 +182,7 @@
    5.62  by (erule parts.induct, blast+)
    5.63  
    5.64  
    5.65 -(** Unions **)
    5.66 +subsubsection{*Unions *}
    5.67  
    5.68  lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
    5.69  by (intro Un_least parts_mono Un_upper1 Un_upper2)
    5.70 @@ -203,7 +202,8 @@
    5.71  
    5.72  (*TWO inserts to avoid looping.  This rewrite is better than nothing.
    5.73    Not suitable for Addsimps: its behaviour can be strange.*)
    5.74 -lemma parts_insert2: "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
    5.75 +lemma parts_insert2:
    5.76 +     "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
    5.77  apply (simp add: Un_assoc)
    5.78  apply (simp add: parts_insert [symmetric])
    5.79  done
    5.80 @@ -231,7 +231,7 @@
    5.81  lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
    5.82  by (blast intro: parts_mono [THEN [2] rev_subsetD])
    5.83  
    5.84 -(** Idempotence and transitivity **)
    5.85 +subsubsection{*Idempotence and transitivity *}
    5.86  
    5.87  lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
    5.88  by (erule parts.induct, blast+)
    5.89 @@ -243,46 +243,51 @@
    5.90  by (drule parts_mono, blast)
    5.91  
    5.92  (*Cut*)
    5.93 -lemma parts_cut: "[| Y\<in> parts (insert X G);  X\<in> parts H |]  
    5.94 -               ==> Y\<in> parts (G \<union> H)"
    5.95 -apply (erule parts_trans, auto)
    5.96 -done
    5.97 +lemma parts_cut:
    5.98 +     "[| Y\<in> parts (insert X G);  X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
    5.99 +by (erule parts_trans, auto)
   5.100  
   5.101  lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
   5.102  by (force dest!: parts_cut intro: parts_insertI)
   5.103  
   5.104  
   5.105 -(** Rewrite rules for pulling out atomic messages **)
   5.106 +subsubsection{*Rewrite rules for pulling out atomic messages *}
   5.107  
   5.108  lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
   5.109  
   5.110  
   5.111 -lemma parts_insert_Agent [simp]: "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
   5.112 +lemma parts_insert_Agent [simp]:
   5.113 +     "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
   5.114  apply (rule parts_insert_eq_I) 
   5.115  apply (erule parts.induct, auto) 
   5.116  done
   5.117  
   5.118 -lemma parts_insert_Nonce [simp]: "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
   5.119 +lemma parts_insert_Nonce [simp]:
   5.120 +     "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
   5.121  apply (rule parts_insert_eq_I) 
   5.122  apply (erule parts.induct, auto) 
   5.123  done
   5.124  
   5.125 -lemma parts_insert_Number [simp]: "parts (insert (Number N) H) = insert (Number N) (parts H)"
   5.126 +lemma parts_insert_Number [simp]:
   5.127 +     "parts (insert (Number N) H) = insert (Number N) (parts H)"
   5.128  apply (rule parts_insert_eq_I) 
   5.129  apply (erule parts.induct, auto) 
   5.130  done
   5.131  
   5.132 -lemma parts_insert_Key [simp]: "parts (insert (Key K) H) = insert (Key K) (parts H)"
   5.133 +lemma parts_insert_Key [simp]:
   5.134 +     "parts (insert (Key K) H) = insert (Key K) (parts H)"
   5.135  apply (rule parts_insert_eq_I) 
   5.136  apply (erule parts.induct, auto) 
   5.137  done
   5.138  
   5.139 -lemma parts_insert_Hash [simp]: "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
   5.140 +lemma parts_insert_Hash [simp]:
   5.141 +     "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
   5.142  apply (rule parts_insert_eq_I) 
   5.143  apply (erule parts.induct, auto) 
   5.144  done
   5.145  
   5.146 -lemma parts_insert_Crypt [simp]: "parts (insert (Crypt K X) H) =  
   5.147 +lemma parts_insert_Crypt [simp]:
   5.148 +     "parts (insert (Crypt K X) H) =  
   5.149            insert (Crypt K X) (parts (insert X H))"
   5.150  apply (rule equalityI)
   5.151  apply (rule subsetI)
   5.152 @@ -291,7 +296,8 @@
   5.153  apply (blast intro: parts.Body)+
   5.154  done
   5.155  
   5.156 -lemma parts_insert_MPair [simp]: "parts (insert {|X,Y|} H) =  
   5.157 +lemma parts_insert_MPair [simp]:
   5.158 +     "parts (insert {|X,Y|} H) =  
   5.159            insert {|X,Y|} (parts (insert X (insert Y H)))"
   5.160  apply (rule equalityI)
   5.161  apply (rule subsetI)
   5.162 @@ -320,9 +326,9 @@
   5.163  
   5.164  subsection{*Inductive relation "analz"*}
   5.165  
   5.166 -(** Inductive definition of "analz" -- what can be broken down from a set of
   5.167 +text{*Inductive definition of "analz" -- what can be broken down from a set of
   5.168      messages, including keys.  A form of downward closure.  Pairs can
   5.169 -    be taken apart; messages decrypted with known keys.  **)
   5.170 +    be taken apart; messages decrypted with known keys.  *}
   5.171  
   5.172  consts  analz   :: "msg set => msg set"
   5.173  inductive "analz H"
   5.174 @@ -335,7 +341,7 @@
   5.175  
   5.176  
   5.177  (*Monotonicity; Lemma 1 of Lowe's paper*)
   5.178 -lemma analz_mono: "G<=H ==> analz(G) <= analz(H)"
   5.179 +lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
   5.180  apply auto
   5.181  apply (erule analz.induct) 
   5.182  apply (auto dest: Fst Snd) 
   5.183 @@ -356,6 +362,8 @@
   5.184  apply (erule analz.induct, blast+)
   5.185  done
   5.186  
   5.187 +lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   5.188 +
   5.189  lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
   5.190  
   5.191  
   5.192 @@ -372,7 +380,7 @@
   5.193  
   5.194  lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
   5.195  
   5.196 -(** General equational properties **)
   5.197 +subsubsection{*General equational properties *}
   5.198  
   5.199  lemma analz_empty [simp]: "analz{} = {}"
   5.200  apply safe
   5.201 @@ -387,26 +395,30 @@
   5.202  lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
   5.203  by (blast intro: analz_mono [THEN [2] rev_subsetD])
   5.204  
   5.205 -(** Rewrite rules for pulling out atomic messages **)
   5.206 +subsubsection{*Rewrite rules for pulling out atomic messages *}
   5.207  
   5.208  lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
   5.209  
   5.210 -lemma analz_insert_Agent [simp]: "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
   5.211 +lemma analz_insert_Agent [simp]:
   5.212 +     "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
   5.213  apply (rule analz_insert_eq_I) 
   5.214  apply (erule analz.induct, auto) 
   5.215  done
   5.216  
   5.217 -lemma analz_insert_Nonce [simp]: "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
   5.218 +lemma analz_insert_Nonce [simp]:
   5.219 +     "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
   5.220  apply (rule analz_insert_eq_I) 
   5.221  apply (erule analz.induct, auto) 
   5.222  done
   5.223  
   5.224 -lemma analz_insert_Number [simp]: "analz (insert (Number N) H) = insert (Number N) (analz H)"
   5.225 +lemma analz_insert_Number [simp]:
   5.226 +     "analz (insert (Number N) H) = insert (Number N) (analz H)"
   5.227  apply (rule analz_insert_eq_I) 
   5.228  apply (erule analz.induct, auto) 
   5.229  done
   5.230  
   5.231 -lemma analz_insert_Hash [simp]: "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
   5.232 +lemma analz_insert_Hash [simp]:
   5.233 +     "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
   5.234  apply (rule analz_insert_eq_I) 
   5.235  apply (erule analz.induct, auto) 
   5.236  done
   5.237 @@ -420,7 +432,8 @@
   5.238  apply (erule analz.induct, auto) 
   5.239  done
   5.240  
   5.241 -lemma analz_insert_MPair [simp]: "analz (insert {|X,Y|} H) =  
   5.242 +lemma analz_insert_MPair [simp]:
   5.243 +     "analz (insert {|X,Y|} H) =  
   5.244            insert {|X,Y|} (analz (insert X (insert Y H)))"
   5.245  apply (rule equalityI)
   5.246  apply (rule subsetI)
   5.247 @@ -453,7 +466,8 @@
   5.248  apply (blast intro: analz_insertI analz.Decrypt)
   5.249  done
   5.250  
   5.251 -lemma analz_insert_Decrypt: "Key (invKey K) \<in> analz H ==>   
   5.252 +lemma analz_insert_Decrypt:
   5.253 +     "Key (invKey K) \<in> analz H ==>   
   5.254                 analz (insert (Crypt K X) H) =  
   5.255                 insert (Crypt K X) (analz (insert X H))"
   5.256  by (intro equalityI lemma1 lemma2)
   5.257 @@ -471,7 +485,8 @@
   5.258  
   5.259  
   5.260  (*This rule supposes "for the sake of argument" that we have the key.*)
   5.261 -lemma analz_insert_Crypt_subset: "analz (insert (Crypt K X) H) \<subseteq>   
   5.262 +lemma analz_insert_Crypt_subset:
   5.263 +     "analz (insert (Crypt K X) H) \<subseteq>   
   5.264             insert (Crypt K X) (analz (insert X H))"
   5.265  apply (rule subsetI)
   5.266  apply (erule analz.induct, auto)
   5.267 @@ -484,7 +499,7 @@
   5.268  done
   5.269  
   5.270  
   5.271 -(** Idempotence and transitivity **)
   5.272 +subsubsection{*Idempotence and transitivity *}
   5.273  
   5.274  lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
   5.275  by (erule analz.induct, blast+)
   5.276 @@ -510,32 +525,35 @@
   5.277  by (blast intro: analz_cut analz_insertI)
   5.278  
   5.279  
   5.280 -(** A congruence rule for "analz" **)
   5.281 +text{*A congruence rule for "analz" *}
   5.282  
   5.283 -lemma analz_subset_cong: "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'  
   5.284 +lemma analz_subset_cong:
   5.285 +     "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'  
   5.286                 |] ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
   5.287  apply clarify
   5.288  apply (erule analz.induct)
   5.289  apply (best intro: analz_mono [THEN subsetD])+
   5.290  done
   5.291  
   5.292 -lemma analz_cong: "[| analz G = analz G'; analz H = analz H'  
   5.293 +lemma analz_cong:
   5.294 +     "[| analz G = analz G'; analz H = analz H'  
   5.295                 |] ==> analz (G \<union> H) = analz (G' \<union> H')"
   5.296 -apply (intro equalityI analz_subset_cong, simp_all) 
   5.297 -done
   5.298 +by (intro equalityI analz_subset_cong, simp_all) 
   5.299  
   5.300 -
   5.301 -lemma analz_insert_cong: "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   5.302 +lemma analz_insert_cong:
   5.303 +     "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
   5.304  by (force simp only: insert_def intro!: analz_cong)
   5.305  
   5.306  (*If there are no pairs or encryptions then analz does nothing*)
   5.307 -lemma analz_trivial: "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   5.308 +lemma analz_trivial:
   5.309 +     "[| \<forall>X Y. {|X,Y|} \<notin> H;  \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
   5.310  apply safe
   5.311  apply (erule analz.induct, blast+)
   5.312  done
   5.313  
   5.314  (*These two are obsolete (with a single Spy) but cost little to prove...*)
   5.315 -lemma analz_UN_analz_lemma: "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   5.316 +lemma analz_UN_analz_lemma:
   5.317 +     "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
   5.318  apply (erule analz.induct)
   5.319  apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
   5.320  done
   5.321 @@ -546,10 +564,10 @@
   5.322  
   5.323  subsection{*Inductive relation "synth"*}
   5.324  
   5.325 -(** Inductive definition of "synth" -- what can be built up from a set of
   5.326 +text{*Inductive definition of "synth" -- what can be built up from a set of
   5.327      messages.  A form of upward closure.  Pairs can be built, messages
   5.328      encrypted with known keys.  Agent names are public domain.
   5.329 -    Numbers can be guessed, but Nonces cannot be.  **)
   5.330 +    Numbers can be guessed, but Nonces cannot be.  *}
   5.331  
   5.332  consts  synth   :: "msg set => msg set"
   5.333  inductive "synth H"
   5.334 @@ -562,7 +580,7 @@
   5.335      Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
   5.336  
   5.337  (*Monotonicity*)
   5.338 -lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
   5.339 +lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   5.340  apply auto
   5.341  apply (erule synth.induct) 
   5.342  apply (auto dest: Fst Snd Body) 
   5.343 @@ -579,7 +597,7 @@
   5.344  lemma synth_increasing: "H \<subseteq> synth(H)"
   5.345  by blast
   5.346  
   5.347 -(** Unions **)
   5.348 +subsubsection{*Unions *}
   5.349  
   5.350  (*Converse fails: we can synth more from the union than from the 
   5.351    separate parts, building a compound message using elements of each.*)
   5.352 @@ -589,7 +607,7 @@
   5.353  lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
   5.354  by (blast intro: synth_mono [THEN [2] rev_subsetD])
   5.355  
   5.356 -(** Idempotence and transitivity **)
   5.357 +subsubsection{*Idempotence and transitivity *}
   5.358  
   5.359  lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
   5.360  by (erule synth.induct, blast+)
   5.361 @@ -616,17 +634,17 @@
   5.362  lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
   5.363  by blast
   5.364  
   5.365 -lemma Crypt_synth_eq [simp]: "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
   5.366 +lemma Crypt_synth_eq [simp]:
   5.367 +     "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
   5.368  by blast
   5.369  
   5.370  
   5.371  lemma keysFor_synth [simp]: 
   5.372      "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
   5.373 -apply (unfold keysFor_def, blast)
   5.374 -done
   5.375 +by (unfold keysFor_def, blast)
   5.376  
   5.377  
   5.378 -(*** Combinations of parts, analz and synth ***)
   5.379 +subsubsection{*Combinations of parts, analz and synth *}
   5.380  
   5.381  lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
   5.382  apply (rule equalityI)
   5.383 @@ -655,22 +673,29 @@
   5.384  done
   5.385  
   5.386  
   5.387 -(** For reasoning about the Fake rule in traces **)
   5.388 +subsubsection{*For reasoning about the Fake rule in traces *}
   5.389  
   5.390  lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   5.391  by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
   5.392  
   5.393  (*More specifically for Fake.  Very occasionally we could do with a version
   5.394    of the form  parts{X} \<subseteq> synth (analz H) \<union> parts H *)
   5.395 -lemma Fake_parts_insert: "X \<in> synth (analz H) ==>  
   5.396 +lemma Fake_parts_insert:
   5.397 +     "X \<in> synth (analz H) ==>  
   5.398        parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   5.399  apply (drule parts_insert_subset_Un)
   5.400  apply (simp (no_asm_use))
   5.401  apply blast
   5.402  done
   5.403  
   5.404 +lemma Fake_parts_insert_in_Un:
   5.405 +     "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   5.406 +      ==> Z \<in>  synth (analz H) \<union> parts H";
   5.407 +by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   5.408 +
   5.409  (*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*)
   5.410 -lemma Fake_analz_insert: "X\<in> synth (analz G) ==>  
   5.411 +lemma Fake_analz_insert:
   5.412 +     "X\<in> synth (analz G) ==>  
   5.413        analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   5.414  apply (rule subsetI)
   5.415  apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
   5.416 @@ -679,10 +704,12 @@
   5.417  apply blast
   5.418  done
   5.419  
   5.420 -lemma analz_conj_parts [simp]: "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
   5.421 +lemma analz_conj_parts [simp]:
   5.422 +     "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
   5.423  by (blast intro: analz_subset_parts [THEN subsetD])
   5.424  
   5.425 -lemma analz_disj_parts [simp]: "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
   5.426 +lemma analz_disj_parts [simp]:
   5.427 +     "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
   5.428  by (blast intro: analz_subset_parts [THEN subsetD])
   5.429  
   5.430  (*Without this equation, other rules for synth and analz would yield
   5.431 @@ -692,19 +719,21 @@
   5.432        (X \<in> synth (analz H) & Y \<in> synth (analz H))"
   5.433  by blast
   5.434  
   5.435 -lemma Crypt_synth_analz: "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]  
   5.436 +lemma Crypt_synth_analz:
   5.437 +     "[| Key K \<in> analz H;  Key (invKey K) \<in> analz H |]  
   5.438         ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
   5.439  by blast
   5.440  
   5.441  
   5.442 -lemma Hash_synth_analz [simp]: "X \<notin> synth (analz H)  
   5.443 +lemma Hash_synth_analz [simp]:
   5.444 +     "X \<notin> synth (analz H)  
   5.445        ==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
   5.446  by blast
   5.447  
   5.448  
   5.449  subsection{*HPair: a combination of Hash and MPair*}
   5.450  
   5.451 -(*** Freeness ***)
   5.452 +subsubsection{*Freeness *}
   5.453  
   5.454  lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
   5.455  by (unfold HPair_def, simp)
   5.456 @@ -733,14 +762,16 @@
   5.457  lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"
   5.458  by (simp add: HPair_def)
   5.459  
   5.460 -lemma MPair_eq_HPair [iff]: "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
   5.461 +lemma MPair_eq_HPair [iff]:
   5.462 +     "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
   5.463  by (simp add: HPair_def)
   5.464  
   5.465 -lemma HPair_eq_MPair [iff]: "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
   5.466 +lemma HPair_eq_MPair [iff]:
   5.467 +     "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
   5.468  by (auto simp add: HPair_def)
   5.469  
   5.470  
   5.471 -(*** Specialized laws, proved in terms of those for Hash and MPair ***)
   5.472 +subsubsection{*Specialized laws, proved in terms of those for Hash and MPair *}
   5.473  
   5.474  lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
   5.475  by (simp add: HPair_def)
   5.476 @@ -766,37 +797,10 @@
   5.477  declare parts.Body [rule del]
   5.478  
   5.479  
   5.480 +text{*Rewrites to push in Key and Crypt messages, so that other messages can
   5.481 +    be pulled out using the @{text analz_insert} rules*}
   5.482  ML
   5.483  {*
   5.484 -(*ML bindings for definitions*)
   5.485 -
   5.486 -val invKey = thm "invKey"
   5.487 -val keysFor_def = thm "keysFor_def"
   5.488 -val HPair_def = thm "HPair_def"
   5.489 -val symKeys_def = thm "symKeys_def"
   5.490 -
   5.491 -structure parts =
   5.492 -  struct
   5.493 -  val induct = thm "parts.induct"
   5.494 -  val Inj    = thm "parts.Inj"
   5.495 -  val Fst    = thm "parts.Fst"
   5.496 -  val Snd    = thm "parts.Snd"
   5.497 -  val Body   = thm "parts.Body"
   5.498 -  end
   5.499 -
   5.500 -structure analz =
   5.501 -  struct
   5.502 -  val induct = thm "analz.induct"
   5.503 -  val Inj    = thm "analz.Inj"
   5.504 -  val Fst    = thm "analz.Fst"
   5.505 -  val Snd    = thm "analz.Snd"
   5.506 -  val Decrypt = thm "analz.Decrypt"
   5.507 -  end
   5.508 -
   5.509 -
   5.510 -(** Rewrites to push in Key and Crypt messages, so that other messages can
   5.511 -    be pulled out using the analz_insert rules **)
   5.512 -
   5.513  fun insComm x y = inst "x" x (inst "y" y insert_commute);
   5.514  
   5.515  bind_thms ("pushKeys",
   5.516 @@ -818,79 +822,19 @@
   5.517  subsection{*Tactics useful for many protocol proofs*}
   5.518  ML
   5.519  {*
   5.520 +val invKey = thm "invKey"
   5.521 +val keysFor_def = thm "keysFor_def"
   5.522 +val HPair_def = thm "HPair_def"
   5.523 +val symKeys_def = thm "symKeys_def"
   5.524  val parts_mono = thm "parts_mono";
   5.525  val analz_mono = thm "analz_mono";
   5.526 -val Key_image_eq = thm "Key_image_eq";
   5.527 -val Nonce_Key_image_eq = thm "Nonce_Key_image_eq";
   5.528 -val keysFor_Un = thm "keysFor_Un";
   5.529 -val keysFor_mono = thm "keysFor_mono";
   5.530 -val keysFor_image_Key = thm "keysFor_image_Key";
   5.531 -val Crypt_imp_invKey_keysFor = thm "Crypt_imp_invKey_keysFor";
   5.532 -val MPair_parts = thm "MPair_parts";
   5.533 -val parts_increasing = thm "parts_increasing";
   5.534 -val parts_insertI = thm "parts_insertI";
   5.535 -val parts_empty = thm "parts_empty";
   5.536 -val parts_emptyE = thm "parts_emptyE";
   5.537 -val parts_singleton = thm "parts_singleton";
   5.538 -val parts_Un_subset1 = thm "parts_Un_subset1";
   5.539 -val parts_Un_subset2 = thm "parts_Un_subset2";
   5.540 -val parts_insert = thm "parts_insert";
   5.541 -val parts_insert2 = thm "parts_insert2";
   5.542 -val parts_UN_subset1 = thm "parts_UN_subset1";
   5.543 -val parts_UN_subset2 = thm "parts_UN_subset2";
   5.544 -val parts_UN = thm "parts_UN";
   5.545 -val parts_insert_subset = thm "parts_insert_subset";
   5.546 -val parts_partsD = thm "parts_partsD";
   5.547 -val parts_trans = thm "parts_trans";
   5.548 -val parts_cut = thm "parts_cut";
   5.549 -val parts_cut_eq = thm "parts_cut_eq";
   5.550 -val parts_insert_eq_I = thm "parts_insert_eq_I";
   5.551 -val parts_image_Key = thm "parts_image_Key";
   5.552 -val MPair_analz = thm "MPair_analz";
   5.553 +val synth_mono = thm "synth_mono";
   5.554  val analz_increasing = thm "analz_increasing";
   5.555 +
   5.556 +val analz_insertI = thm "analz_insertI";
   5.557  val analz_subset_parts = thm "analz_subset_parts";
   5.558 -val not_parts_not_analz = thm "not_parts_not_analz";
   5.559 -val parts_analz = thm "parts_analz";
   5.560 -val analz_parts = thm "analz_parts";
   5.561 -val analz_insertI = thm "analz_insertI";
   5.562 -val analz_empty = thm "analz_empty";
   5.563 -val analz_Un = thm "analz_Un";
   5.564 -val analz_insert_Crypt_subset = thm "analz_insert_Crypt_subset";
   5.565 -val analz_image_Key = thm "analz_image_Key";
   5.566 -val analz_analzD = thm "analz_analzD";
   5.567 -val analz_trans = thm "analz_trans";
   5.568 -val analz_cut = thm "analz_cut";
   5.569 -val analz_insert_eq = thm "analz_insert_eq";
   5.570 -val analz_subset_cong = thm "analz_subset_cong";
   5.571 -val analz_cong = thm "analz_cong";
   5.572 -val analz_insert_cong = thm "analz_insert_cong";
   5.573 -val analz_trivial = thm "analz_trivial";
   5.574 -val analz_UN_analz = thm "analz_UN_analz";
   5.575 -val synth_mono = thm "synth_mono";
   5.576 -val synth_increasing = thm "synth_increasing";
   5.577 -val synth_Un = thm "synth_Un";
   5.578 -val synth_insert = thm "synth_insert";
   5.579 -val synth_synthD = thm "synth_synthD";
   5.580 -val synth_trans = thm "synth_trans";
   5.581 -val synth_cut = thm "synth_cut";
   5.582 -val Agent_synth = thm "Agent_synth";
   5.583 -val Number_synth = thm "Number_synth";
   5.584 -val Nonce_synth_eq = thm "Nonce_synth_eq";
   5.585 -val Key_synth_eq = thm "Key_synth_eq";
   5.586 -val Crypt_synth_eq = thm "Crypt_synth_eq";
   5.587 -val keysFor_synth = thm "keysFor_synth";
   5.588 -val parts_synth = thm "parts_synth";
   5.589 -val analz_analz_Un = thm "analz_analz_Un";
   5.590 -val analz_synth_Un = thm "analz_synth_Un";
   5.591 -val analz_synth = thm "analz_synth";
   5.592 -val parts_insert_subset_Un = thm "parts_insert_subset_Un";
   5.593  val Fake_parts_insert = thm "Fake_parts_insert";
   5.594  val Fake_analz_insert = thm "Fake_analz_insert";
   5.595 -val analz_conj_parts = thm "analz_conj_parts";
   5.596 -val analz_disj_parts = thm "analz_disj_parts";
   5.597 -val MPair_synth_analz = thm "MPair_synth_analz";
   5.598 -val Crypt_synth_analz = thm "Crypt_synth_analz";
   5.599 -val Hash_synth_analz = thm "Hash_synth_analz";
   5.600  val pushes = thms "pushes";
   5.601  
   5.602  
   5.603 @@ -952,7 +896,7 @@
   5.604  lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
   5.605  by auto
   5.606  
   5.607 -lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))"
   5.608 +lemma synth_analz_mono: "G\<subseteq>H ==> synth (analz(G)) \<subseteq> synth (analz(H))"
   5.609  by (simp add: synth_mono analz_mono) 
   5.610  
   5.611  lemma Fake_analz_eq [simp]:
   5.612 @@ -964,14 +908,6 @@
   5.613  apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD]) 
   5.614  done
   5.615  
   5.616 -
   5.617 -lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
   5.618 -
   5.619 -lemma Fake_parts_insert_in_Un:
   5.620 -     "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
   5.621 -      ==> Z \<in>  synth (analz H) \<union> parts H";
   5.622 -by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   5.623 -
   5.624  text{*Two generalizations of @{text analz_insert_eq}*}
   5.625  lemma gen_analz_insert_eq [rule_format]:
   5.626       "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
     6.1 --- a/src/HOL/Auth/NS_Public.thy	Tue Sep 23 15:40:27 2003 +0200
     6.2 +++ b/src/HOL/Auth/NS_Public.thy	Tue Sep 23 15:41:33 2003 +0200
     6.3 @@ -43,8 +43,9 @@
     6.4            \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
     6.5  
     6.6  declare knows_Spy_partsEs [elim]
     6.7 -declare analz_subset_parts [THEN subsetD, dest]
     6.8 -declare Fake_parts_insert [THEN subsetD, dest]
     6.9 +declare knows_Spy_partsEs [elim]
    6.10 +declare analz_into_parts [dest]
    6.11 +declare Fake_parts_insert_in_Un  [dest]
    6.12  declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    6.13  
    6.14  (*A "possibility property": there are traces that reach the end*)
    6.15 @@ -55,9 +56,6 @@
    6.16  apply possibility
    6.17  done
    6.18  
    6.19 -
    6.20 -(**** Inductive proofs about ns_public ****)
    6.21 -
    6.22  (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
    6.23      sends messages containing X! **)
    6.24  
    6.25 @@ -70,8 +68,7 @@
    6.26        "evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> analz (spies evs)) = (A \<in> bad)"
    6.27  by auto
    6.28  
    6.29 -
    6.30 -(*** Authenticity properties obtained from NS2 ***)
    6.31 +subsection{*Authenticity properties obtained from NS2*}
    6.32  
    6.33  
    6.34  (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
    6.35 @@ -143,8 +140,7 @@
    6.36  done
    6.37  
    6.38  
    6.39 -
    6.40 -(*** Authenticity properties obtained from NS2 ***)
    6.41 +subsection{*Authenticity properties obtained from NS2*}
    6.42  
    6.43  (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B 
    6.44    [unicity of B makes Lowe's fix work]
    6.45 @@ -189,8 +185,7 @@
    6.46        \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
    6.47  by (blast intro: B_trusts_NS3_lemma)
    6.48  
    6.49 -(*** Overall guarantee for B ***)
    6.50 -
    6.51 +subsection{*Overall guarantee for B*}
    6.52  
    6.53  (*If NS3 has been sent and the nonce NB agrees with the nonce B joined with
    6.54    NA, then A initiated the run using NA.*)
     7.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Tue Sep 23 15:40:27 2003 +0200
     7.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Tue Sep 23 15:41:33 2003 +0200
     7.3 @@ -46,8 +46,8 @@
     7.4            \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
     7.5  
     7.6  declare knows_Spy_partsEs [elim]
     7.7 -declare analz_subset_parts [THEN subsetD, dest]
     7.8 -declare Fake_parts_insert [THEN subsetD, dest]
     7.9 +declare analz_into_parts [dest]
    7.10 +declare Fake_parts_insert_in_Un  [dest]
    7.11  declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    7.12  
    7.13  (*A "possibility property": there are traces that reach the end*)
    7.14 @@ -207,6 +207,9 @@
    7.15  apply (frule_tac A' = A in 
    7.16         Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
    7.17  apply (rename_tac C B' evs3)
    7.18 +txt{*This is the attack!
    7.19 +@{subgoals[display,indent=0,margin=65]}
    7.20 +*}
    7.21  oops
    7.22  
    7.23  (*
     8.1 --- a/src/HOL/Auth/NS_Shared.thy	Tue Sep 23 15:40:27 2003 +0200
     8.2 +++ b/src/HOL/Auth/NS_Shared.thy	Tue Sep 23 15:41:33 2003 +0200
     8.3 @@ -80,12 +80,14 @@
     8.4  
     8.5  
     8.6  text{*A "possibility property": there are traces that reach the end*}
     8.7 -lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
     8.8 -                              Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
     8.9 +lemma "[| A \<noteq> Server; Key K \<notin> used [] |] 
    8.10 +       ==> \<exists>N. \<exists>evs \<in> ns_shared.
    8.11 +                    Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
    8.12  apply (intro exI bexI)
    8.13  apply (rule_tac [2] ns_shared.Nil
    8.14         [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
    8.15 -	THEN ns_shared.NS4, THEN ns_shared.NS5], possibility)
    8.16 +	THEN ns_shared.NS4, THEN ns_shared.NS5])
    8.17 +apply (possibility, simp add: used_Cons) 
    8.18  done
    8.19  
    8.20  (*This version is similar, while instantiating ?K and ?N to epsilon-terms
     9.1 --- a/src/HOL/Auth/OtwayRees.thy	Tue Sep 23 15:40:27 2003 +0200
     9.2 +++ b/src/HOL/Auth/OtwayRees.thy	Tue Sep 23 15:41:33 2003 +0200
     9.3 @@ -89,16 +89,16 @@
     9.4  
     9.5  
     9.6  text{*A "possibility property": there are traces that reach the end*}
     9.7 -lemma "B \<noteq> Server
     9.8 -      ==> \<exists>K. \<exists>evs \<in> otway.
     9.9 +lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
    9.10 +      ==> \<exists>evs \<in> otway.
    9.11               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
    9.12                 \<in> set evs"
    9.13  apply (intro exI bexI)
    9.14  apply (rule_tac [2] otway.Nil
    9.15                      [THEN otway.OR1, THEN otway.Reception,
    9.16                       THEN otway.OR2, THEN otway.Reception,
    9.17 -                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], 
    9.18 -       possibility)
    9.19 +                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) 
    9.20 +apply (possibility, simp add: used_Cons) 
    9.21  done
    9.22  
    9.23  lemma Gets_imp_Says [dest!]:
    10.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Tue Sep 23 15:40:27 2003 +0200
    10.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Tue Sep 23 15:41:33 2003 +0200
    10.3 @@ -82,15 +82,16 @@
    10.4  
    10.5  
    10.6  (*A "possibility property": there are traces that reach the end*)
    10.7 -lemma "B \<noteq> Server
    10.8 -      ==> \<exists>K. \<exists>evs \<in> otway.
    10.9 +lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
   10.10 +      ==> \<exists>evs \<in> otway.
   10.11             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|})
   10.12               \<in> set evs"
   10.13  apply (intro exI bexI)
   10.14  apply (rule_tac [2] otway.Nil
   10.15                      [THEN otway.OR1, THEN otway.Reception,
   10.16                       THEN otway.OR2, THEN otway.Reception,
   10.17 -                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
   10.18 +                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
   10.19 +apply (possibility, simp add: used_Cons) 
   10.20  done
   10.21  
   10.22  lemma Gets_imp_Says [dest!]:
    11.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Tue Sep 23 15:40:27 2003 +0200
    11.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Tue Sep 23 15:41:33 2003 +0200
    11.3 @@ -90,15 +90,16 @@
    11.4  declare Fake_parts_insert_in_Un  [dest]
    11.5  
    11.6  (*A "possibility property": there are traces that reach the end*)
    11.7 -lemma "B \<noteq> Server
    11.8 -      ==> \<exists>K. \<exists>NA. \<exists>evs \<in> otway.
    11.9 +lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
   11.10 +      ==> \<exists>NA. \<exists>evs \<in> otway.
   11.11              Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
   11.12                \<in> set evs"
   11.13  apply (intro exI bexI)
   11.14  apply (rule_tac [2] otway.Nil
   11.15                      [THEN otway.OR1, THEN otway.Reception,
   11.16                       THEN otway.OR2, THEN otway.Reception,
   11.17 -                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
   11.18 +                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
   11.19 +apply (possibility, simp add: used_Cons) 
   11.20  done
   11.21  
   11.22  lemma Gets_imp_Says [dest!]:
    12.1 --- a/src/HOL/Auth/Public.thy	Tue Sep 23 15:40:27 2003 +0200
    12.2 +++ b/src/HOL/Auth/Public.thy	Tue Sep 23 15:41:33 2003 +0200
    12.3 @@ -400,7 +400,7 @@
    12.4         simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
    12.5         disj_comms 
    12.6         image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
    12.7 -       analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
    12.8 +       analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]
    12.9         insert_Key_singleton 
   12.10         Key_not_used insert_Key_image Un_assoc [THEN sym]
   12.11  
   12.12 @@ -412,19 +412,4 @@
   12.13  	       addsimps thms"analz_image_freshK_simps"
   12.14  *}
   12.15  
   12.16 -axioms
   12.17 -  Key_supply_ax:  "finite KK ==> \<exists>K\<in>symKeys. K \<notin> KK & Key K \<notin> used evs"
   12.18 -  --{*Unlike the corresponding property of nonces, this cannot be proved.
   12.19 -    We have infinitely many agents and there is nothing to stop their
   12.20 -    long-term keys from exhausting all the natural numbers.  The axiom
   12.21 -    assumes that their keys are dispersed so as to leave room for infinitely
   12.22 -    many fresh session keys.  We could, alternatively, restrict agents to
   12.23 -    an unspecified finite number.  We could however replace @{term"used evs"} 
   12.24 -    by @{term "used []"}.*}
   12.25 -
   12.26 -
   12.27 -lemma Key_supply1: "\<exists>K\<in>symKeys. Key K \<notin> used evs"
   12.28 -by (rule Finites.emptyI [THEN Key_supply_ax, THEN bexE], blast)
   12.29 -
   12.30 -
   12.31  end
    13.1 --- a/src/HOL/Auth/Recur.thy	Tue Sep 23 15:40:27 2003 +0200
    13.2 +++ b/src/HOL/Auth/Recur.thy	Tue Sep 23 15:41:33 2003 +0200
    13.3 @@ -117,37 +117,40 @@
    13.4  
    13.5  
    13.6  text{*Simplest case: Alice goes directly to the server*}
    13.7 -lemma "\<exists>K NA. \<exists>evs \<in> recur.
    13.8 -   Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
    13.9 -                   END|}  \<in> set evs"
   13.10 +lemma "Key K \<notin> used [] 
   13.11 +       ==> \<exists>NA. \<exists>evs \<in> recur.
   13.12 +              Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
   13.13 +                    END|}  \<in> set evs"
   13.14  apply (intro exI bexI)
   13.15  apply (rule_tac [2] recur.Nil [THEN recur.RA1, 
   13.16 -                             THEN recur.RA3 [OF _ _ respond.One]], possibility)
   13.17 +                             THEN recur.RA3 [OF _ _ respond.One]])
   13.18 +apply (possibility, simp add: used_Cons) 
   13.19  done
   13.20  
   13.21  
   13.22  text{*Case two: Alice, Bob and the server*}
   13.23 -lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
   13.24 +lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K' |]
   13.25 +       ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
   13.26          Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
   13.27                     END|}  \<in> set evs"
   13.28 -apply (cut_tac Nonce_supply2 Key_supply2, clarify)
   13.29 +apply (cut_tac Nonce_supply2, clarify)
   13.30  apply (intro exI bexI)
   13.31  apply (rule_tac [2] 
   13.32            recur.Nil [THEN recur.RA1, 
   13.33                       THEN recur.RA2,
   13.34                       THEN recur.RA3 [OF _ _ respond.One [THEN respond.Cons]],
   13.35                       THEN recur.RA4])
   13.36 -apply (tactic "basic_possibility_tac")
   13.37 -apply (tactic
   13.38 -      "DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
   13.39 +apply possibility
   13.40 +apply (auto simp add: used_Cons)
   13.41  done
   13.42  
   13.43 -(*Case three: Alice, Bob, Charlie and the server
   13.44 -  Rather slow (16 seconds) to run every time...
   13.45 -lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
   13.46 -        Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
   13.47 -                   END|}  \<in> set evs"
   13.48 -apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1", clarify)
   13.49 +(*Case three: Alice, Bob, Charlie and the server Rather slow (5 seconds)*)
   13.50 +lemma "[| Key K \<notin> used []; Key K' \<notin> used [];  
   13.51 +                       Key K'' \<notin> used []; K \<noteq> K'; K' \<noteq> K''; K \<noteq> K'' |]
   13.52 +       ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
   13.53 +             Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
   13.54 +                        END|}  \<in> set evs"
   13.55 +apply (cut_tac Nonce_supply3, clarify)
   13.56  apply (intro exI bexI)
   13.57  apply (rule_tac [2] 
   13.58            recur.Nil [THEN recur.RA1, 
   13.59 @@ -157,11 +160,8 @@
   13.60                                    [THEN respond.Cons, THEN respond.Cons]],
   13.61                       THEN recur.RA4, THEN recur.RA4])
   13.62  apply (tactic "basic_possibility_tac")
   13.63 -apply (tactic
   13.64 -      "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 ORELSE \
   13.65 -\                   eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
   13.66 +apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)")
   13.67  done
   13.68 -*)
   13.69  
   13.70  (**** Inductive proofs about recur ****)
   13.71  
    14.1 --- a/src/HOL/Auth/Shared.thy	Tue Sep 23 15:40:27 2003 +0200
    14.2 +++ b/src/HOL/Auth/Shared.thy	Tue Sep 23 15:41:33 2003 +0200
    14.3 @@ -51,10 +51,7 @@
    14.4  
    14.5  text{*Now cancel the @{text dest} attribute given to
    14.6   @{text analz.Decrypt} in its declaration.*}
    14.7 -ML
    14.8 -{*
    14.9 -Delrules [analz.Decrypt];
   14.10 -*}
   14.11 +declare analz.Decrypt [rule del]
   14.12  
   14.13  text{*Rewrites should not refer to  @{term "initState(Friend i)"} because
   14.14    that expression is not in normal form.*}
   14.15 @@ -137,7 +134,7 @@
   14.16  apply (cut_tac evs = evs in Nonce_supply_lemma)
   14.17  apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify)
   14.18  apply (rule_tac x = N in exI)
   14.19 -apply (rule_tac x = "Suc (N+Na) " in exI)
   14.20 +apply (rule_tac x = "Suc (N+Na)" in exI)
   14.21  apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
   14.22  done
   14.23  
   14.24 @@ -147,7 +144,7 @@
   14.25  apply (cut_tac evs = "evs'" in Nonce_supply_lemma)
   14.26  apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify)
   14.27  apply (rule_tac x = N in exI)
   14.28 -apply (rule_tac x = "Suc (N+Na) " in exI)
   14.29 +apply (rule_tac x = "Suc (N+Na)" in exI)
   14.30  apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI)
   14.31  apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
   14.32  done
   14.33 @@ -157,42 +154,12 @@
   14.34  apply (rule someI, blast)
   14.35  done
   14.36  
   14.37 -subsection{*Supply fresh keys for possibility theorems.*}
   14.38 -
   14.39 -axioms
   14.40 -  Key_supply_ax:  "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"
   14.41 -  --{*Unlike the corresponding property of nonces, this cannot be proved.
   14.42 +text{*Unlike the corresponding property of nonces, we cannot prove
   14.43 +    @{term "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"}.
   14.44      We have infinitely many agents and there is nothing to stop their
   14.45 -    long-term keys from exhausting all the natural numbers.  The axiom
   14.46 -    assumes that their keys are dispersed so as to leave room for infinitely
   14.47 -    many fresh session keys.  We could, alternatively, restrict agents to
   14.48 -    an unspecified finite number.  We could however replace @{term"used evs"} 
   14.49 -    by @{term "used []"}.*}
   14.50 -
   14.51 -lemma Key_supply1: "\<exists>K. Key K \<notin> used evs"
   14.52 -by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast)
   14.53 +    long-term keys from exhausting all the natural numbers.  Instead,
   14.54 +    possibility theorems must assume the existence of a few keys.*}
   14.55  
   14.56 -lemma Key_supply2: "\<exists>K K'. Key K \<notin> used evs & Key K' \<notin> used evs' & K \<noteq> K'"
   14.57 -apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
   14.58 -apply (erule exE)
   14.59 -apply (cut_tac evs="evs'" in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax], auto) 
   14.60 -done
   14.61 -
   14.62 -lemma Key_supply3: "\<exists>K K' K''. Key K \<notin> used evs & Key K' \<notin> used evs' &  
   14.63 -                       Key K'' \<notin> used evs'' & K \<noteq> K' & K' \<noteq> K'' & K \<noteq> K''"
   14.64 -apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
   14.65 -apply (erule exE)
   14.66 -(*Blast_tac requires instantiation of the keys for some reason*)
   14.67 -apply (cut_tac evs="evs'" and a1 = K in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax])
   14.68 -apply (erule exE)
   14.69 -apply (cut_tac evs = "evs''" and a1 = Ka and a2 = K 
   14.70 -       in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Key_supply_ax], blast)
   14.71 -done
   14.72 -
   14.73 -lemma Key_supply: "Key (@ K. Key K \<notin> used evs) \<notin> used evs"
   14.74 -apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE])
   14.75 -apply (rule someI, blast)
   14.76 -done
   14.77  
   14.78  subsection{*Tactics for possibility theorems*}
   14.79  
   14.80 @@ -200,8 +167,6 @@
   14.81  {*
   14.82  val inj_shrK      = thm "inj_shrK";
   14.83  val isSym_keys    = thm "isSym_keys";
   14.84 -val Key_supply_ax = thm "Key_supply_ax";
   14.85 -val Key_supply = thm "Key_supply";
   14.86  val Nonce_supply = thm "Nonce_supply";
   14.87  val invKey_K = thm "invKey_K";
   14.88  val analz_Decrypt' = thm "analz_Decrypt'";
   14.89 @@ -221,10 +186,6 @@
   14.90  val Nonce_supply2 = thm "Nonce_supply2";
   14.91  val Nonce_supply3 = thm "Nonce_supply3";
   14.92  val Nonce_supply = thm "Nonce_supply";
   14.93 -val Key_supply1 = thm "Key_supply1";
   14.94 -val Key_supply2 = thm "Key_supply2";
   14.95 -val Key_supply3 = thm "Key_supply3";
   14.96 -val Key_supply = thm "Key_supply";
   14.97  *}
   14.98  
   14.99  
  14.100 @@ -238,7 +199,7 @@
  14.101                           setSolver safe_solver))
  14.102       THEN
  14.103       REPEAT_FIRST (eq_assume_tac ORELSE' 
  14.104 -                   resolve_tac [refl, conjI, Nonce_supply, Key_supply])))
  14.105 +                   resolve_tac [refl, conjI, Nonce_supply])))
  14.106  
  14.107  (*Tactic for possibility theorems (ML script version)*)
  14.108  fun possibility_tac state = gen_possibility_tac (simpset()) state
    15.1 --- a/src/HOL/Auth/Yahalom.thy	Tue Sep 23 15:40:27 2003 +0200
    15.2 +++ b/src/HOL/Auth/Yahalom.thy	Tue Sep 23 15:41:33 2003 +0200
    15.3 @@ -88,15 +88,16 @@
    15.4  declare analz_into_parts [dest]
    15.5  
    15.6  (*A "possibility property": there are traces that reach the end*)
    15.7 -lemma "A \<noteq> Server  
    15.8 -      ==> \<exists>X NB K. \<exists>evs \<in> yahalom.           
    15.9 +lemma "[| A \<noteq> Server; Key K \<notin> used [] |] 
   15.10 +      ==> \<exists>X NB. \<exists>evs \<in> yahalom.           
   15.11               Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   15.12  apply (intro exI bexI)
   15.13  apply (rule_tac [2] yahalom.Nil
   15.14                      [THEN yahalom.YM1, THEN yahalom.Reception, 
   15.15                       THEN yahalom.YM2, THEN yahalom.Reception, 
   15.16                       THEN yahalom.YM3, THEN yahalom.Reception, 
   15.17 -                     THEN yahalom.YM4], possibility)
   15.18 +                     THEN yahalom.YM4])
   15.19 +apply (possibility, simp add: used_Cons) 
   15.20  done
   15.21  
   15.22  lemma Gets_imp_Says:
    16.1 --- a/src/HOL/Auth/Yahalom2.thy	Tue Sep 23 15:40:27 2003 +0200
    16.2 +++ b/src/HOL/Auth/Yahalom2.thy	Tue Sep 23 15:41:33 2003 +0200
    16.3 @@ -80,14 +80,16 @@
    16.4  declare analz_into_parts [dest]
    16.5  
    16.6  text{*A "possibility property": there are traces that reach the end*}
    16.7 -lemma "\<exists>X NB K. \<exists>evs \<in> yahalom.
    16.8 +lemma "Key K \<notin> used []
    16.9 +       ==> \<exists>X NB. \<exists>evs \<in> yahalom.
   16.10               Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   16.11  apply (intro exI bexI)
   16.12  apply (rule_tac [2] yahalom.Nil
   16.13                      [THEN yahalom.YM1, THEN yahalom.Reception,
   16.14                       THEN yahalom.YM2, THEN yahalom.Reception,
   16.15                       THEN yahalom.YM3, THEN yahalom.Reception,
   16.16 -                     THEN yahalom.YM4], possibility)
   16.17 +                     THEN yahalom.YM4])
   16.18 +apply (possibility, simp add: used_Cons) 
   16.19  done
   16.20  
   16.21  lemma Gets_imp_Says:
    17.1 --- a/src/HOL/Auth/Yahalom_Bad.thy	Tue Sep 23 15:40:27 2003 +0200
    17.2 +++ b/src/HOL/Auth/Yahalom_Bad.thy	Tue Sep 23 15:41:33 2003 +0200
    17.3 @@ -70,15 +70,16 @@
    17.4  
    17.5  
    17.6  (*A "possibility property": there are traces that reach the end*)
    17.7 -lemma "A \<noteq> Server
    17.8 -      ==> \<exists>X NB K. \<exists>evs \<in> yahalom.
    17.9 -             Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   17.10 +lemma "[| A \<noteq> Server; Key K \<notin> used [] |] 
   17.11 +       ==> \<exists>X NB. \<exists>evs \<in> yahalom.
   17.12 +              Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   17.13  apply (intro exI bexI)
   17.14  apply (rule_tac [2] yahalom.Nil
   17.15                      [THEN yahalom.YM1, THEN yahalom.Reception,
   17.16                       THEN yahalom.YM2, THEN yahalom.Reception,
   17.17                       THEN yahalom.YM3, THEN yahalom.Reception,
   17.18 -                     THEN yahalom.YM4], possibility)
   17.19 +                     THEN yahalom.YM4])
   17.20 +apply (possibility, simp add: used_Cons) 
   17.21  done
   17.22  
   17.23  lemma Gets_imp_Says: