Removal of the Key_supply axiom (affects many possbility proofs) and minor
changes
--- a/src/HOL/Auth/CertifiedEmail.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy Tue Sep 23 15:41:33 2003 +0200
@@ -93,14 +93,15 @@
declare analz_into_parts [dest]
(*A "possibility property": there are traces that reach the end*)
-lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
+lemma "[| Key K \<notin> used []; K \<in> symKeys |] ==>
+ \<exists>S2TTP. \<exists>evs \<in> certified_mail.
Says TTP S (Crypt (priSK TTP) S2TTP) \<in> set evs"
-apply (rule bexE [OF Key_supply1])
apply (intro exI bexI)
apply (rule_tac [2] certified_mail.Nil
[THEN certified_mail.CM1, THEN certified_mail.Reception,
THEN certified_mail.CM2,
- THEN certified_mail.CM3], possibility, possibility, auto)
+ THEN certified_mail.CM3])
+apply (possibility, auto)
done
--- a/src/HOL/Auth/Event.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/Event.thy Tue Sep 23 15:41:33 2003 +0200
@@ -35,13 +35,10 @@
text{*Spy has access to his own key for spoof messages, but Server is secure*}
specification (bad)
- bad_properties: "Spy \<in> bad & Server \<notin> bad"
+ Spy_in_bad [iff]: "Spy \<in> bad"
+ Server_not_bad [iff]: "Server \<notin> bad"
by (rule exI [of _ "{Spy}"], simp)
-lemmas Spy_in_bad = bad_properties [THEN conjunct1, iff]
-lemmas Server_not_bad = bad_properties [THEN conjunct2, iff]
-
-
primrec
knows_Nil: "knows A [] = initState A"
knows_Cons:
@@ -111,8 +108,8 @@
"knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
by simp
-text{*The point of letting the Spy see "bad" agents' notes is to prevent
- redundant case-splits on whether A=Spy and whether A:bad*}
+text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits
+ on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*}
lemma knows_Spy_Notes [simp]:
"knows Spy (Notes A X # evs) =
(if A:bad then insert X (knows Spy evs) else knows Spy evs)"
--- a/src/HOL/Auth/KerberosIV.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/KerberosIV.thy Tue Sep 23 15:41:33 2003 +0200
@@ -242,9 +242,10 @@
(*---------------------------------------------------------------------*)
-declare Says_imp_knows_Spy [THEN parts.Inj, dest] parts.Body [dest]
-declare analz_subset_parts [THEN subsetD, dest]
-declare Fake_parts_insert [THEN subsetD, dest]
+declare Says_imp_knows_Spy [THEN parts.Inj, dest]
+declare parts.Body [dest]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
subsection{*Lemmas about Lists*}
@@ -294,31 +295,27 @@
ev \<noteq> Says Kas A (Crypt (shrK A) {|akey, Agent Peer, Tk,
(Crypt (shrK Peer) {|Agent A, Agent Peer, akey, Tk|})|}))
==> AuthKeys (ev # evs) = AuthKeys evs"
-apply (unfold AuthKeys_def, auto)
-done
+by (unfold AuthKeys_def, auto)
lemma AuthKeys_insert:
"AuthKeys
(Says Kas A (Crypt (shrK A) {|Key K, Agent Peer, Number Tk,
(Crypt (shrK Peer) {|Agent A, Agent Peer, Key K, Number Tk|})|}) # evs)
= insert K (AuthKeys evs)"
-apply (unfold AuthKeys_def, auto)
-done
+by (unfold AuthKeys_def, auto)
lemma AuthKeys_simp:
"K \<in> AuthKeys
(Says Kas A (Crypt (shrK A) {|Key K', Agent Peer, Number Tk,
(Crypt (shrK Peer) {|Agent A, Agent Peer, Key K', Number Tk|})|}) # evs)
==> K = K' | K \<in> AuthKeys evs"
-apply (unfold AuthKeys_def, auto)
-done
+by (unfold AuthKeys_def, auto)
lemma AuthKeysI:
"Says Kas A (Crypt (shrK A) {|Key K, Agent Tgs, Number Tk,
(Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key K, Number Tk|})|}) \<in> set evs
==> K \<in> AuthKeys evs"
-apply (unfold AuthKeys_def, auto)
-done
+by (unfold AuthKeys_def, auto)
lemma AuthKeys_used: "K \<in> AuthKeys evs ==> Key K \<in> used evs"
by (simp add: AuthKeys_def, blast)
@@ -344,8 +341,7 @@
lemma K5_msg_in_parts_spies:
"Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})
\<in> set evs ==> ServTicket \<in> parts (spies evs)"
-apply blast
-done
+by blast
lemma Oops_range_spies2:
"[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
@@ -358,8 +354,7 @@
lemma Says_ticket_in_parts_spies:
"Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \<in> set evs
==> Ticket \<in> parts (spies evs)"
-apply blast
-done
+by blast
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
@@ -980,8 +975,7 @@
~ ExpirAuth Tk evs;
A \<notin> bad; evs \<in> kerberos |]
==> Key AuthKey \<notin> analz (spies evs)"
-apply (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
-done
+by (blast dest: Says_Kas_message_form Confidentiality_Kas_lemma)
subsection{* Guarantees for Tgs *}
@@ -1261,8 +1255,8 @@
~ ExpirAuth Tk evs; A \<notin> bad; evs \<in> kerberos |]
==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
\<in> set evs"
-apply (blast dest: A_trusts_AuthKey Confidentiality_Auth_A A_trusts_K4_bis)
-done
+by (blast dest: A_trusts_AuthKey Confidentiality_Auth_A A_trusts_K4_bis)
+
text{*Note: requires a temporal check*}
@@ -1422,8 +1416,7 @@
~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;
A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
-apply (blast dest!: Confidentiality_B B_Knows_B_Knows_ServKey_lemma)
-done
+by (blast dest!: Confidentiality_B B_Knows_B_Knows_ServKey_lemma)
lemma B_Knows_B_Knows_ServKey_refined:
"[| Says B A (Crypt ServKey (Number Ta)) \<in> set evs;
@@ -1432,9 +1425,7 @@
~ ExpirServ Tt evs;
A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
-apply (blast dest!: Confidentiality_B_refined B_Knows_B_Knows_ServKey_lemma)
-done
-
+by (blast dest!: Confidentiality_B_refined B_Knows_B_Knows_ServKey_lemma)
lemma A_Knows_B_Knows_ServKey:
"[| Crypt ServKey (Number Ta) \<in> parts (spies evs);
@@ -1445,8 +1436,7 @@
~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;
A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
==> B Issues A with (Crypt ServKey (Number Ta)) on evs"
-apply (blast dest!: B_Authenticity Confidentiality_Serv_A B_Knows_B_Knows_ServKey_lemma)
-done
+by (blast dest!: B_Authenticity Confidentiality_Serv_A B_Knows_B_Knows_ServKey_lemma)
lemma K3_imp_K2:
"[| Says A Tgs
@@ -1525,8 +1515,7 @@
~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;
B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerberos |]
==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs"
-apply (blast dest!: Confidentiality_Serv_A A_Knows_A_Knows_ServKey_lemma)
-done
+by (blast dest!: Confidentiality_Serv_A A_Knows_A_Knows_ServKey_lemma)
lemma B_Knows_A_Knows_ServKey:
"[| Crypt ServKey {|Agent A, Number Ta|} \<in> parts (spies evs);
@@ -1539,8 +1528,7 @@
~ ExpirServ Tt evs; ~ ExpirAuth Tk evs;
B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerberos |]
==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs"
-apply (blast dest: A_Authenticity Confidentiality_B A_Knows_A_Knows_ServKey_lemma)
-done
+by (blast dest: A_Authenticity Confidentiality_B A_Knows_A_Knows_ServKey_lemma)
lemma B_Knows_A_Knows_ServKey_refined:
@@ -1550,7 +1538,6 @@
~ ExpirServ Tt evs;
B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerberos |]
==> A Issues B with (Crypt ServKey {|Agent A, Number Ta|}) on evs"
-apply (blast dest: A_Authenticity_refined Confidentiality_B_refined A_Knows_A_Knows_ServKey_lemma)
-done
+by (blast dest: A_Authenticity_refined Confidentiality_B_refined A_Knows_A_Knows_ServKey_lemma)
end
--- a/src/HOL/Auth/Kerberos_BAN.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Tue Sep 23 15:41:33 2003 +0200
@@ -100,20 +100,22 @@
==> Notes Spy {|Number Ts, Key K|} # evso \<in> kerberos_ban"
-declare Says_imp_knows_Spy [THEN parts.Inj, dest] parts.Body [dest]
-declare analz_subset_parts [THEN subsetD, dest]
-declare Fake_parts_insert [THEN subsetD, dest]
+declare Says_imp_knows_Spy [THEN parts.Inj, dest]
+declare parts.Body [dest]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
(*A "possibility property": there are traces that reach the end.*)
-lemma "\<exists>Timestamp K. \<exists>evs \<in> kerberos_ban.
+lemma "Key K \<notin> used []
+ ==> \<exists>Timestamp. \<exists>evs \<in> kerberos_ban.
Says B A (Crypt K (Number Timestamp))
\<in> set evs"
apply (cut_tac SesKeyLife_LB)
apply (intro exI bexI)
apply (rule_tac [2]
kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2,
- THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4], possibility)
-apply (simp_all (no_asm_simp))
+ THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4])
+apply (possibility, simp_all (no_asm_simp) add: used_Cons)
done
--- a/src/HOL/Auth/Message.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/Message.thy Tue Sep 23 15:41:33 2003 +0200
@@ -39,13 +39,13 @@
agent = Server | Friend nat | Spy
datatype
- msg = Agent agent (*Agent names*)
- | Number nat (*Ordinary integers, timestamps, ...*)
- | Nonce nat (*Unguessable nonces*)
- | Key key (*Crypto keys*)
- | Hash msg (*Hashing*)
- | MPair msg msg (*Compound messages*)
- | Crypt key msg (*Encryption, public- or shared-key*)
+ msg = Agent agent --{*Agent names*}
+ | Number nat --{*Ordinary integers, timestamps, ...*}
+ | Nonce nat --{*Unguessable nonces*}
+ | Key key --{*Crypto keys*}
+ | Hash msg --{*Hashing*}
+ | MPair msg msg --{*Compound messages*}
+ | Crypt key msg --{*Encryption, public- or shared-key*}
(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
@@ -69,7 +69,7 @@
keysFor :: "msg set => key set"
"keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
-(** Inductive definition of all "parts" of a message. **)
+subsubsection{*Inductive definition of all "parts" of a message. *}
consts parts :: "msg set => msg set"
inductive "parts H"
@@ -81,7 +81,7 @@
(*Monotonicity*)
-lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
+lemma parts_mono: "G\<subseteq>H ==> parts(G) \<subseteq> parts(H)"
apply auto
apply (erule parts.induct)
apply (auto dest: Fst Snd Body)
@@ -99,7 +99,7 @@
by auto
-(** Inverse of keys **)
+subsubsection{*Inverse of keys *}
lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
apply safe
@@ -142,8 +142,7 @@
lemma keysFor_insert_Crypt [simp]:
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
-apply (unfold keysFor_def, auto)
-done
+by (unfold keysFor_def, auto)
lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
by (unfold keysFor_def, auto)
@@ -183,7 +182,7 @@
by (erule parts.induct, blast+)
-(** Unions **)
+subsubsection{*Unions *}
lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)"
by (intro Un_least parts_mono Un_upper1 Un_upper2)
@@ -203,7 +202,8 @@
(*TWO inserts to avoid looping. This rewrite is better than nothing.
Not suitable for Addsimps: its behaviour can be strange.*)
-lemma parts_insert2: "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
+lemma parts_insert2:
+ "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
apply (simp add: Un_assoc)
apply (simp add: parts_insert [symmetric])
done
@@ -231,7 +231,7 @@
lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
by (blast intro: parts_mono [THEN [2] rev_subsetD])
-(** Idempotence and transitivity **)
+subsubsection{*Idempotence and transitivity *}
lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
by (erule parts.induct, blast+)
@@ -243,46 +243,51 @@
by (drule parts_mono, blast)
(*Cut*)
-lemma parts_cut: "[| Y\<in> parts (insert X G); X\<in> parts H |]
- ==> Y\<in> parts (G \<union> H)"
-apply (erule parts_trans, auto)
-done
+lemma parts_cut:
+ "[| Y\<in> parts (insert X G); X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
+by (erule parts_trans, auto)
lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
by (force dest!: parts_cut intro: parts_insertI)
-(** Rewrite rules for pulling out atomic messages **)
+subsubsection{*Rewrite rules for pulling out atomic messages *}
lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
-lemma parts_insert_Agent [simp]: "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
+lemma parts_insert_Agent [simp]:
+ "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"
apply (rule parts_insert_eq_I)
apply (erule parts.induct, auto)
done
-lemma parts_insert_Nonce [simp]: "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
+lemma parts_insert_Nonce [simp]:
+ "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"
apply (rule parts_insert_eq_I)
apply (erule parts.induct, auto)
done
-lemma parts_insert_Number [simp]: "parts (insert (Number N) H) = insert (Number N) (parts H)"
+lemma parts_insert_Number [simp]:
+ "parts (insert (Number N) H) = insert (Number N) (parts H)"
apply (rule parts_insert_eq_I)
apply (erule parts.induct, auto)
done
-lemma parts_insert_Key [simp]: "parts (insert (Key K) H) = insert (Key K) (parts H)"
+lemma parts_insert_Key [simp]:
+ "parts (insert (Key K) H) = insert (Key K) (parts H)"
apply (rule parts_insert_eq_I)
apply (erule parts.induct, auto)
done
-lemma parts_insert_Hash [simp]: "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
+lemma parts_insert_Hash [simp]:
+ "parts (insert (Hash X) H) = insert (Hash X) (parts H)"
apply (rule parts_insert_eq_I)
apply (erule parts.induct, auto)
done
-lemma parts_insert_Crypt [simp]: "parts (insert (Crypt K X) H) =
+lemma parts_insert_Crypt [simp]:
+ "parts (insert (Crypt K X) H) =
insert (Crypt K X) (parts (insert X H))"
apply (rule equalityI)
apply (rule subsetI)
@@ -291,7 +296,8 @@
apply (blast intro: parts.Body)+
done
-lemma parts_insert_MPair [simp]: "parts (insert {|X,Y|} H) =
+lemma parts_insert_MPair [simp]:
+ "parts (insert {|X,Y|} H) =
insert {|X,Y|} (parts (insert X (insert Y H)))"
apply (rule equalityI)
apply (rule subsetI)
@@ -320,9 +326,9 @@
subsection{*Inductive relation "analz"*}
-(** Inductive definition of "analz" -- what can be broken down from a set of
+text{*Inductive definition of "analz" -- what can be broken down from a set of
messages, including keys. A form of downward closure. Pairs can
- be taken apart; messages decrypted with known keys. **)
+ be taken apart; messages decrypted with known keys. *}
consts analz :: "msg set => msg set"
inductive "analz H"
@@ -335,7 +341,7 @@
(*Monotonicity; Lemma 1 of Lowe's paper*)
-lemma analz_mono: "G<=H ==> analz(G) <= analz(H)"
+lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
apply auto
apply (erule analz.induct)
apply (auto dest: Fst Snd)
@@ -356,6 +362,8 @@
apply (erule analz.induct, blast+)
done
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+
lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
@@ -372,7 +380,7 @@
lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
-(** General equational properties **)
+subsubsection{*General equational properties *}
lemma analz_empty [simp]: "analz{} = {}"
apply safe
@@ -387,26 +395,30 @@
lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)"
by (blast intro: analz_mono [THEN [2] rev_subsetD])
-(** Rewrite rules for pulling out atomic messages **)
+subsubsection{*Rewrite rules for pulling out atomic messages *}
lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert]
-lemma analz_insert_Agent [simp]: "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
+lemma analz_insert_Agent [simp]:
+ "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
-lemma analz_insert_Nonce [simp]: "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
+lemma analz_insert_Nonce [simp]:
+ "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
-lemma analz_insert_Number [simp]: "analz (insert (Number N) H) = insert (Number N) (analz H)"
+lemma analz_insert_Number [simp]:
+ "analz (insert (Number N) H) = insert (Number N) (analz H)"
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
-lemma analz_insert_Hash [simp]: "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
+lemma analz_insert_Hash [simp]:
+ "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
@@ -420,7 +432,8 @@
apply (erule analz.induct, auto)
done
-lemma analz_insert_MPair [simp]: "analz (insert {|X,Y|} H) =
+lemma analz_insert_MPair [simp]:
+ "analz (insert {|X,Y|} H) =
insert {|X,Y|} (analz (insert X (insert Y H)))"
apply (rule equalityI)
apply (rule subsetI)
@@ -453,7 +466,8 @@
apply (blast intro: analz_insertI analz.Decrypt)
done
-lemma analz_insert_Decrypt: "Key (invKey K) \<in> analz H ==>
+lemma analz_insert_Decrypt:
+ "Key (invKey K) \<in> analz H ==>
analz (insert (Crypt K X) H) =
insert (Crypt K X) (analz (insert X H))"
by (intro equalityI lemma1 lemma2)
@@ -471,7 +485,8 @@
(*This rule supposes "for the sake of argument" that we have the key.*)
-lemma analz_insert_Crypt_subset: "analz (insert (Crypt K X) H) \<subseteq>
+lemma analz_insert_Crypt_subset:
+ "analz (insert (Crypt K X) H) \<subseteq>
insert (Crypt K X) (analz (insert X H))"
apply (rule subsetI)
apply (erule analz.induct, auto)
@@ -484,7 +499,7 @@
done
-(** Idempotence and transitivity **)
+subsubsection{*Idempotence and transitivity *}
lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
by (erule analz.induct, blast+)
@@ -510,32 +525,35 @@
by (blast intro: analz_cut analz_insertI)
-(** A congruence rule for "analz" **)
+text{*A congruence rule for "analz" *}
-lemma analz_subset_cong: "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'
+lemma analz_subset_cong:
+ "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H'
|] ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
apply clarify
apply (erule analz.induct)
apply (best intro: analz_mono [THEN subsetD])+
done
-lemma analz_cong: "[| analz G = analz G'; analz H = analz H'
+lemma analz_cong:
+ "[| analz G = analz G'; analz H = analz H'
|] ==> analz (G \<union> H) = analz (G' \<union> H')"
-apply (intro equalityI analz_subset_cong, simp_all)
-done
+by (intro equalityI analz_subset_cong, simp_all)
-
-lemma analz_insert_cong: "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
+lemma analz_insert_cong:
+ "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
by (force simp only: insert_def intro!: analz_cong)
(*If there are no pairs or encryptions then analz does nothing*)
-lemma analz_trivial: "[| \<forall>X Y. {|X,Y|} \<notin> H; \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
+lemma analz_trivial:
+ "[| \<forall>X Y. {|X,Y|} \<notin> H; \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
apply safe
apply (erule analz.induct, blast+)
done
(*These two are obsolete (with a single Spy) but cost little to prove...*)
-lemma analz_UN_analz_lemma: "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
+lemma analz_UN_analz_lemma:
+ "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
apply (erule analz.induct)
apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
done
@@ -546,10 +564,10 @@
subsection{*Inductive relation "synth"*}
-(** Inductive definition of "synth" -- what can be built up from a set of
+text{*Inductive definition of "synth" -- what can be built up from a set of
messages. A form of upward closure. Pairs can be built, messages
encrypted with known keys. Agent names are public domain.
- Numbers can be guessed, but Nonces cannot be. **)
+ Numbers can be guessed, but Nonces cannot be. *}
consts synth :: "msg set => msg set"
inductive "synth H"
@@ -562,7 +580,7 @@
Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
(*Monotonicity*)
-lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
+lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
apply auto
apply (erule synth.induct)
apply (auto dest: Fst Snd Body)
@@ -579,7 +597,7 @@
lemma synth_increasing: "H \<subseteq> synth(H)"
by blast
-(** Unions **)
+subsubsection{*Unions *}
(*Converse fails: we can synth more from the union than from the
separate parts, building a compound message using elements of each.*)
@@ -589,7 +607,7 @@
lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
by (blast intro: synth_mono [THEN [2] rev_subsetD])
-(** Idempotence and transitivity **)
+subsubsection{*Idempotence and transitivity *}
lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
by (erule synth.induct, blast+)
@@ -616,17 +634,17 @@
lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)"
by blast
-lemma Crypt_synth_eq [simp]: "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
+lemma Crypt_synth_eq [simp]:
+ "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
by blast
lemma keysFor_synth [simp]:
"keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
-apply (unfold keysFor_def, blast)
-done
+by (unfold keysFor_def, blast)
-(*** Combinations of parts, analz and synth ***)
+subsubsection{*Combinations of parts, analz and synth *}
lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
apply (rule equalityI)
@@ -655,22 +673,29 @@
done
-(** For reasoning about the Fake rule in traces **)
+subsubsection{*For reasoning about the Fake rule in traces *}
lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
(*More specifically for Fake. Very occasionally we could do with a version
of the form parts{X} \<subseteq> synth (analz H) \<union> parts H *)
-lemma Fake_parts_insert: "X \<in> synth (analz H) ==>
+lemma Fake_parts_insert:
+ "X \<in> synth (analz H) ==>
parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
apply (drule parts_insert_subset_Un)
apply (simp (no_asm_use))
apply blast
done
+lemma Fake_parts_insert_in_Un:
+ "[|Z \<in> parts (insert X H); X: synth (analz H)|]
+ ==> Z \<in> synth (analz H) \<union> parts H";
+by (blast dest: Fake_parts_insert [THEN subsetD, dest])
+
(*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*)
-lemma Fake_analz_insert: "X\<in> synth (analz G) ==>
+lemma Fake_analz_insert:
+ "X\<in> synth (analz G) ==>
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
apply (rule subsetI)
apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
@@ -679,10 +704,12 @@
apply blast
done
-lemma analz_conj_parts [simp]: "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
+lemma analz_conj_parts [simp]:
+ "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
by (blast intro: analz_subset_parts [THEN subsetD])
-lemma analz_disj_parts [simp]: "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
+lemma analz_disj_parts [simp]:
+ "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
by (blast intro: analz_subset_parts [THEN subsetD])
(*Without this equation, other rules for synth and analz would yield
@@ -692,19 +719,21 @@
(X \<in> synth (analz H) & Y \<in> synth (analz H))"
by blast
-lemma Crypt_synth_analz: "[| Key K \<in> analz H; Key (invKey K) \<in> analz H |]
+lemma Crypt_synth_analz:
+ "[| Key K \<in> analz H; Key (invKey K) \<in> analz H |]
==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))"
by blast
-lemma Hash_synth_analz [simp]: "X \<notin> synth (analz H)
+lemma Hash_synth_analz [simp]:
+ "X \<notin> synth (analz H)
==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
by blast
subsection{*HPair: a combination of Hash and MPair*}
-(*** Freeness ***)
+subsubsection{*Freeness *}
lemma Agent_neq_HPair: "Agent A ~= Hash[X] Y"
by (unfold HPair_def, simp)
@@ -733,14 +762,16 @@
lemma HPair_eq [iff]: "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"
by (simp add: HPair_def)
-lemma MPair_eq_HPair [iff]: "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
+lemma MPair_eq_HPair [iff]:
+ "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"
by (simp add: HPair_def)
-lemma HPair_eq_MPair [iff]: "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
+lemma HPair_eq_MPair [iff]:
+ "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"
by (auto simp add: HPair_def)
-(*** Specialized laws, proved in terms of those for Hash and MPair ***)
+subsubsection{*Specialized laws, proved in terms of those for Hash and MPair *}
lemma keysFor_insert_HPair [simp]: "keysFor (insert (Hash[X] Y) H) = keysFor H"
by (simp add: HPair_def)
@@ -766,37 +797,10 @@
declare parts.Body [rule del]
+text{*Rewrites to push in Key and Crypt messages, so that other messages can
+ be pulled out using the @{text analz_insert} rules*}
ML
{*
-(*ML bindings for definitions*)
-
-val invKey = thm "invKey"
-val keysFor_def = thm "keysFor_def"
-val HPair_def = thm "HPair_def"
-val symKeys_def = thm "symKeys_def"
-
-structure parts =
- struct
- val induct = thm "parts.induct"
- val Inj = thm "parts.Inj"
- val Fst = thm "parts.Fst"
- val Snd = thm "parts.Snd"
- val Body = thm "parts.Body"
- end
-
-structure analz =
- struct
- val induct = thm "analz.induct"
- val Inj = thm "analz.Inj"
- val Fst = thm "analz.Fst"
- val Snd = thm "analz.Snd"
- val Decrypt = thm "analz.Decrypt"
- end
-
-
-(** Rewrites to push in Key and Crypt messages, so that other messages can
- be pulled out using the analz_insert rules **)
-
fun insComm x y = inst "x" x (inst "y" y insert_commute);
bind_thms ("pushKeys",
@@ -818,79 +822,19 @@
subsection{*Tactics useful for many protocol proofs*}
ML
{*
+val invKey = thm "invKey"
+val keysFor_def = thm "keysFor_def"
+val HPair_def = thm "HPair_def"
+val symKeys_def = thm "symKeys_def"
val parts_mono = thm "parts_mono";
val analz_mono = thm "analz_mono";
-val Key_image_eq = thm "Key_image_eq";
-val Nonce_Key_image_eq = thm "Nonce_Key_image_eq";
-val keysFor_Un = thm "keysFor_Un";
-val keysFor_mono = thm "keysFor_mono";
-val keysFor_image_Key = thm "keysFor_image_Key";
-val Crypt_imp_invKey_keysFor = thm "Crypt_imp_invKey_keysFor";
-val MPair_parts = thm "MPair_parts";
-val parts_increasing = thm "parts_increasing";
-val parts_insertI = thm "parts_insertI";
-val parts_empty = thm "parts_empty";
-val parts_emptyE = thm "parts_emptyE";
-val parts_singleton = thm "parts_singleton";
-val parts_Un_subset1 = thm "parts_Un_subset1";
-val parts_Un_subset2 = thm "parts_Un_subset2";
-val parts_insert = thm "parts_insert";
-val parts_insert2 = thm "parts_insert2";
-val parts_UN_subset1 = thm "parts_UN_subset1";
-val parts_UN_subset2 = thm "parts_UN_subset2";
-val parts_UN = thm "parts_UN";
-val parts_insert_subset = thm "parts_insert_subset";
-val parts_partsD = thm "parts_partsD";
-val parts_trans = thm "parts_trans";
-val parts_cut = thm "parts_cut";
-val parts_cut_eq = thm "parts_cut_eq";
-val parts_insert_eq_I = thm "parts_insert_eq_I";
-val parts_image_Key = thm "parts_image_Key";
-val MPair_analz = thm "MPair_analz";
+val synth_mono = thm "synth_mono";
val analz_increasing = thm "analz_increasing";
+
+val analz_insertI = thm "analz_insertI";
val analz_subset_parts = thm "analz_subset_parts";
-val not_parts_not_analz = thm "not_parts_not_analz";
-val parts_analz = thm "parts_analz";
-val analz_parts = thm "analz_parts";
-val analz_insertI = thm "analz_insertI";
-val analz_empty = thm "analz_empty";
-val analz_Un = thm "analz_Un";
-val analz_insert_Crypt_subset = thm "analz_insert_Crypt_subset";
-val analz_image_Key = thm "analz_image_Key";
-val analz_analzD = thm "analz_analzD";
-val analz_trans = thm "analz_trans";
-val analz_cut = thm "analz_cut";
-val analz_insert_eq = thm "analz_insert_eq";
-val analz_subset_cong = thm "analz_subset_cong";
-val analz_cong = thm "analz_cong";
-val analz_insert_cong = thm "analz_insert_cong";
-val analz_trivial = thm "analz_trivial";
-val analz_UN_analz = thm "analz_UN_analz";
-val synth_mono = thm "synth_mono";
-val synth_increasing = thm "synth_increasing";
-val synth_Un = thm "synth_Un";
-val synth_insert = thm "synth_insert";
-val synth_synthD = thm "synth_synthD";
-val synth_trans = thm "synth_trans";
-val synth_cut = thm "synth_cut";
-val Agent_synth = thm "Agent_synth";
-val Number_synth = thm "Number_synth";
-val Nonce_synth_eq = thm "Nonce_synth_eq";
-val Key_synth_eq = thm "Key_synth_eq";
-val Crypt_synth_eq = thm "Crypt_synth_eq";
-val keysFor_synth = thm "keysFor_synth";
-val parts_synth = thm "parts_synth";
-val analz_analz_Un = thm "analz_analz_Un";
-val analz_synth_Un = thm "analz_synth_Un";
-val analz_synth = thm "analz_synth";
-val parts_insert_subset_Un = thm "parts_insert_subset_Un";
val Fake_parts_insert = thm "Fake_parts_insert";
val Fake_analz_insert = thm "Fake_analz_insert";
-val analz_conj_parts = thm "analz_conj_parts";
-val analz_disj_parts = thm "analz_disj_parts";
-val MPair_synth_analz = thm "MPair_synth_analz";
-val Crypt_synth_analz = thm "Crypt_synth_analz";
-val Hash_synth_analz = thm "Hash_synth_analz";
val pushes = thms "pushes";
@@ -952,7 +896,7 @@
lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A"
by auto
-lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))"
+lemma synth_analz_mono: "G\<subseteq>H ==> synth (analz(G)) \<subseteq> synth (analz(H))"
by (simp add: synth_mono analz_mono)
lemma Fake_analz_eq [simp]:
@@ -964,14 +908,6 @@
apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD])
done
-
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
-
-lemma Fake_parts_insert_in_Un:
- "[|Z \<in> parts (insert X H); X: synth (analz H)|]
- ==> Z \<in> synth (analz H) \<union> parts H";
-by (blast dest: Fake_parts_insert [THEN subsetD, dest])
-
text{*Two generalizations of @{text analz_insert_eq}*}
lemma gen_analz_insert_eq [rule_format]:
"X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
--- a/src/HOL/Auth/NS_Public.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/NS_Public.thy Tue Sep 23 15:41:33 2003 +0200
@@ -43,8 +43,9 @@
\<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
declare knows_Spy_partsEs [elim]
-declare analz_subset_parts [THEN subsetD, dest]
-declare Fake_parts_insert [THEN subsetD, dest]
+declare knows_Spy_partsEs [elim]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
(*A "possibility property": there are traces that reach the end*)
@@ -55,9 +56,6 @@
apply possibility
done
-
-(**** Inductive proofs about ns_public ****)
-
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
sends messages containing X! **)
@@ -70,8 +68,7 @@
"evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
-
-(*** Authenticity properties obtained from NS2 ***)
+subsection{*Authenticity properties obtained from NS2*}
(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
@@ -143,8 +140,7 @@
done
-
-(*** Authenticity properties obtained from NS2 ***)
+subsection{*Authenticity properties obtained from NS2*}
(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B
[unicity of B makes Lowe's fix work]
@@ -189,8 +185,7 @@
\<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
by (blast intro: B_trusts_NS3_lemma)
-(*** Overall guarantee for B ***)
-
+subsection{*Overall guarantee for B*}
(*If NS3 has been sent and the nonce NB agrees with the nonce B joined with
NA, then A initiated the run using NA.*)
--- a/src/HOL/Auth/NS_Public_Bad.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Tue Sep 23 15:41:33 2003 +0200
@@ -46,8 +46,8 @@
\<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
declare knows_Spy_partsEs [elim]
-declare analz_subset_parts [THEN subsetD, dest]
-declare Fake_parts_insert [THEN subsetD, dest]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
(*A "possibility property": there are traces that reach the end*)
@@ -207,6 +207,9 @@
apply (frule_tac A' = A in
Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
apply (rename_tac C B' evs3)
+txt{*This is the attack!
+@{subgoals[display,indent=0,margin=65]}
+*}
oops
(*
--- a/src/HOL/Auth/NS_Shared.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Tue Sep 23 15:41:33 2003 +0200
@@ -80,12 +80,14 @@
text{*A "possibility property": there are traces that reach the end*}
-lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
- Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
+lemma "[| A \<noteq> Server; Key K \<notin> used [] |]
+ ==> \<exists>N. \<exists>evs \<in> ns_shared.
+ Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] ns_shared.Nil
[THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
- THEN ns_shared.NS4, THEN ns_shared.NS5], possibility)
+ THEN ns_shared.NS4, THEN ns_shared.NS5])
+apply (possibility, simp add: used_Cons)
done
(*This version is similar, while instantiating ?K and ?N to epsilon-terms
--- a/src/HOL/Auth/OtwayRees.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Tue Sep 23 15:41:33 2003 +0200
@@ -89,16 +89,16 @@
text{*A "possibility property": there are traces that reach the end*}
-lemma "B \<noteq> Server
- ==> \<exists>K. \<exists>evs \<in> otway.
+lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
+ ==> \<exists>evs \<in> otway.
Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
\<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] otway.Nil
[THEN otway.OR1, THEN otway.Reception,
THEN otway.OR2, THEN otway.Reception,
- THEN otway.OR3, THEN otway.Reception, THEN otway.OR4],
- possibility)
+ THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
+apply (possibility, simp add: used_Cons)
done
lemma Gets_imp_Says [dest!]:
--- a/src/HOL/Auth/OtwayRees_AN.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Tue Sep 23 15:41:33 2003 +0200
@@ -82,15 +82,16 @@
(*A "possibility property": there are traces that reach the end*)
-lemma "B \<noteq> Server
- ==> \<exists>K. \<exists>evs \<in> otway.
+lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
+ ==> \<exists>evs \<in> otway.
Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|})
\<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] otway.Nil
[THEN otway.OR1, THEN otway.Reception,
THEN otway.OR2, THEN otway.Reception,
- THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
+ THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
+apply (possibility, simp add: used_Cons)
done
lemma Gets_imp_Says [dest!]:
--- a/src/HOL/Auth/OtwayRees_Bad.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Tue Sep 23 15:41:33 2003 +0200
@@ -90,15 +90,16 @@
declare Fake_parts_insert_in_Un [dest]
(*A "possibility property": there are traces that reach the end*)
-lemma "B \<noteq> Server
- ==> \<exists>K. \<exists>NA. \<exists>evs \<in> otway.
+lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
+ ==> \<exists>NA. \<exists>evs \<in> otway.
Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
\<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] otway.Nil
[THEN otway.OR1, THEN otway.Reception,
THEN otway.OR2, THEN otway.Reception,
- THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
+ THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
+apply (possibility, simp add: used_Cons)
done
lemma Gets_imp_Says [dest!]:
--- a/src/HOL/Auth/Public.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/Public.thy Tue Sep 23 15:41:33 2003 +0200
@@ -400,7 +400,7 @@
simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
disj_comms
image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
- analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
+ analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]
insert_Key_singleton
Key_not_used insert_Key_image Un_assoc [THEN sym]
@@ -412,19 +412,4 @@
addsimps thms"analz_image_freshK_simps"
*}
-axioms
- Key_supply_ax: "finite KK ==> \<exists>K\<in>symKeys. K \<notin> KK & Key K \<notin> used evs"
- --{*Unlike the corresponding property of nonces, this cannot be proved.
- We have infinitely many agents and there is nothing to stop their
- long-term keys from exhausting all the natural numbers. The axiom
- assumes that their keys are dispersed so as to leave room for infinitely
- many fresh session keys. We could, alternatively, restrict agents to
- an unspecified finite number. We could however replace @{term"used evs"}
- by @{term "used []"}.*}
-
-
-lemma Key_supply1: "\<exists>K\<in>symKeys. Key K \<notin> used evs"
-by (rule Finites.emptyI [THEN Key_supply_ax, THEN bexE], blast)
-
-
end
--- a/src/HOL/Auth/Recur.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/Recur.thy Tue Sep 23 15:41:33 2003 +0200
@@ -117,37 +117,40 @@
text{*Simplest case: Alice goes directly to the server*}
-lemma "\<exists>K NA. \<exists>evs \<in> recur.
- Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
- END|} \<in> set evs"
+lemma "Key K \<notin> used []
+ ==> \<exists>NA. \<exists>evs \<in> recur.
+ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
+ END|} \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] recur.Nil [THEN recur.RA1,
- THEN recur.RA3 [OF _ _ respond.One]], possibility)
+ THEN recur.RA3 [OF _ _ respond.One]])
+apply (possibility, simp add: used_Cons)
done
text{*Case two: Alice, Bob and the server*}
-lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
+lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K' |]
+ ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
END|} \<in> set evs"
-apply (cut_tac Nonce_supply2 Key_supply2, clarify)
+apply (cut_tac Nonce_supply2, clarify)
apply (intro exI bexI)
apply (rule_tac [2]
recur.Nil [THEN recur.RA1,
THEN recur.RA2,
THEN recur.RA3 [OF _ _ respond.One [THEN respond.Cons]],
THEN recur.RA4])
-apply (tactic "basic_possibility_tac")
-apply (tactic
- "DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
+apply possibility
+apply (auto simp add: used_Cons)
done
-(*Case three: Alice, Bob, Charlie and the server
- Rather slow (16 seconds) to run every time...
-lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
- Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
- END|} \<in> set evs"
-apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1", clarify)
+(*Case three: Alice, Bob, Charlie and the server Rather slow (5 seconds)*)
+lemma "[| Key K \<notin> used []; Key K' \<notin> used [];
+ Key K'' \<notin> used []; K \<noteq> K'; K' \<noteq> K''; K \<noteq> K'' |]
+ ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
+ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
+ END|} \<in> set evs"
+apply (cut_tac Nonce_supply3, clarify)
apply (intro exI bexI)
apply (rule_tac [2]
recur.Nil [THEN recur.RA1,
@@ -157,11 +160,8 @@
[THEN respond.Cons, THEN respond.Cons]],
THEN recur.RA4, THEN recur.RA4])
apply (tactic "basic_possibility_tac")
-apply (tactic
- "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 ORELSE \
-\ eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
+apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)")
done
-*)
(**** Inductive proofs about recur ****)
--- a/src/HOL/Auth/Shared.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/Shared.thy Tue Sep 23 15:41:33 2003 +0200
@@ -51,10 +51,7 @@
text{*Now cancel the @{text dest} attribute given to
@{text analz.Decrypt} in its declaration.*}
-ML
-{*
-Delrules [analz.Decrypt];
-*}
+declare analz.Decrypt [rule del]
text{*Rewrites should not refer to @{term "initState(Friend i)"} because
that expression is not in normal form.*}
@@ -137,7 +134,7 @@
apply (cut_tac evs = evs in Nonce_supply_lemma)
apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify)
apply (rule_tac x = N in exI)
-apply (rule_tac x = "Suc (N+Na) " in exI)
+apply (rule_tac x = "Suc (N+Na)" in exI)
apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
done
@@ -147,7 +144,7 @@
apply (cut_tac evs = "evs'" in Nonce_supply_lemma)
apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify)
apply (rule_tac x = N in exI)
-apply (rule_tac x = "Suc (N+Na) " in exI)
+apply (rule_tac x = "Suc (N+Na)" in exI)
apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI)
apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
done
@@ -157,42 +154,12 @@
apply (rule someI, blast)
done
-subsection{*Supply fresh keys for possibility theorems.*}
-
-axioms
- Key_supply_ax: "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"
- --{*Unlike the corresponding property of nonces, this cannot be proved.
+text{*Unlike the corresponding property of nonces, we cannot prove
+ @{term "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"}.
We have infinitely many agents and there is nothing to stop their
- long-term keys from exhausting all the natural numbers. The axiom
- assumes that their keys are dispersed so as to leave room for infinitely
- many fresh session keys. We could, alternatively, restrict agents to
- an unspecified finite number. We could however replace @{term"used evs"}
- by @{term "used []"}.*}
-
-lemma Key_supply1: "\<exists>K. Key K \<notin> used evs"
-by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast)
+ long-term keys from exhausting all the natural numbers. Instead,
+ possibility theorems must assume the existence of a few keys.*}
-lemma Key_supply2: "\<exists>K K'. Key K \<notin> used evs & Key K' \<notin> used evs' & K \<noteq> K'"
-apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
-apply (erule exE)
-apply (cut_tac evs="evs'" in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax], auto)
-done
-
-lemma Key_supply3: "\<exists>K K' K''. Key K \<notin> used evs & Key K' \<notin> used evs' &
- Key K'' \<notin> used evs'' & K \<noteq> K' & K' \<noteq> K'' & K \<noteq> K''"
-apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
-apply (erule exE)
-(*Blast_tac requires instantiation of the keys for some reason*)
-apply (cut_tac evs="evs'" and a1 = K in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax])
-apply (erule exE)
-apply (cut_tac evs = "evs''" and a1 = Ka and a2 = K
- in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Key_supply_ax], blast)
-done
-
-lemma Key_supply: "Key (@ K. Key K \<notin> used evs) \<notin> used evs"
-apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE])
-apply (rule someI, blast)
-done
subsection{*Tactics for possibility theorems*}
@@ -200,8 +167,6 @@
{*
val inj_shrK = thm "inj_shrK";
val isSym_keys = thm "isSym_keys";
-val Key_supply_ax = thm "Key_supply_ax";
-val Key_supply = thm "Key_supply";
val Nonce_supply = thm "Nonce_supply";
val invKey_K = thm "invKey_K";
val analz_Decrypt' = thm "analz_Decrypt'";
@@ -221,10 +186,6 @@
val Nonce_supply2 = thm "Nonce_supply2";
val Nonce_supply3 = thm "Nonce_supply3";
val Nonce_supply = thm "Nonce_supply";
-val Key_supply1 = thm "Key_supply1";
-val Key_supply2 = thm "Key_supply2";
-val Key_supply3 = thm "Key_supply3";
-val Key_supply = thm "Key_supply";
*}
@@ -238,7 +199,7 @@
setSolver safe_solver))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
- resolve_tac [refl, conjI, Nonce_supply, Key_supply])))
+ resolve_tac [refl, conjI, Nonce_supply])))
(*Tactic for possibility theorems (ML script version)*)
fun possibility_tac state = gen_possibility_tac (simpset()) state
--- a/src/HOL/Auth/Yahalom.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/Yahalom.thy Tue Sep 23 15:41:33 2003 +0200
@@ -88,15 +88,16 @@
declare analz_into_parts [dest]
(*A "possibility property": there are traces that reach the end*)
-lemma "A \<noteq> Server
- ==> \<exists>X NB K. \<exists>evs \<in> yahalom.
+lemma "[| A \<noteq> Server; Key K \<notin> used [] |]
+ ==> \<exists>X NB. \<exists>evs \<in> yahalom.
Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] yahalom.Nil
[THEN yahalom.YM1, THEN yahalom.Reception,
THEN yahalom.YM2, THEN yahalom.Reception,
THEN yahalom.YM3, THEN yahalom.Reception,
- THEN yahalom.YM4], possibility)
+ THEN yahalom.YM4])
+apply (possibility, simp add: used_Cons)
done
lemma Gets_imp_Says:
--- a/src/HOL/Auth/Yahalom2.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Tue Sep 23 15:41:33 2003 +0200
@@ -80,14 +80,16 @@
declare analz_into_parts [dest]
text{*A "possibility property": there are traces that reach the end*}
-lemma "\<exists>X NB K. \<exists>evs \<in> yahalom.
+lemma "Key K \<notin> used []
+ ==> \<exists>X NB. \<exists>evs \<in> yahalom.
Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] yahalom.Nil
[THEN yahalom.YM1, THEN yahalom.Reception,
THEN yahalom.YM2, THEN yahalom.Reception,
THEN yahalom.YM3, THEN yahalom.Reception,
- THEN yahalom.YM4], possibility)
+ THEN yahalom.YM4])
+apply (possibility, simp add: used_Cons)
done
lemma Gets_imp_Says:
--- a/src/HOL/Auth/Yahalom_Bad.thy Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy Tue Sep 23 15:41:33 2003 +0200
@@ -70,15 +70,16 @@
(*A "possibility property": there are traces that reach the end*)
-lemma "A \<noteq> Server
- ==> \<exists>X NB K. \<exists>evs \<in> yahalom.
- Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+lemma "[| A \<noteq> Server; Key K \<notin> used [] |]
+ ==> \<exists>X NB. \<exists>evs \<in> yahalom.
+ Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] yahalom.Nil
[THEN yahalom.YM1, THEN yahalom.Reception,
THEN yahalom.YM2, THEN yahalom.Reception,
THEN yahalom.YM3, THEN yahalom.Reception,
- THEN yahalom.YM4], possibility)
+ THEN yahalom.YM4])
+apply (possibility, simp add: used_Cons)
done
lemma Gets_imp_Says: