--- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Wed Sep 24 10:44:41 2003 +0200
+++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Fri Sep 26 10:32:26 2003 +0200
@@ -250,26 +250,23 @@
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
\<in> set evs"
apply (intro exI bexI)
-apply (rule_tac [2] ?NC1.8 = NC1 and ?NC1.10 = NC1
- and ?NC2.4 = NC2 and ?NC2.6 = NC2
- and ?NC3.0 = NC3 and ?NC3.2 = NC3
- and NCA2 = NCA and NCA4 = NCA
- and CardSecret = CardSecret and CardSecret2 = CardSecret
- and ?KC1.4 = KC1 and ?KC1.6 = KC1
- and ?KC2.0 = KC2 and ?KC2.2 = KC2
- and ?KC3.0 = KC3 and ?KC3.2 = KC3
- in
- set_cr.Nil [THEN set_cr.SET_CR1, THEN Says_to_Gets,
- THEN set_cr.SET_CR2, THEN Says_to_Gets,
- THEN set_cr.SET_CR3, THEN Says_to_Gets,
- THEN set_cr.SET_CR4, THEN Says_to_Gets,
- THEN set_cr.SET_CR5, THEN Says_to_Gets,
- THEN set_cr.SET_CR6])
+apply (rule_tac [2]
+ set_cr.Nil
+ [THEN set_cr.SET_CR1 [of concl: C i NC1],
+ THEN Says_to_Gets,
+ THEN set_cr.SET_CR2 [of concl: i C NC1],
+ THEN Says_to_Gets,
+ THEN set_cr.SET_CR3 [of concl: C i KC1 _ NC2],
+ THEN Says_to_Gets,
+ THEN set_cr.SET_CR4 [of concl: i C NC2 NCA],
+ THEN Says_to_Gets,
+ THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret],
+ THEN Says_to_Gets,
+ THEN set_cr.SET_CR6 [of concl: i C KC2]])
+apply (tactic "basic_possibility_tac")
apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
-apply auto
done
-
text{*General facts about message reception*}
lemma Gets_imp_Says:
"[| Gets B X \<in> set evs; evs \<in> set_cr |] ==> \<exists>A. Says A B X \<in> set evs"
--- a/src/HOL/SET-Protocol/PublicSET.thy Wed Sep 24 10:44:41 2003 +0200
+++ b/src/HOL/SET-Protocol/PublicSET.thy Fri Sep 26 10:32:26 2003 +0200
@@ -9,17 +9,6 @@
subsection{*Symmetric and Asymmetric Keys*}
-axioms
- Key_supply_ax:
- "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs & K \<in> symKeys"
- --{*Unlike the corresponding property of nonces, this cannot be proved.
- We have infinitely many agents and there is nothing to stop their
- 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.*}
-
-
text{*definitions influenced by the wish to assign asymmetric keys
- since the beginning - only to RCA and CAs, namely we need a partial
function on type Agent*}
@@ -322,8 +311,7 @@
text{*Spy sees private keys of bad agents! [and obviously public keys too]*}
lemma knows_Spy_bad_privateKey [intro!]:
"A \<in> bad ==> Key (invKey (publicKey b A)) \<in> knows Spy evs"
-apply (rule initState_subset_knows [THEN subsetD], simp)
-done
+by (rule initState_subset_knows [THEN subsetD], simp)
subsection{*Fresh Nonces for Possibility Theorems*}
@@ -351,52 +339,12 @@
done
-subsection{*Fresh Numbers for Possibility Theorems*}
-
-lemma Number_notin_initState [iff]: "Number N \<notin> parts (initState B)"
-by (induct_tac "B", auto)
-
-lemma Number_notin_used_empty [simp]: "Number N \<notin> used []"
-by (simp add: used_Nil)
-
-text{*In any trace, there is an upper bound N on the greatest number in use.*}
-lemma Number_supply_lemma: "\<exists>N. \<forall>n. N<=n --> Number n \<notin> used evs"
-apply (induct_tac "evs")
-apply (rule_tac x = 0 in exI)
-apply (simp_all add: used_Cons split add: event.split, safe)
-apply (rule msg_Number_supply [THEN exE], blast elim!: add_leE)+
-done
-
-lemma Number_supply1: "\<exists>N. Number N \<notin> used evs"
-by (rule Number_supply_lemma [THEN exE], blast)
-
-lemma Number_supply: "Number (@ N. Number N \<notin> used evs) \<notin> used evs"
-apply (rule Number_supply_lemma [THEN exE])
-apply (rule someI, fast)
-done
-
-
-subsection{*Fresh Keys for Possibility Theorems*}
-
-lemma Key_supply1: "\<exists>K. Key K \<notin> used evs & K \<in> symKeys"
-by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast)
-
-lemma Key_supply:
- "(@K. K \<in> symKeys & Key K \<notin> used evs) \<in> symKeys &
- Key (@K. K \<in> symKeys & Key K \<notin> used evs) \<notin> used evs"
-apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE])
-apply (rule someI, blast)
-done
-
-
subsection{*Specialized Methods for Possibility Theorems*}
ML
{*
val Nonce_supply1 = thm "Nonce_supply1";
val Nonce_supply = thm "Nonce_supply";
-val Key_supply = thm "Key_supply";
-val Number_supply = thm "Number_supply";
val used_Says = thm "used_Says";
val used_Notes = thm "used_Notes";
@@ -407,9 +355,7 @@
(ALLGOALS (simp_tac (ss delsimps [used_Says,used_Notes]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
- resolve_tac [refl, conjI, Nonce_supply, Number_supply,
- Key_supply RS conjunct1,
- Key_supply RS conjunct2]))
+ 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/SET-Protocol/Purchase.thy Wed Sep 24 10:44:41 2003 +0200
+++ b/src/HOL/SET-Protocol/Purchase.thy Fri Sep 26 10:32:26 2003 +0200
@@ -296,54 +296,80 @@
"Says A B X # evs \<in> set_pur ==> Gets B X # Says A B X # evs \<in> set_pur"
by (rule set_pur.Reception, auto)
-(* Possibility for UNSIGNED purchases*)
+text{*Possibility for UNSIGNED purchases. Note that we need to ensure
+that XID differs from OrderDesc and PurchAmt, since it is supposed to be
+a unique number!*}
lemma possibility_Uns:
- "[| CardSecret k = 0;
- \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range CardSecret;
- \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range PANSecret;
- \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range CardSecret;
- \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range PANSecret
- |] ==> \<exists>LID_M. \<exists>XID. \<exists>Chall_C.
- \<exists>evs \<in> set_pur.
- Says (Merchant i) (Cardholder k)
- (sign (priSK (Merchant i))
- {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|})
- \<in> set evs"
+ "[| CardSecret k = 0;
+ C = Cardholder k; M = Merchant i;
+ Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used [];
+ KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys;
+ KC < KM; KM < KP;
+ Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret;
+ Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret;
+ Chall_C < Chall_M;
+ Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret;
+ Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret;
+ LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |]
+ ==> \<exists>evs \<in> set_pur.
+ Says M C
+ (sign (priSK M)
+ {|Number LID_M, Number XID, Nonce Chall_C,
+ Hash (Number PurchAmt)|})
+ \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2]
- set_pur.Nil [THEN set_pur.Start,
- THEN set_pur.PInitReq, THEN Says_to_Gets,
- THEN set_pur.PInitRes, THEN Says_to_Gets,
- THEN set_pur.PReqUns, THEN Says_to_Gets,
- THEN set_pur.AuthReq, THEN Says_to_Gets,
- THEN set_pur.AuthResUns, THEN Says_to_Gets,
- THEN set_pur.PRes])
-apply (possibility, erule spec)+
+ set_pur.Nil
+ [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt],
+ THEN set_pur.PInitReq [of concl: C M LID_M Chall_C],
+ THEN Says_to_Gets,
+ THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M],
+ THEN Says_to_Gets,
+ THEN set_pur.PReqUns [of concl: C M KC],
+ THEN Says_to_Gets,
+ THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID],
+ THEN Says_to_Gets,
+ THEN set_pur.AuthResUns [of concl: "PG j" M KP LID_M XID],
+ THEN Says_to_Gets,
+ THEN set_pur.PRes])
+apply (tactic "basic_possibility_tac")
+apply (simp_all add: used_Cons symKeys_neq_imp_neq)
done
lemma possibility_S:
- "[| CardSecret k \<noteq> 0;
- \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range CardSecret;
- \<forall>evs. (@ No. Nonce No \<notin> used evs) \<notin> range PANSecret;
- \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range CardSecret;
- \<forall>evs. (@ Nn. Number Nn \<notin> used evs) \<notin> range PANSecret
- |] ==> \<exists>LID_M. \<exists>XID. \<exists>Chall_C.
- \<exists>evs \<in> set_pur.
- Says (Merchant i) (Cardholder k)
- (sign (priSK (Merchant i))
- {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|})
- \<in> set evs"
+ "[| CardSecret k \<noteq> 0;
+ C = Cardholder k; M = Merchant i;
+ Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used [];
+ KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys;
+ KC < KM; KM < KP;
+ Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret;
+ Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret;
+ Chall_C < Chall_M;
+ Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret;
+ Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret;
+ LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |]
+ ==> \<exists>evs \<in> set_pur.
+ Says M C
+ (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C,
+ Hash (Number PurchAmt)|})
+ \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2]
- set_pur.Nil [THEN set_pur.Start,
- THEN set_pur.PInitReq, THEN Says_to_Gets,
- THEN set_pur.PInitRes, THEN Says_to_Gets,
- THEN set_pur.PReqS, THEN Says_to_Gets,
- THEN set_pur.AuthReq, THEN Says_to_Gets,
- THEN set_pur.AuthResS, THEN Says_to_Gets,
- THEN set_pur.PRes])
-apply possibility --{*39 seconds on a 1.8GHz machine*}
-apply ((erule spec)+, auto)
+ set_pur.Nil
+ [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt],
+ THEN set_pur.PInitReq [of concl: C M LID_M Chall_C],
+ THEN Says_to_Gets,
+ THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M],
+ THEN Says_to_Gets,
+ THEN set_pur.PReqS [of concl: C M _ _ KC],
+ THEN Says_to_Gets,
+ THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID],
+ THEN Says_to_Gets,
+ THEN set_pur.AuthResS [of concl: "PG j" M KP LID_M XID],
+ THEN Says_to_Gets,
+ THEN set_pur.PRes])
+apply (tactic "basic_possibility_tac")
+apply (auto simp add: used_Cons symKeys_neq_imp_neq)
done
(*General facts about message reception*)