# HG changeset patch # User paulson # Date 1064565146 -7200 # Node ID 77bf175f51450b650c6b32f316f6cdb656567a9e # Parent 4ae8d65bc97cff92219995b99e6d30df26776ad3 Tidying of SET's "possibility theorems" (removal of Key_supply_ax) diff -r 4ae8d65bc97c -r 77bf175f5145 src/HOL/SET-Protocol/Cardholder_Registration.thy --- 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)|}) \ 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 \ set evs; evs \ set_cr |] ==> \A. Says A B X \ set evs" diff -r 4ae8d65bc97c -r 77bf175f5145 src/HOL/SET-Protocol/PublicSET.thy --- 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 ==> \K. K \ KK & Key K \ used evs & K \ 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 \ bad ==> Key (invKey (publicKey b A)) \ 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 \ parts (initState B)" -by (induct_tac "B", auto) - -lemma Number_notin_used_empty [simp]: "Number N \ 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: "\N. \n. N<=n --> Number n \ 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: "\N. Number N \ used evs" -by (rule Number_supply_lemma [THEN exE], blast) - -lemma Number_supply: "Number (@ N. Number N \ used evs) \ used evs" -apply (rule Number_supply_lemma [THEN exE]) -apply (rule someI, fast) -done - - -subsection{*Fresh Keys for Possibility Theorems*} - -lemma Key_supply1: "\K. Key K \ used evs & K \ symKeys" -by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast) - -lemma Key_supply: - "(@K. K \ symKeys & Key K \ used evs) \ symKeys & - Key (@K. K \ symKeys & Key K \ used evs) \ 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 diff -r 4ae8d65bc97c -r 77bf175f5145 src/HOL/SET-Protocol/Purchase.thy --- 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 \ set_pur ==> Gets B X # Says A B X # evs \ 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; - \evs. (@ No. Nonce No \ used evs) \ range CardSecret; - \evs. (@ No. Nonce No \ used evs) \ range PANSecret; - \evs. (@ Nn. Number Nn \ used evs) \ range CardSecret; - \evs. (@ Nn. Number Nn \ used evs) \ range PANSecret - |] ==> \LID_M. \XID. \Chall_C. - \evs \ set_pur. - Says (Merchant i) (Cardholder k) - (sign (priSK (Merchant i)) - {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|}) - \ set evs" + "[| CardSecret k = 0; + C = Cardholder k; M = Merchant i; + Key KC \ used []; Key KM \ used []; Key KP \ used []; + KC \ symKeys; KM \ symKeys; KP \ symKeys; + KC < KM; KM < KP; + Nonce Chall_C \ used []; Chall_C \ range CardSecret \ range PANSecret; + Nonce Chall_M \ used []; Chall_M \ range CardSecret \ range PANSecret; + Chall_C < Chall_M; + Number LID_M \ used []; LID_M \ range CardSecret \ range PANSecret; + Number XID \ used []; XID \ range CardSecret \ range PANSecret; + LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] + ==> \evs \ set_pur. + Says M C + (sign (priSK M) + {|Number LID_M, Number XID, Nonce Chall_C, + Hash (Number PurchAmt)|}) + \ 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 \ 0; - \evs. (@ No. Nonce No \ used evs) \ range CardSecret; - \evs. (@ No. Nonce No \ used evs) \ range PANSecret; - \evs. (@ Nn. Number Nn \ used evs) \ range CardSecret; - \evs. (@ Nn. Number Nn \ used evs) \ range PANSecret - |] ==> \LID_M. \XID. \Chall_C. - \evs \ set_pur. - Says (Merchant i) (Cardholder k) - (sign (priSK (Merchant i)) - {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|}) - \ set evs" + "[| CardSecret k \ 0; + C = Cardholder k; M = Merchant i; + Key KC \ used []; Key KM \ used []; Key KP \ used []; + KC \ symKeys; KM \ symKeys; KP \ symKeys; + KC < KM; KM < KP; + Nonce Chall_C \ used []; Chall_C \ range CardSecret \ range PANSecret; + Nonce Chall_M \ used []; Chall_M \ range CardSecret \ range PANSecret; + Chall_C < Chall_M; + Number LID_M \ used []; LID_M \ range CardSecret \ range PANSecret; + Number XID \ used []; XID \ range CardSecret \ range PANSecret; + LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] + ==> \evs \ set_pur. + Says M C + (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, + Hash (Number PurchAmt)|}) + \ 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*)