(* Title: HOL/Auth/Public ID: $Id: Public.thy,v 1.24 2005/06/17 14:13:06 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge Theory of Public Keys (common to all public-key protocols) Private and public keys; initial states of agents *) theory Public imports Event begin lemma invKey_K: "K ∈ symKeys ==> invKey K = K" by (simp add: symKeys_def) subsection{*Asymmetric Keys*} consts (*the bool is TRUE if a signing key*) publicKey :: "[bool,agent] => key" syntax pubEK :: "agent => key" pubSK :: "agent => key" privateKey :: "[bool,agent] => key" priEK :: "agent => key" priSK :: "agent => key" translations "pubEK" == "publicKey False" "pubSK" == "publicKey True" (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*) "privateKey b A" == "invKey (publicKey b A)" "priEK A" == "privateKey False A" "priSK A" == "privateKey True A" text{*These translations give backward compatibility. They represent the simple situation where the signature and encryption keys are the same.*} syntax pubK :: "agent => key" priK :: "agent => key" translations "pubK A" == "pubEK A" "priK A" == "invKey (pubEK A)" text{*By freeness of agents, no two agents have the same key. Since @{term "True≠False"}, no agent has identical signing and encryption keys*} specification (publicKey) injective_publicKey: "publicKey b A = publicKey c A' ==> b=c & A=A'" apply (rule exI [of _ "%b A. 2 * agent_case 0 (λn. n + 2) 1 A + (if b then 1 else 0)"]) apply (auto simp add: inj_on_def split: agent.split, presburger+) done axioms (*No private key equals any public key (essential to ensure that private keys are private!) *) privateKey_neq_publicKey [iff]: "privateKey b A ≠ publicKey c A'" declare privateKey_neq_publicKey [THEN not_sym, iff] subsection{*Basic properties of @{term pubK} and @{term priK}*} lemma [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')" by (blast dest!: injective_publicKey) lemma not_symKeys_pubK [iff]: "publicKey b A ∉ symKeys" by (simp add: symKeys_def) lemma not_symKeys_priK [iff]: "privateKey b A ∉ symKeys" by (simp add: symKeys_def) lemma symKey_neq_priEK: "K ∈ symKeys ==> K ≠ priEK A" by auto lemma symKeys_neq_imp_neq: "(K ∈ symKeys) ≠ (K' ∈ symKeys) ==> K ≠ K'" by blast lemma symKeys_invKey_iff [iff]: "(invKey K ∈ symKeys) = (K ∈ symKeys)" by (unfold symKeys_def, auto) lemma analz_symKeys_Decrypt: "[| Crypt K X ∈ analz H; K ∈ symKeys; Key K ∈ analz H |] ==> X ∈ analz H" by (auto simp add: symKeys_def) subsection{*"Image" equations that hold for injective functions*} lemma invKey_image_eq [simp]: "(invKey x ∈ invKey`A) = (x ∈ A)" by auto (*holds because invKey is injective*) lemma publicKey_image_eq [simp]: "(publicKey b x ∈ publicKey c ` AA) = (b=c & x ∈ AA)" by auto lemma privateKey_notin_image_publicKey [simp]: "privateKey b x ∉ publicKey c ` AA" by auto lemma privateKey_image_eq [simp]: "(privateKey b A ∈ invKey ` publicKey c ` AS) = (b=c & A∈AS)" by auto lemma publicKey_notin_image_privateKey [simp]: "publicKey b A ∉ invKey ` publicKey c ` AS" by auto subsection{*Symmetric Keys*} text{*For some protocols, it is convenient to equip agents with symmetric as well as asymmetric keys. The theory @{text Shared} assumes that all keys are symmetric.*} consts shrK :: "agent => key" --{*long-term shared keys*} specification (shrK) inj_shrK: "inj shrK" --{*No two agents have the same long-term key*} apply (rule exI [of _ "agent_case 0 (λn. n + 2) 1"]) apply (simp add: inj_on_def split: agent.split) done axioms sym_shrK [iff]: "shrK X ∈ symKeys" --{*All shared keys are symmetric*} (*Injectiveness: Agents' long-term keys are distinct.*) declare inj_shrK [THEN inj_eq, iff] lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A" by (simp add: invKey_K) lemma analz_shrK_Decrypt: "[| Crypt (shrK A) X ∈ analz H; Key(shrK A) ∈ analz H |] ==> X ∈ analz H" by auto lemma analz_Decrypt': "[| Crypt K X ∈ analz H; K ∈ symKeys; Key K ∈ analz H |] ==> X ∈ analz H" by (auto simp add: invKey_K) lemma priK_neq_shrK [iff]: "shrK A ≠ privateKey b C" by (simp add: symKeys_neq_imp_neq) declare priK_neq_shrK [THEN not_sym, simp] lemma pubK_neq_shrK [iff]: "shrK A ≠ publicKey b C" by (simp add: symKeys_neq_imp_neq) declare pubK_neq_shrK [THEN not_sym, simp] lemma priEK_noteq_shrK [simp]: "priEK A ≠ shrK B" by auto lemma publicKey_notin_image_shrK [simp]: "publicKey b x ∉ shrK ` AA" by auto lemma privateKey_notin_image_shrK [simp]: "privateKey b x ∉ shrK ` AA" by auto lemma shrK_notin_image_publicKey [simp]: "shrK x ∉ publicKey b ` AA" by auto lemma shrK_notin_image_privateKey [simp]: "shrK x ∉ invKey ` publicKey b ` AA" by auto lemma shrK_image_eq [simp]: "(shrK x ∈ shrK ` AA) = (x ∈ AA)" by auto text{*For some reason, moving this up can make some proofs loop!*} declare invKey_K [simp] subsection{*Initial States of Agents*} text{*Note: for all practical purposes, all that matters is the initial knowledge of the Spy. All other agents are automata, merely following the protocol.*} primrec (*Agents know their private key and all public keys*) initState_Server: "initState Server = {Key (priEK Server), Key (priSK Server)} ∪ (Key ` range pubEK) ∪ (Key ` range pubSK) ∪ (Key ` range shrK)" initState_Friend: "initState (Friend i) = {Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} ∪ (Key ` range pubEK) ∪ (Key ` range pubSK)" initState_Spy: "initState Spy = (Key ` invKey ` pubEK ` bad) ∪ (Key ` invKey ` pubSK ` bad) ∪ (Key ` shrK ` bad) ∪ (Key ` range pubEK) ∪ (Key ` range pubSK)" text{*These lemmas allow reasoning about @{term "used evs"} rather than @{term "knows Spy evs"}, which is useful when there are private Notes. Because they depend upon the definition of @{term initState}, they cannot be moved up.*} lemma used_parts_subset_parts [rule_format]: "∀X ∈ used evs. parts {X} ⊆ used evs" apply (induct evs) prefer 2 apply (simp add: used_Cons) apply (rule ballI) apply (case_tac a, auto) apply (auto dest!: parts_cut) txt{*Base case*} apply (simp add: used_Nil) done lemma MPair_used_D: "{|X,Y|} ∈ used H ==> X ∈ used H & Y ∈ used H" by (drule used_parts_subset_parts, simp, blast) lemma MPair_used [elim!]: "[| {|X,Y|} ∈ used H; [| X ∈ used H; Y ∈ used H |] ==> P |] ==> P" by (blast dest: MPair_used_D) text{*Rewrites should not refer to @{term "initState(Friend i)"} because that expression is not in normal form.*} lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" apply (unfold keysFor_def) apply (induct_tac "C") apply (auto intro: range_eqI) done lemma Crypt_notin_initState: "Crypt K X ∉ parts (initState B)" by (induct B, auto) lemma Crypt_notin_used_empty [simp]: "Crypt K X ∉ used []" by (simp add: Crypt_notin_initState used_Nil) (*** Basic properties of shrK ***) (*Agents see their own shared keys!*) lemma shrK_in_initState [iff]: "Key (shrK A) ∈ initState A" by (induct_tac "A", auto) lemma shrK_in_knows [iff]: "Key (shrK A) ∈ knows A evs" by (simp add: initState_subset_knows [THEN subsetD]) lemma shrK_in_used [iff]: "Key (shrK A) ∈ used evs" by (rule initState_into_used, blast) (** Fresh keys never clash with long-term shared keys **) (*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys from long-term shared keys*) lemma Key_not_used [simp]: "Key K ∉ used evs ==> K ∉ range shrK" by blast lemma shrK_neq: "Key K ∉ used evs ==> shrK B ≠ K" by blast declare shrK_neq [THEN not_sym, simp] subsection{*Function @{term spies} *} text{*Agents see their own private keys!*} lemma priK_in_initState [iff]: "Key (privateKey b A) ∈ initState A" by (induct_tac "A", auto) text{*Agents see all public keys!*} lemma publicKey_in_initState [iff]: "Key (publicKey b A) ∈ initState B" by (case_tac "B", auto) text{*All public keys are visible*} lemma spies_pubK [iff]: "Key (publicKey b A) ∈ spies evs" apply (induct_tac "evs") apply (simp_all add: imageI knows_Cons split add: event.split) done declare spies_pubK [THEN analz.Inj, iff] text{*Spy sees private keys of bad agents!*} lemma Spy_spies_bad_privateKey [intro!]: "A ∈ bad ==> Key (privateKey b A) ∈ spies evs" apply (induct_tac "evs") apply (simp_all add: imageI knows_Cons split add: event.split) done text{*Spy sees long-term shared keys of bad agents!*} lemma Spy_spies_bad_shrK [intro!]: "A ∈ bad ==> Key (shrK A) ∈ spies evs" apply (induct_tac "evs") apply (simp_all add: imageI knows_Cons split add: event.split) done lemma publicKey_into_used [iff] :"Key (publicKey b A) ∈ used evs" apply (rule initState_into_used) apply (rule publicKey_in_initState [THEN parts.Inj]) done lemma privateKey_into_used [iff]: "Key (privateKey b A) ∈ used evs" apply(rule initState_into_used) apply(rule priK_in_initState [THEN parts.Inj]) done (*For case analysis on whether or not an agent is compromised*) lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X ∈ analz (knows Spy evs); A ∈ bad |] ==> X ∈ analz (knows Spy evs)" by force subsection{*Fresh Nonces*} lemma Nonce_notin_initState [iff]: "Nonce N ∉ parts (initState B)" by (induct_tac "B", auto) lemma Nonce_notin_used_empty [simp]: "Nonce N ∉ used []" by (simp add: used_Nil) subsection{*Supply fresh nonces for possibility theorems*} text{*In any trace, there is an upper bound N on the greatest nonce in use*} lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n ∉ used evs" apply (induct_tac "evs") apply (rule_tac x = 0 in exI) apply (simp_all (no_asm_simp) add: used_Cons split add: event.split) apply safe apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+ done lemma Nonce_supply1: "EX N. Nonce N ∉ used evs" by (rule Nonce_supply_lemma [THEN exE], blast) lemma Nonce_supply: "Nonce (@ N. Nonce N ∉ used evs) ∉ used evs" apply (rule Nonce_supply_lemma [THEN exE]) apply (rule someI, fast) done subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*} lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H" by blast lemma insert_Key_image: "insert (Key K) (Key`KK ∪ C) = Key ` (insert K KK) ∪ C" by blast ML {* val Key_not_used = thm "Key_not_used"; val insert_Key_singleton = thm "insert_Key_singleton"; val insert_Key_image = thm "insert_Key_image"; *} lemma Crypt_imp_keysFor :"[|Crypt K X ∈ H; K ∈ symKeys|] ==> K ∈ keysFor H" by (drule Crypt_imp_invKey_keysFor, simp) text{*Lemma for the trivial direction of the if-and-only-if of the Session Key Compromise Theorem*} lemma analz_image_freshK_lemma: "(Key K ∈ analz (Key`nE ∪ H)) --> (K ∈ nE | Key K ∈ analz H) ==> (Key K ∈ analz (Key`nE ∪ H)) = (K ∈ nE | Key K ∈ analz H)" by (blast intro: analz_mono [THEN [2] rev_subsetD]) lemmas analz_image_freshK_simps = 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 subsetD] insert_Key_singleton Key_not_used insert_Key_image Un_assoc [THEN sym] ML {* val analz_image_freshK_lemma = thm "analz_image_freshK_lemma"; val analz_image_freshK_simps = thms "analz_image_freshK_simps"; val analz_image_freshK_ss = simpset() delsimps [image_insert, image_Un] delsimps [imp_disjL] (*reduces blow-up*) addsimps thms "analz_image_freshK_simps" *} method_setup analz_freshK = {* Method.no_args (Method.METHOD (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), REPEAT_FIRST (rtac analz_image_freshK_lemma), ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *} "for proving the Session Key Compromise theorem" subsection{*Specialized Methods for Possibility Theorems*} ML {* val Nonce_supply = thm "Nonce_supply"; (*Tactic for possibility theorems (Isar interface)*) fun gen_possibility_tac ss state = state |> REPEAT (*omit used_Says so that Nonces start from different traces!*) (ALLGOALS (simp_tac (ss delsimps [used_Says])) THEN REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI, Nonce_supply])) (*Tactic for possibility theorems (ML script version)*) fun possibility_tac state = gen_possibility_tac (simpset()) state (*For harder protocols (such as Recur) where we have to set up some nonces and keys initially*) fun basic_possibility_tac st = st |> REPEAT (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver)) THEN REPEAT_FIRST (resolve_tac [refl, conjI])) *} method_setup possibility = {* Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => gen_possibility_tac (local_simpset_of ctxt))) *} "for proving possibility theorems" end
lemma invKey_K:
K ∈ symKeys ==> invKey K = K
lemma
(publicKey b A = publicKey c A') = (b = c ∧ A = A')
lemma not_symKeys_pubK:
publicKey b A ∉ symKeys
lemma not_symKeys_priK:
privateKey b A ∉ symKeys
lemma symKey_neq_priEK:
K ∈ symKeys ==> K ≠ priEK A
lemma symKeys_neq_imp_neq:
(K ∈ symKeys) ≠ (K' ∈ symKeys) ==> K ≠ K'
lemma symKeys_invKey_iff:
(invKey K ∈ symKeys) = (K ∈ symKeys)
lemma analz_symKeys_Decrypt:
[| Crypt K X ∈ analz H; K ∈ symKeys; Key K ∈ analz H |] ==> X ∈ analz H
lemma invKey_image_eq:
(invKey x ∈ invKey ` A) = (x ∈ A)
lemma publicKey_image_eq:
(publicKey b x ∈ publicKey c ` AA) = (b = c ∧ x ∈ AA)
lemma privateKey_notin_image_publicKey:
privateKey b x ∉ publicKey c ` AA
lemma privateKey_image_eq:
(privateKey b A ∈ invKey ` publicKey c ` AS) = (b = c ∧ A ∈ AS)
lemma publicKey_notin_image_privateKey:
publicKey b A ∉ invKey ` publicKey c ` AS
lemma invKey_shrK:
invKey (shrK A) = shrK A
lemma analz_shrK_Decrypt:
[| Crypt (shrK A) X ∈ analz H; Key (shrK A) ∈ analz H |] ==> X ∈ analz H
lemma analz_Decrypt':
[| Crypt K X ∈ analz H; K ∈ symKeys; Key K ∈ analz H |] ==> X ∈ analz H
lemma priK_neq_shrK:
shrK A ≠ privateKey b C
lemma pubK_neq_shrK:
shrK A ≠ publicKey b C
lemma priEK_noteq_shrK:
priEK A ≠ shrK B
lemma publicKey_notin_image_shrK:
publicKey b x ∉ shrK ` AA
lemma privateKey_notin_image_shrK:
privateKey b x ∉ shrK ` AA
lemma shrK_notin_image_publicKey:
shrK x ∉ publicKey b ` AA
lemma shrK_notin_image_privateKey:
shrK x ∉ invKey ` publicKey b ` AA
lemma shrK_image_eq:
(shrK x ∈ shrK ` AA) = (x ∈ AA)
lemma used_parts_subset_parts:
X ∈ used evs ==> parts {X} ⊆ used evs
lemma MPair_used_D:
{|X, Y|} ∈ used H ==> X ∈ used H ∧ Y ∈ used H
lemma MPair_used:
[| {|X, Y|} ∈ used H; [| X ∈ used H; Y ∈ used H |] ==> P |] ==> P
lemma keysFor_parts_initState:
keysFor (parts (initState C)) = {}
lemma Crypt_notin_initState:
Crypt K X ∉ parts (initState B)
lemma Crypt_notin_used_empty:
Crypt K X ∉ used []
lemma shrK_in_initState:
Key (shrK A) ∈ initState A
lemma shrK_in_knows:
Key (shrK A) ∈ knows A evs
lemma shrK_in_used:
Key (shrK A) ∈ used evs
lemma Key_not_used:
Key K ∉ used evs ==> K ∉ range shrK
lemma shrK_neq:
Key K ∉ used evs ==> shrK B ≠ K
lemma priK_in_initState:
Key (privateKey b A) ∈ initState A
lemma publicKey_in_initState:
Key (publicKey b A) ∈ initState B
lemma spies_pubK:
Key (publicKey b A) ∈ knows Spy evs
lemma Spy_spies_bad_privateKey:
A ∈ bad ==> Key (privateKey b A) ∈ knows Spy evs
lemma Spy_spies_bad_shrK:
A ∈ bad ==> Key (shrK A) ∈ knows Spy evs
lemma publicKey_into_used:
Key (publicKey b A) ∈ used evs
lemma privateKey_into_used:
Key (privateKey b A) ∈ used evs
lemma Crypt_Spy_analz_bad:
[| Crypt (shrK A) X ∈ analz (knows Spy evs); A ∈ bad |] ==> X ∈ analz (knows Spy evs)
lemma Nonce_notin_initState:
Nonce N ∉ parts (initState B)
lemma Nonce_notin_used_empty:
Nonce N ∉ used []
lemma Nonce_supply_lemma:
∃N. ∀n. N ≤ n --> Nonce n ∉ used evs
lemma Nonce_supply1:
∃N. Nonce N ∉ used evs
lemma Nonce_supply:
Nonce (SOME N. Nonce N ∉ used evs) ∉ used evs
lemma insert_Key_singleton:
insert (Key K) H = Key ` {K} ∪ H
lemma insert_Key_image:
insert (Key K) (Key ` KK ∪ C) = Key ` insert K KK ∪ C
lemma Crypt_imp_keysFor:
[| Crypt K X ∈ H; K ∈ symKeys |] ==> K ∈ keysFor H
lemma analz_image_freshK_lemma:
Key K ∈ analz (Key ` nE ∪ H) --> K ∈ nE ∨ Key K ∈ analz H ==> (Key K ∈ analz (Key ` nE ∪ H)) = (K ∈ nE ∨ Key K ∈ analz H)
lemmas analz_image_freshK_simps:
(¬ ¬ P) = P
((¬ P) = (¬ Q)) = (P = Q)
(P ≠ Q) = (P = (¬ Q))
(P ∨ ¬ P) = True
(¬ P ∨ P) = True
(x = x) = True
(¬ True) = False
(¬ False) = True
(¬ P) ≠ P
P ≠ (¬ P)
(True = P) = P
(P = True) = P
(False = P) = (¬ P)
(P = False) = (¬ P)
(True --> P) = P
(False --> P) = True
(P --> True) = True
(P --> P) = True
(P --> False) = (¬ P)
(P --> ¬ P) = (¬ P)
(P ∧ True) = P
(True ∧ P) = P
(P ∧ False) = False
(False ∧ P) = False
(P ∧ P) = P
(P ∧ P ∧ Q) = (P ∧ Q)
(P ∧ ¬ P) = False
(¬ P ∧ P) = False
(P ∨ True) = True
(True ∨ P) = True
(P ∨ False) = P
(False ∨ P) = P
(P ∨ P) = P
(P ∨ P ∨ Q) = (P ∨ Q)
(∀x. P) = P
(∃x. P) = P
∃x. x = t
∃x. t = x
(∃x. x = t ∧ P x) = P t
(∃x. t = x ∧ P x) = P t
(∀x. x = t --> P x) = P t
(∀x. t = x --> P x) = P t
(a ∈ insert b A) = (a = b ∨ a ∈ A)
(c ∈ {}) = False
(c ∈ A ∪ B) = (c ∈ A ∨ c ∈ B)
(c ∈ A ∩ B) = (c ∈ A ∧ c ∈ B)
(c ∈ - A) = (c ∉ A)
(c ∈ A - B) = (c ∈ A ∧ c ∉ B)
(a ∈ {x. P x}) = P a
(b ∈ (UN x:A. B x)) = (∃x∈A. b ∈ B x)
(A ∈ Union C) = (∃X∈C. A ∈ X)
(b ∈ (INT x:A. B x)) = (∀x∈A. b ∈ B x)
(A ∈ Inter C) = (∀X∈C. A ∈ X)
(P ∨ Q) = (Q ∨ P)
(P ∨ Q ∨ R) = (Q ∨ P ∨ R)
insert (f1 a1) (f1 ` B1) = f1 ` insert a1 B1
f1 ` A1 ∪ f1 ` B1 = f1 ` (A1 ∪ B1)
{} ⊆ A
(insert x A ⊆ B) = (x ∈ B ∧ A ⊆ B)
X ∈ analz H ==> analz (insert X H) = analz H
c ∈ analz G1 ==> c ∈ analz (A2 ∪ G1)
insert (Key K) H = Key ` {K} ∪ H
Key K ∉ used evs ==> K ∉ range shrK
insert (Key K) (Key ` KK ∪ C) = Key ` insert K KK ∪ C
A1 ∪ (B1 ∪ C1) = A1 ∪ B1 ∪ C1
lemmas analz_image_freshK_simps:
(¬ ¬ P) = P
((¬ P) = (¬ Q)) = (P = Q)
(P ≠ Q) = (P = (¬ Q))
(P ∨ ¬ P) = True
(¬ P ∨ P) = True
(x = x) = True
(¬ True) = False
(¬ False) = True
(¬ P) ≠ P
P ≠ (¬ P)
(True = P) = P
(P = True) = P
(False = P) = (¬ P)
(P = False) = (¬ P)
(True --> P) = P
(False --> P) = True
(P --> True) = True
(P --> P) = True
(P --> False) = (¬ P)
(P --> ¬ P) = (¬ P)
(P ∧ True) = P
(True ∧ P) = P
(P ∧ False) = False
(False ∧ P) = False
(P ∧ P) = P
(P ∧ P ∧ Q) = (P ∧ Q)
(P ∧ ¬ P) = False
(¬ P ∧ P) = False
(P ∨ True) = True
(True ∨ P) = True
(P ∨ False) = P
(False ∨ P) = P
(P ∨ P) = P
(P ∨ P ∨ Q) = (P ∨ Q)
(∀x. P) = P
(∃x. P) = P
∃x. x = t
∃x. t = x
(∃x. x = t ∧ P x) = P t
(∃x. t = x ∧ P x) = P t
(∀x. x = t --> P x) = P t
(∀x. t = x --> P x) = P t
(a ∈ insert b A) = (a = b ∨ a ∈ A)
(c ∈ {}) = False
(c ∈ A ∪ B) = (c ∈ A ∨ c ∈ B)
(c ∈ A ∩ B) = (c ∈ A ∧ c ∈ B)
(c ∈ - A) = (c ∉ A)
(c ∈ A - B) = (c ∈ A ∧ c ∉ B)
(a ∈ {x. P x}) = P a
(b ∈ (UN x:A. B x)) = (∃x∈A. b ∈ B x)
(A ∈ Union C) = (∃X∈C. A ∈ X)
(b ∈ (INT x:A. B x)) = (∀x∈A. b ∈ B x)
(A ∈ Inter C) = (∀X∈C. A ∈ X)
(P ∨ Q) = (Q ∨ P)
(P ∨ Q ∨ R) = (Q ∨ P ∨ R)
insert (f1 a1) (f1 ` B1) = f1 ` insert a1 B1
f1 ` A1 ∪ f1 ` B1 = f1 ` (A1 ∪ B1)
{} ⊆ A
(insert x A ⊆ B) = (x ∈ B ∧ A ⊆ B)
X ∈ analz H ==> analz (insert X H) = analz H
c ∈ analz G1 ==> c ∈ analz (A2 ∪ G1)
insert (Key K) H = Key ` {K} ∪ H
Key K ∉ used evs ==> K ∉ range shrK
insert (Key K) (Key ` KK ∪ C) = Key ` insert K KK ∪ C
A1 ∪ (B1 ∪ C1) = A1 ∪ B1 ∪ C1