# HG changeset patch # User paulson # Date 1065085024 -7200 # Node ID db95d1c2f51b33107a48c026eeba70afeac35e0e # Parent 9f5679e97eac2e1da74b726e05766f8d43440cea removal of junk and improvement of the document diff -r 9f5679e97eac -r db95d1c2f51b src/HOL/SET-Protocol/Cardholder_Registration.thy --- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Wed Oct 01 11:02:36 2003 +0200 +++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Thu Oct 02 10:57:04 2003 +0200 @@ -348,11 +348,8 @@ apply (erule set_cr.induct) apply (frule_tac [8] Gets_certificate_valid) apply (frule_tac [6] Gets_certificate_valid, simp_all) -txt{*Fake*} -apply (force dest!: usedI keysFor_parts_insert) -txt{*Others*} -apply blast -apply auto +apply (force dest!: usedI keysFor_parts_insert) --{*Fake*} +apply (blast,auto) --{*Others*} done @@ -389,6 +386,7 @@ by (blast intro: Crypt_parts_imp_used) +(*<*) subsection{*Messages signed by CA*} text{*Message @{text SET_CR2}: C can check CA's signature if he has received @@ -459,7 +457,7 @@ ==> \Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \ set evs" by (blast dest!: certificate_valid_pubSK intro!: CA_Says_6_lemma) - +(*>*) subsection{*Useful lemmas *} @@ -574,10 +572,8 @@ analz_image_priEK disj_simps) --{*46 seconds on a 1.8GHz machine*} apply spy_analz -txt{*3*} -apply blast -txt{*5*} -apply blast +apply blast --{*3*} +apply blast --{*5*} done text{*The remaining quantifiers seem to be essential. @@ -601,8 +597,7 @@ DK_fresh_not_KeyCryptKey analz_image_priEK) --{*13 seconds on a 1.8GHz machine*} -txt{*Fake*} -apply spy_analz +apply spy_analz --{*Fake*} apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used) done @@ -691,8 +686,7 @@ "[|cardSK \ symKeys; \C. cardSK \ priEK C; evs \ set_cr|] ==> Key cardSK \ analz (knows Spy evs) --> ~ KeyCryptNonce cardSK N evs" apply (erule set_cr.induct, analz_mono_contra, simp_all) -txt{*6*} -apply (blast dest: not_KeyCryptKey_cardSK) +apply (blast dest: not_KeyCryptKey_cardSK) --{*6*} done subsubsection{*Lemmas for message 5 and 6: @@ -746,20 +740,18 @@ DK_fresh_not_KeyCryptNonce K_fresh_not_KeyCryptKey ball_conj_distrib analz_image_priEK) --{*71 seconds on a 1.8GHz machine*} -txt{*Fake*} -apply spy_analz -txt{*3*} -apply blast -txt{*5*} -apply blast -txt{*6*} -txt{*cardSK compromised?*} +apply spy_analz --{*Fake*} +apply blast --{*3*} +apply blast --{*5*} +txt{*Message 6*} apply (force del: allE ballE impCE simp add: symKey_compromise) + --{*cardSK compromised*} txt{*Simplify again--necessary because the previous simplification introduces some logical connectives*} -by (force del: allE ballE impCE +apply (force del: allE ballE impCE simp del: image_insert image_Un imp_disjL simp add: analz_image_keys_simps symKey_compromise) +done subsection{*Secrecy of CardSecret: the Cardholder's secret*} @@ -824,22 +816,14 @@ ball_conj_distrib Nonce_compromise symKey_compromise analz_image_priEK) --{*12 seconds on a 1.8GHz machine*} -txt{*Fake*} -apply spy_analz +apply spy_analz --{*Fake*} apply (simp_all (no_asm_simp)) -txt{*1*} -apply blast -txt{*2*} -apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) -txt{*3*} -apply blast -txt{*4*} -apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt) -txt{*5*} -apply blast -txt{*6*} -apply (blast dest: KC2_secrecy) -apply (blast dest: KC2_secrecy) +apply blast --{*1*} +apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) --{*2*} +apply blast --{*3*} +apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt) --{*4*} +apply blast --{*5*} +apply (blast dest: KC2_secrecy)+ --{*Message 6: two cases*} done @@ -898,21 +882,13 @@ ball_conj_distrib Nonce_compromise symKey_compromise analz_image_priEK) --{*15 seconds on a 1.8GHz machine*} -txt{*Fake*} -apply spy_analz -txt{*1*} -apply blast -txt{*2*} -apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) -txt{*3*} -apply blast -txt{*4*} -apply (blast dest: NC2_not_NonceCCA) -txt{*5*} -apply blast -txt{*6*} -apply (blast dest: KC2_secrecy) -apply (blast dest: KC2_secrecy) +apply spy_analz --{*Fake*} +apply blast --{*1*} +apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) --{*2*} +apply blast --{*3*} +apply (blast dest: NC2_not_NonceCCA) --{*4*} +apply blast --{*5*} +apply (blast dest: KC2_secrecy)+ --{*Message 6: two cases*} done @@ -974,8 +950,7 @@ notin_image_iff analz_image_priEK) --{*33 seconds on a 1.8GHz machine*} apply spy_analz -txt{*6*} -apply (simp add: insert_absorb) +apply (simp add: insert_absorb) --{*6*} done lemma analz_insert_pan: @@ -1005,14 +980,10 @@ add: analz_image_keys_simps analz_insert_pan analz_image_pan notin_image_iff analz_image_priEK) --{*18 seconds on a 1.8GHz machine*} -txt{*fake*} -apply spy_analz -txt{*3*} -apply blast -txt{*5*} -apply blast -txt{*6*} -apply (simp (no_asm_simp) add: insert_absorb) +apply spy_analz --{*fake*} +apply blast --{*3*} +apply blast --{*5*} +apply (simp (no_asm_simp) add: insert_absorb) --{*6*} done @@ -1052,6 +1023,7 @@ done +(*<*) text{*UNUSED unicity result*} lemma unique_KC1: "[|Says C B {|Crypt KC1 X, Crypt EK {|Key KC1, Y|}|} @@ -1073,6 +1045,8 @@ apply (erule rev_mp) apply (erule set_cr.induct, auto) done +(*>*) + text{*Cannot show cardSK to be secret because it isn't assumed to be fresh it could be a previously compromised cardSK [e.g. involving a bad CA]*} diff -r 9f5679e97eac -r db95d1c2f51b src/HOL/SET-Protocol/EventSET.thy --- a/src/HOL/SET-Protocol/EventSET.thy Wed Oct 01 11:02:36 2003 +0200 +++ b/src/HOL/SET-Protocol/EventSET.thy Thu Oct 02 10:57:04 2003 +0200 @@ -131,75 +131,6 @@ parts.Body [THEN revcut_rl, standard] -subsection{*Lemmas About Agents' Knowledge*} - -lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)" -by auto - -lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)" -by auto - -lemma knows_Gets: - "A \ Spy --> knows A (Gets A X # evs) = insert X (knows A evs)" -by auto - -lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A B X # evs)" -by auto - -lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A X # evs)" -by auto - -lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A X # evs)" -by auto - -(*Agents know what they say*) -lemma Says_imp_knows [rule_format]: - "Says A B X \ set evs --> X \ knows A evs" -apply (induct_tac "evs") -apply (auto split: event.split) -done - -(*Agents know what they note*) -lemma Notes_imp_knows [rule_format]: - "Notes A X \ set evs --> X \ knows A evs" -apply (induct_tac "evs") -apply (auto split: event.split) -done - -(*Agents know what they receive*) -lemma Gets_imp_knows_agents [rule_format]: - "A \ Spy --> Gets A X \ set evs --> X \ knows A evs" -apply (induct_tac "evs") -apply (auto split: event.split) -done - - -(*What agents DIFFERENT FROM Spy know - was either said, or noted, or got, or known initially*) -lemma knows_imp_Says_Gets_Notes_initState [rule_format]: - "[| X \ knows A evs; A \ Spy |] ==> - \B. Says A B X \ set evs | - Gets A X \ set evs | - Notes A X \ set evs | - X \ initState A" -apply (erule rev_mp) -apply (induct_tac "evs") -apply (auto split: event.split) -done - -(*What the Spy knows -- for the time being -- - was either said or noted, or known initially*) -lemma knows_Spy_imp_Says_Notes_initState [rule_format]: - "[| X \ knows Spy evs |] ==> - \A B. Says A B X \ set evs | - Notes A X \ set evs | - X \ initState Spy" -apply (erule rev_mp) -apply (induct_tac "evs") -apply (auto split: event.split) -done - - subsection{*The Function @{term used}*} lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs" @@ -225,11 +156,6 @@ lemma used_Gets [simp]: "used (Gets A X # evs) = used evs" by auto -lemma used_nil_subset: "used [] <= used evs" -apply auto -apply (rule initState_into_used, auto) -done - lemma Notes_imp_parts_subset_used [rule_format]: "Notes A X \ set evs --> parts {X} <= used evs" @@ -255,11 +181,9 @@ {* val analz_mono_contra_tac = let val analz_impI = inst "P" "?Y \ analz (knows Spy ?evs)" impI - in - rtac analz_impI THEN' - REPEAT1 o - (dresolve_tac (thms"analz_mono_contra")) - THEN' mp_tac + in rtac analz_impI THEN' + REPEAT1 o (dresolve_tac (thms"analz_mono_contra")) THEN' + mp_tac end *} diff -r 9f5679e97eac -r db95d1c2f51b src/HOL/SET-Protocol/Merchant_Registration.thy --- a/src/HOL/SET-Protocol/Merchant_Registration.thy Wed Oct 01 11:02:36 2003 +0200 +++ b/src/HOL/SET-Protocol/Merchant_Registration.thy Thu Oct 02 10:57:04 2003 +0200 @@ -189,14 +189,10 @@ ==> Key K \ used evs --> K \ symKeys --> K \ keysFor (parts (knows Spy evs))" apply (erule set_mr.induct, simp_all) -txt{*Fake*} -apply (force dest!: usedI keysFor_parts_insert) -txt{*Message 2*} -apply force -txt{*Message 3*} -apply (blast dest: Gets_certificate_valid) -txt{*Message 4*} -apply force +apply (force dest!: usedI keysFor_parts_insert) --{*Fake*} +apply force --{*Message 2*} +apply (blast dest: Gets_certificate_valid) --{*Message 3*} +apply force --{*Message 4*} done @@ -294,10 +290,8 @@ analz_knows_absorb2 analz_Key_image_insert_eq notin_image_iff Spy_analz_private_Key analz_image_priEK) --{*23 seconds on a 1.8GHz machine*} -txt{*Fake*} -apply spy_analz -txt{*Message 3*} -apply auto +apply spy_analz --{*Fake*} +apply auto --{*Message 3*} done lemma symKey_secrecy [rule_format]: @@ -315,12 +309,9 @@ analz_knows_absorb2 analz_Key_image_insert_eq symKey_compromise notin_image_iff Spy_analz_private_Key analz_image_priEK) -txt{*Fake*} -apply spy_analz -txt{*Message 1*} -apply force -txt{*Message 3*} -apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used) +apply spy_analz --{*Fake*} +apply force --{*Message 1*} +apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used) --{*Message 3*} done subsection{*Unicity *} diff -r 9f5679e97eac -r db95d1c2f51b src/HOL/SET-Protocol/MessageSET.thy --- a/src/HOL/SET-Protocol/MessageSET.thy Wed Oct 01 11:02:36 2003 +0200 +++ b/src/HOL/SET-Protocol/MessageSET.thy Thu Oct 02 10:57:04 2003 +0200 @@ -829,86 +829,16 @@ subsection{*Tactics useful for many protocol proofs*} +(*<*) ML {* -val invKey = thm "invKey" -val keysFor_def = thm "keysFor_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 analz_increasing = thm "analz_increasing"; 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"; - (*Prove base case (subgoal i) and simplify others. A typical base case concerns Crypt K X \ Key`shrK`bad and cannot be proved by rewriting @@ -955,6 +885,8 @@ fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i *} +(*>*) + (*By default only o_apply is built-in. But in the presence of eta-expansion this means that some terms displayed as (f o g) will be rewritten, and others diff -r 9f5679e97eac -r db95d1c2f51b src/HOL/SET-Protocol/PublicSET.thy --- a/src/HOL/SET-Protocol/PublicSET.thy Wed Oct 01 11:02:36 2003 +0200 +++ b/src/HOL/SET-Protocol/PublicSET.thy Thu Oct 02 10:57:04 2003 +0200 @@ -40,6 +40,7 @@ specification (publicKey) injective_publicKey: "publicKey b A = publicKey c A' ==> b=c & A=A'" +(*<*) apply (rule exI [of _ "%b A. 2 * nat_of_agent A + (if b then 1 else 0)"]) apply (auto simp add: inj_on_def inj_nat_of_agent [THEN inj_eq] split: agent.split) apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+ @@ -47,7 +48,7 @@ apply presburger+ *) done - +(*>*) axioms (*No private key equals any public key (essential to ensure that private @@ -68,7 +69,7 @@ RCA (has already certified and therefore) knows all CAs public keys; Spy knows all keys of all bad agents.*} primrec - +(*<*) initState_CA: "initState (CA i) = (if i=0 then Key ` ({priEK RCA, priSK RCA} Un @@ -94,7 +95,7 @@ {Key (priEK (PG i)), Key (priSK (PG i)), Key (pubEK (PG i)), Key (pubSK (PG i)), Key (pubEK RCA), Key (pubSK RCA)}" - +(*>*) initState_Spy: "initState Spy = Key ` (invKey ` pubEK ` bad Un invKey ` pubSK ` bad Un @@ -108,9 +109,11 @@ specification (pan) inj_pan: "inj pan" --{*No two agents have the same PAN*} +(*<*) apply (rule exI [of _ "nat_of_agent"]) apply (simp add: inj_on_def inj_nat_of_agent [THEN inj_eq]) done +(*>*) declare inj_pan [THEN inj_eq, iff] @@ -274,11 +277,10 @@ lemma keysFor_parts_insert: "[| K \ keysFor (parts (insert X H)); X \ synth (analz H) |] ==> K \ keysFor (parts H) | Key (invKey K) \ parts H" -apply (force dest!: +by (force dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD] analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] intro: analz_into_parts) -done lemma Crypt_imp_keysFor [intro]: "[|K \ symKeys; Crypt K X \ H|] ==> K \ keysFor H"