Theory Payloads

(*******************************************************************************

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  Payloads.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Payloads.thy 132885 2016-12-23 18:41:32Z csprenge $
  Author:  Joseph Lallemand, INRIA Nancy <joseph.lallemand@loria.fr>
           Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Payload messages are messages that contain no implementation material,
  i.e. neither long-term keys nor channel tags; also:
  - auxiliary definitions: Keys_bad, broken, Enc_keys_clean 
  - lemmas for moving message sets out of 'analz'

  Copyright (c) 2015-2016 Joseph Lallemand and Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

section ‹Payloads and Support for Channel Message Implementations› 

text ‹Definitions and lemmas that do not require the implementations.›

theory Payloads
imports Message_derivation
begin

subsection ‹Payload messages›
(**************************************************************************************************)

text ‹Payload messages contain no implementation material ie no long term keys or tags.›

text ‹Define set of payloads for basic messages.›
inductive_set cpayload :: "cmsg set" where
  "cAgent A ∈ cpayload"
| "cNumber T ∈ cpayload"
| "cNonce N ∈ cpayload"
| "cEphK K ∈ cpayload"
| "X ∈ cpayload ⟹ cHash X ∈ cpayload"
| "⟦ X ∈ cpayload; Y ∈ cpayload ⟧ ⟹ cPair X Y ∈ cpayload"
| "⟦ X ∈ cpayload; Y ∈ cpayload ⟧ ⟹ cEnc X Y ∈ cpayload"
| "⟦ X ∈ cpayload; Y ∈ cpayload ⟧ ⟹ cAenc X Y ∈ cpayload"
| "⟦ X ∈ cpayload; Y ∈ cpayload ⟧ ⟹ cSign X Y ∈ cpayload"
| "⟦ X ∈ cpayload; Y ∈ cpayload ⟧ ⟹ cExp X Y ∈ cpayload"

text ‹Lift @{term cpayload} to the quotiented message type.›
lift_definition payload :: "msg set" is cpayload by -

text ‹Lemmas used to prove the intro and inversion rules for @{term payload}.›
lemma eq_rep_abs: "eq x (Re (Ab x))"
by (simp add: Quotient3_msg rep_abs_rsp)


lemma eq_cpayload:
  assumes "eq x y" and "x ∈ cpayload"
  shows "y ∈ cpayload"
using assms by (induction x y rule: eq.induct, auto intro: cpayload.intros elim: cpayload.cases)

lemma abs_payload: "Ab x ∈ payload ⟷ x ∈ cpayload"
by (auto simp add: payload_def msg.abs_eq_iff eq_cpayload eq_sym cpayload.intros 
         elim: cpayload.cases)

lemma abs_cpayload_rep: "x ∈ Ab` cpayload ⟷ Re x ∈ cpayload"
apply (auto elim: eq_cpayload [OF eq_rep_abs])
apply (subgoal_tac "x = Ab (Re x)", auto)
using Quotient3_abs_rep Quotient3_msg by fastforce

lemma payload_rep_cpayload: "Re x ∈ cpayload ⟷ x ∈ payload"
by (auto simp add: payload_def abs_cpayload_rep)

text ‹Manual proof of payload introduction rules. Transfer does not work for these›

declare cpayload.intros [intro]
lemma payload_AgentI: "Agent A ∈ payload"
  by (auto simp add: msg_defs abs_payload)
lemma payload_NonceI: "Nonce N ∈ payload"
  by (auto simp add: msg_defs abs_payload)
lemma payload_NumberI: "Number N ∈ payload"
  by (auto simp add: msg_defs abs_payload)
lemma payload_EphKI: "EphK X ∈ payload"
  by (auto simp add: msg_defs abs_payload)
lemma payload_HashI: "x ∈ payload ⟹ Hash x ∈ payload"
  by (auto simp add: msg_defs payload_rep_cpayload abs_payload)
lemma payload_PairI: "x ∈ payload ⟹ y ∈ payload ⟹ Pair x y ∈ payload"
  by (auto simp add: msg_defs payload_rep_cpayload abs_payload)
lemma payload_EncI: "x ∈ payload ⟹ y ∈ payload ⟹ Enc x y ∈ payload"
  by (auto simp add: msg_defs payload_rep_cpayload abs_payload)
lemma payload_AencI: "x ∈ payload ⟹ y ∈ payload ⟹ Aenc x y ∈ payload"
  by (auto simp add: msg_defs payload_rep_cpayload abs_payload)
lemma payload_SignI: "x ∈ payload ⟹ y ∈ payload ⟹ Sign x y ∈ payload"
  by (auto simp add: msg_defs payload_rep_cpayload abs_payload)
lemma payload_ExpI: "x ∈ payload ⟹ y ∈ payload ⟹ Exp x y ∈ payload"
by (auto simp add: msg_defs payload_rep_cpayload abs_payload)

lemmas payload_intros [simp, intro] =
  payload_AgentI payload_NonceI payload_NumberI payload_EphKI payload_HashI
  payload_PairI payload_EncI payload_AencI payload_SignI payload_ExpI

text ‹Manual proof of payload inversion rules, transfer does not work for these.›

declare cpayload.cases[elim]
lemma payload_Tag: "Tag X ∈ payload ⟹ P"
apply (auto simp add: payload_def msg_defs msg.abs_eq_iff eq_sym)
apply (auto dest!: eq_cpayload simp add: abs_cpayload_rep)
done

lemma payload_LtK: "LtK X ∈ payload ⟹ P"
apply (auto simp add: payload_def msg_defs msg.abs_eq_iff eq_sym)
apply (auto dest!: eq_cpayload simp add: abs_cpayload_rep)
done
lemma payload_Hash: "Hash X ∈ payload ⟹ (X ∈ payload ⟹ P) ⟹ P"
apply (auto simp add: payload_def msg_defs msg.abs_eq_iff eq_sym)
apply (auto dest!: eq_cpayload simp add: abs_cpayload_rep)
done
lemma payload_Pair: "Pair X Y ∈ payload ⟹ (X ∈ payload ⟹ Y ∈ payload ⟹ P) ⟹ P"
apply (auto simp add: payload_def msg_defs msg.abs_eq_iff eq_sym)
apply (auto dest!: eq_cpayload simp add: abs_cpayload_rep)
done
lemma payload_Enc: "Enc X Y ∈ payload ⟹ (X ∈ payload ⟹ Y ∈ payload ⟹ P) ⟹ P"
apply (auto simp add: payload_def msg_defs msg.abs_eq_iff eq_sym)
apply (auto dest!: eq_cpayload simp add: abs_cpayload_rep)
done
lemma payload_Aenc: "Aenc X Y ∈ payload ⟹ (X ∈ payload ⟹ Y ∈ payload ⟹ P) ⟹ P"
apply (auto simp add: payload_def msg_defs msg.abs_eq_iff eq_sym)
apply (auto dest!: eq_cpayload simp add: abs_cpayload_rep)
done
lemma payload_Sign: "Sign X Y ∈ payload ⟹ (X ∈ payload ⟹ Y ∈ payload ⟹ P) ⟹ P"
apply (auto simp add: payload_def msg_defs msg.abs_eq_iff eq_sym)
apply (auto dest!: eq_cpayload simp add: abs_cpayload_rep)
done
lemma payload_Exp: "Exp X Y ∈ payload ⟹ (X ∈ payload ⟹ Y ∈ payload ⟹ P) ⟹ P"
apply (auto simp add: payload_def Exp_def msg.abs_eq_iff eq_sym)
apply (auto dest!: eq_cpayload simp add: abs_cpayload_rep)
done

declare cpayload.intros[rule del]
declare cpayload.cases[rule del]

lemmas payload_inductive_cases =
  payload_Tag payload_LtK payload_Hash
  payload_Pair payload_Enc payload_Aenc payload_Sign payload_Exp

lemma eq_exhaust:
"(⋀x. eq y (cAgent x) ⟹ P) ⟹
 (⋀x. eq y (cNumber x) ⟹ P) ⟹
 (⋀x. eq y (cNonce x) ⟹ P) ⟹
 (⋀x. eq y (cLtK x) ⟹ P) ⟹
 (⋀x. eq y (cEphK x) ⟹ P) ⟹
 (⋀x x'. eq y (cPair x x') ⟹ P) ⟹
 (⋀x x'. eq y (cEnc x x') ⟹ P) ⟹
 (⋀x x'. eq y (cAenc x x') ⟹ P) ⟹
 (⋀x x'. eq y (cSign x x') ⟹ P) ⟹
 (⋀x. eq y (cHash x) ⟹ P) ⟹
 (⋀x. eq y (cTag x) ⟹ P) ⟹
 (⋀x x'. eq y (cExp x x') ⟹ P) ⟹
 P"
apply (cases y)
apply (meson Messages.eq_refl)+
done

lemma msg_exhaust:
"(⋀x. y = Agent x ⟹ P) ⟹
 (⋀x. y = Number x ⟹ P) ⟹
 (⋀x. y = Nonce x ⟹ P) ⟹
 (⋀x. y = LtK x ⟹ P) ⟹
 (⋀x. y = EphK x ⟹ P) ⟹
 (⋀x x'. y = Pair x x' ⟹ P) ⟹
 (⋀x x'. y = Enc x x' ⟹ P) ⟹
 (⋀x x'. y = Aenc x x' ⟹ P) ⟹
 (⋀x x'. y = Sign x x' ⟹ P) ⟹
 (⋀x. y = Hash x ⟹ P) ⟹
 (⋀x. y = Tag x ⟹ P) ⟹
 (⋀x x'. y = Exp x x' ⟹ P) ⟹
 P"
apply transfer
apply (erule eq_exhaust, auto)
done

lemma payload_cases: 
"a ∈ payload ⟹
(⋀A. a = Agent A ⟹ P) ⟹
(⋀T. a = Number T ⟹ P) ⟹
(⋀N. a = Nonce N ⟹ P) ⟹
(⋀K. a = EphK K ⟹ P) ⟹
(⋀X. a = Hash X ⟹ X ∈ payload ⟹ P) ⟹
(⋀X Y. a = Pair X Y ⟹ X ∈ payload ⟹ Y ∈ payload ⟹ P) ⟹
(⋀X Y. a = Enc X Y ⟹ X ∈ payload ⟹ Y ∈ payload ⟹ P) ⟹
(⋀X Y. a = Aenc X Y ⟹ X ∈ payload ⟹ Y ∈ payload ⟹ P) ⟹
(⋀X Y. a = Sign X Y ⟹ X ∈ payload ⟹ Y ∈ payload ⟹ P) ⟹
(⋀X Y. a = Exp X Y ⟹ X ∈ payload ⟹ Y ∈ payload ⟹ P) ⟹
 P"
by (erule msg_exhaust [of a], auto elim: payload_inductive_cases)

declare payload_cases [elim]
declare payload_inductive_cases [elim]

text ‹Properties of payload; messages constructed from payload messages are also payloads.›

lemma payload_parts [simp, dest]:
  "⟦ X ∈ parts S; S ⊆ payload ⟧ ⟹ X ∈ payload" 
by (erule parts.induct) (auto)

lemma payload_parts_singleton [simp, dest]:
  "⟦ X ∈ parts {Y}; Y ∈ payload ⟧ ⟹ X ∈ payload" 
by (erule parts.induct) (auto)

lemma payload_analz [simp, dest]:
  "⟦ X ∈ analz S; S ⊆ payload ⟧ ⟹ X ∈ payload" 
by (auto dest: analz_into_parts)

lemma payload_synth_analz: 
  "⟦ X ∈ synth (analz S); S ⊆ payload ⟧ ⟹ X ∈ payload" 
by (erule synth.induct) (auto intro: payload_analz)

text ‹Important lemma: using messages with implementation material one can only 
synthesise more such messages.›

lemma synth_payload: 
  "Y ∩ payload = {} ⟹ synth (X ∪ Y) ⊆ synth X ∪ -payload"
by (rule, erule synth.induct) (auto) 

lemma synth_payload2:
  "Y ∩ payload = {} ⟹ synth (Y ∪ X) ⊆ synth X ∪ -payload"
by (rule, erule synth.induct) (auto) 

text ‹Lemma: in the case of the previous lemma, @{term synth} can be applied on the 
left with no consequence.›

lemma synth_idem_payload:
  "X ⊆ synth Y ∪ -payload ⟹ synth X ⊆ synth Y ∪ -payload"
by (auto dest: synth_mono subset_trans [OF _ synth_payload])


subsection ‹‹isLtKey›: is a long term key›
(**************************************************************************************************)

lemma LtKeys_payload [dest]: "NI ⊆ payload ⟹ NI ∩ range LtK = {}"
by (auto)

lemma LtKeys_parts_payload [dest]: "NI ⊆ payload ⟹ parts NI ∩ range LtK = {}"
by (auto)

lemma LtKeys_parts_payload_singleton [elim]: "X ∈ payload ⟹ LtK Y ∈ parts {X} ⟹ False"
by (auto)

lemma parts_of_LtKeys [simp]: "K ⊆ range LtK ⟹ parts K = K"
by (rule, rule, erule parts.induct, auto) 


subsection‹‹keys_of›: the long term keys of an agent›
(**************************************************************************************************)

definition
  keys_of :: "agent ⇒ msg set"
where
  "keys_of A ≡ insert (priK A) {shrK B C | B C. B = A ∨ C = A}"

lemma keys_of_Ltk [intro!]: "keys_of A ⊆ range LtK"
by (auto simp add: keys_of_def)

lemma priK_keys_of [intro!]:
  "priK A ∈ keys_of A"
by (simp add: keys_of_def)

lemma shrK_keys_of_1 [intro!]:
  "shrK A B ∈ keys_of A"
by (simp add: keys_of_def)

lemma shrK_keys_of_2 [intro!]:
  "shrK B A ∈ keys_of A"
by (simp add: keys_of_def)
lemma priK_keys_of_eq [dest]:
  "priK B ∈ keys_of A ⟹ A = B"
by (simp add: keys_of_def)

lemma shrK_keys_of_eq [dest]:
  "shrK A B ∈ keys_of C ⟹ A = C ∨ B = C"
by (simp add: keys_of_def)

lemma def_keys_of [dest]:
  "K ∈ keys_of A ⟹ K = priK A ∨ (∃ B. K = shrK A B ∨ K = shrK B A)"
by (auto simp add: keys_of_def)

lemma parts_keys_of [simp]: "parts (keys_of A) = keys_of A"
by (auto intro!: parts_of_LtKeys)


lemma analz_keys_of [simp]: "analz (keys_of A) = keys_of A"
by (rule, rule, erule analz.induct, auto)

subsection ‹‹Keys_bad›: bounds on the attacker's knowledge of long-term keys.›
(**************************************************************************************************)

text ‹A set of keys contains all public long term keys, and only the private/shared keys 
of bad agents.›

definition
  Keys_bad :: "msg set ⇒ agent set ⇒ bool"
where
  "Keys_bad IK Bad ≡    
    IK ∩ range LtK ⊆ range pubK ∪ ⋃ (keys_of ` Bad)
    ∧ range pubK ⊆ IK"

― ‹basic lemmas›

lemma Keys_badI:
  "⟦ IK ∩ range LtK ⊆ range pubK ∪ priK`Bad ∪ {shrK A B | A B. A ∈ Bad ∨ B ∈ Bad}; 
     range pubK ⊆ IK  ⟧
 ⟹ Keys_bad IK Bad"
by (auto simp add: Keys_bad_def)

lemma Keys_badE [elim]: 
  "⟦ Keys_bad IK Bad;
     ⟦ range pubK ⊆ IK; 
       IK ∩ range LtK ⊆ range pubK ∪ ⋃ (keys_of ` Bad)⟧
   ⟹ P ⟧ 
 ⟹ P"
by (auto simp add: Keys_bad_def)

lemma Keys_bad_Ltk [simp]:
  "Keys_bad (IK ∩ range LtK) Bad ⟷ Keys_bad IK Bad"
by (auto simp add: Keys_bad_def)


lemma Keys_bad_priK_D: "⟦ priK A ∈ IK; Keys_bad IK Bad ⟧ ⟹ A ∈ Bad"
by (auto simp add: Keys_bad_def)

lemma Keys_bad_shrK_D: "⟦ shrK A B ∈ IK; Keys_bad IK Bad ⟧ ⟹ A ∈ Bad ∨ B ∈ Bad"
by (auto simp add: Keys_bad_def)

lemmas Keys_bad_dests [dest] = Keys_bad_priK_D Keys_bad_shrK_D


text ‹interaction with @{term insert}.›

lemma Keys_bad_insert_non_LtK: 
  "X ∉ range LtK ⟹ Keys_bad (insert X IK) Bad ⟷ Keys_bad IK Bad"
by (auto simp add: Keys_bad_def)

lemma Keys_bad_insert_pubK: 
  "⟦ Keys_bad IK Bad ⟧ ⟹ Keys_bad (insert (pubK A) IK) Bad"
by (auto simp add: Keys_bad_def)

lemma Keys_bad_insert_priK_bad: 
  "⟦ Keys_bad IK Bad; A ∈ Bad ⟧ ⟹ Keys_bad (insert (priK A) IK) Bad"
by (auto simp add: Keys_bad_def)

lemma Keys_bad_insert_shrK_bad: 
  "⟦ Keys_bad IK Bad; A ∈ Bad ∨ B ∈ Bad ⟧ ⟹ Keys_bad (insert (shrK A B) IK) Bad"
by (auto simp add: Keys_bad_def)

lemmas Keys_bad_insert_lemmas [simp] = 
  Keys_bad_insert_non_LtK Keys_bad_insert_pubK 
  Keys_bad_insert_priK_bad Keys_bad_insert_shrK_bad


lemma Keys_bad_insert_Fake:
assumes "Keys_bad IK Bad" 
    and "parts IK ∩ range LtK ⊆ IK"
    and "X ∈ synth (analz IK)"
shows "Keys_bad (insert X IK) Bad"
proof cases
  assume "X ∈ range LtK"
  then obtain ltk where "X = LtK ltk" by blast
  thus ?thesis using assms
    by (auto simp add: insert_absorb dest: analz_into_parts)
next 
  assume "X ∉ range LtK"
  thus ?thesis using assms(1) by simp
qed


lemma Keys_bad_insert_keys_of:
  "Keys_bad Ik Bad ⟹
   Keys_bad (keys_of A ∪ Ik) (insert A Bad)"
by (auto simp add: Keys_bad_def)

lemma Keys_bad_insert_payload:
  "Keys_bad Ik Bad ⟹
   x ∈ payload ⟹
   Keys_bad (insert x Ik) Bad"
by (auto simp add: Keys_bad_def)


subsection ‹‹broken K›: pairs of agents where at least one is compromised.›
(**************************************************************************************************)

text ‹Set of pairs (A,B) such that the priK of A or B, or their shared key, is in K›

definition
  broken :: "msg set ⇒ (agent * agent) set"
where
  "broken K ≡ {(A,B) | A B. priK A ∈ K ∨ priK B ∈ K ∨ shrK A B ∈ K ∨ shrK B A ∈ K}"

lemma brokenD [dest!]:
  "(A, B) ∈ broken K ⟹ priK A ∈ K ∨ priK B ∈ K ∨ shrK A B ∈ K ∨ shrK B A ∈ K"
by (simp add: broken_def)

lemma brokenI [intro!]:
  "priK A ∈ K ∨ priK B ∈ K ∨ shrK A B ∈ K ∨ shrK B A ∈ K ⟹ (A, B) ∈ broken K"
by (auto simp add: broken_def)


subsection ‹‹Enc_keys_clean S›: messages with ``clean'' symmetric encryptions.›
(**************************************************************************************************)

text ‹All terms used as symmetric keys in S are either long term keys or messages without 
implementation material.›

definition
  Enc_keys_clean :: "msg set ⇒ bool"
where
  "Enc_keys_clean S ≡ ∀X Y. Enc X Y ∈ parts S ⟶ Y ∈ range LtK ∪ payload"

lemma Enc_keys_cleanI:
  "∀X Y. Enc X Y ∈ parts S ⟶ Y ∈ range LtK ∪ payload ⟹ Enc_keys_clean S"
by (simp add: Enc_keys_clean_def)

― ‹general lemmas about ‹Enc_keys_clean››
lemma Enc_keys_clean_mono: 
  "Enc_keys_clean H ⟹ G ⊆ H ⟹ Enc_keys_clean G"  ― ‹anti-tone›
by (auto simp add: Enc_keys_clean_def dest!: parts_monotone [where G=G])

lemma Enc_keys_clean_Un [simp]: 
  "Enc_keys_clean (G ∪ H) ⟷ Enc_keys_clean G ∧ Enc_keys_clean H" 
by (auto simp add: Enc_keys_clean_def)


― ‹from ‹Enc_keys_clean S›, the property on ‹parts S› also holds for ‹analz S››
lemma Enc_keys_clean_analz:
  "Enc X K ∈ analz S ⟹ Enc_keys_clean S ⟹ K ∈ range LtK ∪ payload"
by (auto simp add: Enc_keys_clean_def dest: analz_into_parts)


― ‹‹Enc_keys_clean› and different types of messages›
lemma Enc_keys_clean_Tags [simp,intro]: "Enc_keys_clean Tags"
by (auto simp add: Enc_keys_clean_def)

lemma Enc_keys_clean_LtKeys [simp,intro]: "K ⊆ range LtK ⟹ Enc_keys_clean K"
by (auto simp add: Enc_keys_clean_def)

lemma Enc_keys_clean_payload [simp,intro]: "NI ⊆ payload ⟹ Enc_keys_clean NI"
by (auto simp add: Enc_keys_clean_def)


subsection ‹Sets of messages with particular constructors›
(**************************************************************************************************)

text ‹Sets of all pairs, ciphertexts, and signatures constructed from a set of messages.›
(*
 FIX: These should probably be turned into definitions, since they may create automation problems 
*)
abbreviation AgentSet :: "msg set"
where "AgentSet ≡ range Agent"

abbreviation PairSet :: "msg set ⇒ msg set ⇒ msg set"
where "PairSet G H ≡ {Pair X Y | X Y. X ∈ G ∧ Y ∈ H}"

abbreviation EncSet :: "msg set ⇒ msg set ⇒ msg set"
where "EncSet G K ≡ {Enc X Y | X Y. X ∈ G ∧ Y ∈ K}"

abbreviation AencSet :: "msg set ⇒ msg set ⇒ msg set"
where "AencSet G K ≡ {Aenc X Y | X Y. X ∈ G ∧ Y ∈ K}"

abbreviation SignSet :: "msg set ⇒ msg set ⇒ msg set"
where "SignSet G K ≡ {Sign X Y | X Y. X ∈ G ∧ Y ∈ K}"

abbreviation HashSet :: "msg set ⇒ msg set"
where "HashSet G ≡ {Hash X | X. X ∈ G}"


text ‹Move @{term Enc}, @{term Aenc}, @{term Sign}, and @{term Pair} sets out of @{term parts}. 
›

lemma parts_PairSet:
  "parts (PairSet G H) ⊆ PairSet G H ∪ parts G ∪ parts H"
by (rule, erule parts.induct, auto)

lemma parts_EncSet:
  "parts (EncSet G K) ⊆ EncSet G K ∪ PairSet (range Agent) G  ∪ range Agent ∪  parts G"
by (rule, erule parts.induct, auto)

lemma parts_AencSet:
  "parts (AencSet G K) ⊆ AencSet G K ∪ PairSet (range Agent) G  ∪ range Agent ∪  parts G"
by (rule, erule parts.induct, auto)

lemma parts_SignSet:
  "parts (SignSet G K) ⊆ SignSet G K ∪ PairSet (range Agent) G  ∪ range Agent ∪  parts G"
by (rule, erule parts.induct, auto)

lemma parts_HashSet:
  "parts (HashSet G) ⊆ HashSet G"
by (rule, erule parts.induct, auto)

lemmas parts_msgSet = parts_PairSet parts_EncSet parts_AencSet parts_SignSet parts_HashSet
lemmas parts_msgSetD = parts_msgSet [THEN [2] rev_subsetD]

text ‹
Remove the message sets from under the @{term "Enc_keys_clean"} predicate.
Only when the first part is a set of agents or tags for @{term Pair}, this is sufficient.›

lemma Enc_keys_clean_PairSet_Agent_Un: 
  "Enc_keys_clean (G ∪ H) ⟹ Enc_keys_clean (PairSet (Agent`X) G ∪ H)"
by (auto simp add: Enc_keys_clean_def dest!: parts_msgSetD)

lemma Enc_keys_clean_PairSet_Tag_Un: 
  "Enc_keys_clean (G ∪ H) ⟹ Enc_keys_clean (PairSet Tags G ∪ H)"
by (auto simp add: Enc_keys_clean_def dest!: parts_msgSetD)

lemma Enc_keys_clean_AencSet_Un: 
  "Enc_keys_clean (G ∪ H) ⟹ Enc_keys_clean (AencSet G K ∪ H)"
by (auto simp add: Enc_keys_clean_def dest!: parts_msgSetD)

lemma Enc_keys_clean_EncSet_Un: 
  "K ⊆ range LtK ⟹ Enc_keys_clean (G ∪ H) ⟹ Enc_keys_clean (EncSet G K ∪ H)"
by (auto simp add: Enc_keys_clean_def dest!: parts_msgSetD)

lemma Enc_keys_clean_SignSet_Un: 
  "Enc_keys_clean (G ∪ H) ⟹ Enc_keys_clean (SignSet G K ∪ H)"
by (auto simp add: Enc_keys_clean_def dest!: parts_msgSetD)

lemma Enc_keys_clean_HashSet_Un: 
  "Enc_keys_clean (G ∪ H) ⟹ Enc_keys_clean (HashSet G ∪ H)"
by (auto simp add: Enc_keys_clean_def dest!: parts_msgSetD)

lemmas Enc_keys_clean_msgSet_Un =
  Enc_keys_clean_PairSet_Tag_Un Enc_keys_clean_PairSet_Agent_Un
  Enc_keys_clean_EncSet_Un Enc_keys_clean_AencSet_Un
  Enc_keys_clean_SignSet_Un Enc_keys_clean_HashSet_Un


subsubsection ‹Lemmas for moving message sets out of @{term "analz"}›
(**************************************************************************************************)

text ‹Pull @{term EncSet} out of @{term analz}.›

lemma analz_Un_EncSet:
assumes "K ⊆ range LtK" and "Enc_keys_clean (G ∪ H)" 
shows "analz (EncSet G K ∪ H) ⊆ EncSet G K ∪ analz (G ∪ H)"
proof 
  fix X
  assume "X ∈ analz (EncSet G K ∪ H)"
  thus "X ∈ EncSet G K ∪ analz (G ∪ H)"
  proof (induction X rule: analz.induct)
    case (Dec Y K')     
    from Dec.IH(1) show ?case
    proof
      assume "Enc Y K' ∈ analz (G ∪ H)"
      have "K' ∈ synth (analz (G ∪ H))"
      proof -
        have "K' ∈ range LtK ∪ payload" using ‹Enc Y K' ∈ analz (G ∪ H)› assms(2)
          by (blast dest: Enc_keys_clean_analz)
        moreover
        have "K' ∈ synth (EncSet G K ∪ analz (G ∪ H))" using Dec.IH(2)
          by (auto simp add: Collect_disj_eq dest: synth_Int2)
        moreover
        hence "K' ∈ synth (analz (G ∪ H)) ∪ -payload" using assms(1) 
          by (blast dest!: synth_payload2 [THEN [2] rev_subsetD])
        ultimately show ?thesis by auto
      qed  
      thus ?case using ‹Enc Y K' ∈ analz (G ∪ H)› by auto
    qed auto
  next
    case (Adec_eph Y K')  
    thus ?case by (auto dest!: EpriK_synth)
  qed (auto)
qed 

text ‹Pull @{term EncSet} out of @{term analz}, 2nd case: the keys are unknown.›

lemma analz_Un_EncSet2:
assumes "Enc_keys_clean H" and "K ⊆ range LtK" and "K ∩ synth (analz H) = {}"
shows "analz (EncSet G K ∪ H) ⊆ EncSet G K ∪ analz H"
proof 
  fix X
  assume "X ∈ analz (EncSet G K ∪ H)"
  thus "X ∈ EncSet G K ∪ analz H"
  proof (induction X rule: analz.induct)
    case (Dec Y K')
    from Dec.IH(1) show ?case 
    proof
      assume "Enc Y K' ∈ analz H"
      moreover have "K' ∈ synth (analz H)"
      proof -
          have "K' ∈ range LtK ∪ payload" using ‹Enc Y K' ∈ analz H› assms(1)
            by (auto dest: Enc_keys_clean_analz)
          moreover
          from Dec.IH(2) have H: "K' ∈ synth (EncSet G K ∪ analz H)" 
            by (auto simp add: Collect_disj_eq dest: synth_Int2)
          moreover
          hence "K' ∈ synth (analz H) ∪ -payload" 
          proof (rule synth_payload2 [THEN [2] rev_subsetD], auto elim!: payload_Enc)
            fix X Y
            assume "Y ∈ K" "Y ∈ payload"
            with ‹K ⊆ range LtK› obtain KK where "Y = LtK KK" by auto
            with ‹Y ∈ payload› show False by auto
          qed
        ultimately 
        show ?thesis by auto
      qed
      ultimately show ?case by auto
    next
      assume "Enc Y K' ∈ EncSet G K"
      moreover hence "K' ∈ K" by auto
      moreover with ‹K ⊆ range LtK› obtain KK where "K' = LtK KK" by auto
      moreover with Dec.IH(2) have "K' ∈ analz H" 
        by (auto simp add: Collect_disj_eq dest: synth_Int2)
      ultimately show ?case using ‹K ∩ synth (analz H) = {}› by auto
    qed
  next 
    case (Adec_eph Y K') 
    thus ?case by (auto dest!: EpriK_synth)
  qed (insert assms(2), auto)
qed


text ‹Pull @{term AencSet} out of the @{term analz}.›

lemma analz_Un_AencSet:
assumes "K ⊆ range LtK" and "Enc_keys_clean (G ∪ H)" 
shows "analz (AencSet G K ∪ H) ⊆ AencSet G K ∪ analz (G ∪ H)"
proof 
  fix X
  assume "X ∈ analz (AencSet G K ∪ H)"
  thus "X ∈ AencSet G K ∪ analz (G ∪ H)"
  proof (induction X rule: analz.induct)
    case (Dec Y K') 
    from Dec.IH(1) have "Enc Y K' ∈ analz (G ∪ H)" by auto
    moreover have "K' ∈ synth (analz (G ∪ H))" 
    proof -
      have "K' ∈ range LtK ∪ payload" using ‹Enc Y K' ∈ analz (G ∪ H)› assms(2) 
        by (blast dest: Enc_keys_clean_analz)
      moreover
      have "K' ∈ synth (AencSet G K ∪ analz (G ∪ H))" using Dec.IH(2)
        by (auto simp add: Collect_disj_eq dest: synth_Int2)
      moreover
      hence "K' ∈ synth (analz (G ∪ H)) ∪ -payload" using assms(1) 
        by (blast dest!: synth_payload2 [THEN [2] rev_subsetD])
      ultimately 
      show ?thesis by auto 
    qed
    ultimately show ?case by auto
  next 
    case (Adec_eph Y K') 
    thus ?case by (auto dest!: EpriK_synth)
  qed auto
qed

text ‹Pull @{term AencSet} out of @{term analz}, 2nd case: the keys are unknown.›

lemma analz_Un_AencSet2:
assumes "Enc_keys_clean H" and "priK`Ag ∩ synth (analz H) = {}"
shows "analz (AencSet G (pubK`Ag) ∪ H) ⊆ AencSet G (pubK`Ag) ∪ analz H"
proof 
  fix X
  assume "X ∈ analz (AencSet G (pubK` Ag) ∪ H)"
  thus "X ∈ AencSet G (pubK` Ag) ∪ analz H"
  proof (induction X rule: analz.induct)
    case (Dec Y K') 
    from Dec.IH(1) have "Enc Y K' ∈ analz H" by auto
    moreover have "K' ∈ synth (analz H)"
    proof -
      have "K' ∈ range LtK ∪ payload" using ‹Enc Y K' ∈ analz H› assms(1)
      by (auto dest: Enc_keys_clean_analz)
      moreover
      from Dec.IH(2) have H: "K' ∈ synth (AencSet G (pubK`Ag) ∪ analz H)" 
        by (auto simp add: Collect_disj_eq dest: synth_Int2)
      moreover
      hence "K' ∈ synth (analz H) ∪ -payload" 
        by (auto dest: synth_payload2 [THEN [2] rev_subsetD])
      ultimately 
      show ?thesis by auto
    qed
    ultimately show ?case by auto
  next 
    case (Adec_eph Y K') 
    thus ?case by (auto dest!: EpriK_synth)
  qed (insert assms(2), auto)
qed

text ‹Pull @{term PairSet} out of @{term analz}.›
lemma analz_Un_PairSet:
  "analz (PairSet G G' ∪ H) ⊆ PairSet G G' ∪ analz (G ∪ G' ∪ H)"
proof 
  fix X
  assume "X ∈ analz (PairSet G G' ∪ H)"
  thus "X ∈ PairSet G G' ∪ analz (G ∪ G' ∪ H)"
  proof (induct X rule: analz.induct)
    case (Dec Y K) 
    from Dec.hyps(2) have "Enc Y K ∈ analz (G ∪ G' ∪ H)" by auto
    moreover
    from Dec.hyps(3) have "K ∈ synth (PairSet G G' ∪ analz (G ∪ G' ∪ H))"
      by (auto simp add: Collect_disj_eq dest: synth_Int2)
    then have "K ∈ synth (analz (G ∪ G' ∪ H))"
      by (elim synth_trans) auto
    ultimately
    show ?case by auto
  next 
    case (Adec_eph Y K) 
    thus ?case by (auto dest!: EpriK_synth)
  qed auto
qed

― ‹move the ‹SignSet› out of the ‹analz››
lemma analz_Un_SignSet:
assumes "K ⊆ range LtK" and "Enc_keys_clean (G ∪ H)"
shows "analz (SignSet G K ∪ H) ⊆ SignSet G K ∪ analz (G ∪ H)"
proof 
  fix X
  assume "X ∈ analz (SignSet G K ∪ H)"
  thus "X ∈ SignSet G K ∪ analz (G ∪ H)"
  proof (induct X rule: analz.induct)
    case (Dec Y K') 
    from Dec.hyps(2) have "Enc Y K' ∈ analz (G ∪ H)" by auto
    moreover have "K' ∈ synth (analz (G ∪ H))"
    proof -
      have "K' ∈ range LtK ∪ payload" using ‹Enc Y K' ∈ analz (G ∪ H)› assms(2) 
        by (blast dest: Enc_keys_clean_analz)
      moreover
      from Dec.hyps(3) have "K' ∈ synth (SignSet G K ∪ analz (G ∪ H)) "
        by (auto simp add: Collect_disj_eq dest: synth_Int2)
      moreover
      hence "K' ∈ synth (analz (G ∪ H)) ∪ -payload" using assms(1) 
        by (blast dest!: synth_payload2 [THEN [2] rev_subsetD])
      ultimately 
      show ?thesis by auto
    qed
    ultimately show ?case by auto
  next 
    case (Adec_eph Y K) 
    thus ?case by (auto dest!: EpriK_synth)
  qed auto
qed

text ‹Pull @{term Tags} out of @{term analz}.›

lemma analz_Un_Tag:
assumes "Enc_keys_clean H"
shows "analz (Tags ∪ H) ⊆ Tags ∪ analz H"
proof 
  fix X
  assume "X ∈ analz (Tags ∪ H)"
  thus "X ∈ Tags ∪ analz H"
  proof (induction X rule: analz.induct)
    case (Dec Y K') 
    have "Enc Y K' ∈ analz H" using Dec.IH(1) by auto
    moreover have "K' ∈ synth (analz H)" 
    proof -
      have "K' ∈ range LtK ∪ payload" using ‹Enc Y K' ∈ analz H› assms 
        by (auto dest: Enc_keys_clean_analz)
      moreover
      from Dec.IH(2) have "K' ∈ synth (Tags ∪ analz H)" 
        by (auto simp add: Collect_disj_eq dest: synth_Int2)
      moreover
      hence "K' ∈ synth (analz H) ∪ -payload" 
        by (auto dest: synth_payload2 [THEN [2] rev_subsetD]) 
      ultimately show ?thesis by auto
    qed
    ultimately show ?case by (auto)
  next
    case (Adec_eph Y K') 
    thus ?case by (auto dest!: EpriK_synth)
  qed auto
qed 

text ‹Pull the @{term AgentSet} out of the @{term analz}.›

lemma analz_Un_AgentSet:
shows "analz (AgentSet ∪ H) ⊆ AgentSet ∪ analz H"
proof 
  fix X
  assume "X ∈ analz (AgentSet ∪ H)"
  thus "X ∈ AgentSet ∪ analz H"
  proof (induction X rule: analz.induct)
    case (Dec Y K') 
    from Dec.IH(1) have "Enc Y K' ∈ analz H" by auto
    moreover have "K' ∈ synth (analz H)" 
      proof -
        from Dec.IH(2) have "K' ∈ synth (AgentSet ∪ analz H)" 
          by (auto simp add: Collect_disj_eq dest: synth_Int2)
        moreover have "synth (AgentSet ∪ analz H) ⊆ synth (analz H)" 
          by (auto simp add: synth_subset_iff)
        ultimately show ?thesis by auto
    qed
    ultimately show ?case by (auto)
  next
    case (Adec_eph Y K') 
    thus ?case by (auto dest!: EpriK_synth)
  qed auto
qed 

text ‹Pull @{term HashSet} out of @{term analz}.›
lemma analz_Un_HashSet:
assumes "Enc_keys_clean H" and "G ⊆ - payload" 
shows "analz (HashSet G  ∪ H) ⊆ HashSet G ∪ analz H"
proof 
  fix X
  assume "X ∈ analz (HashSet G ∪ H)"
  thus "X ∈ HashSet G ∪ analz H"
  proof (induction X rule: analz.induct)
    case (Dec Y K')
    from Dec.IH(1) have "Enc Y K' ∈ analz H" by auto
    moreover have "K' ∈ synth (analz H)"
    proof -
      have "K' ∈ range LtK ∪ payload" using ‹Enc Y K' ∈ analz H› assms(1)
      by (auto dest: Enc_keys_clean_analz)
      thus ?thesis
      proof
        assume "K' ∈ range LtK"
        then obtain KK where "K' = LtK KK" by auto
        moreover
        with Dec.IH(2) show ?thesis
          by (auto simp add: Collect_disj_eq dest: synth_Int2)
      next
        assume "K' ∈ payload"  
        moreover
        from assms have "HashSet G ∩ payload = {}" by auto
        moreover from Dec.IH(2) have "K' ∈ synth (HashSet G ∪ analz H)" 
          by (auto simp add: Collect_disj_eq dest: synth_Int2)
        ultimately
        have "K' ∈ synth (analz H) ∪ -payload" 
          by (auto dest: synth_payload2 [THEN [2] rev_subsetD])
        with ‹K' ∈ payload› show ?thesis by auto 
      qed
    qed
    ultimately show ?case by auto
  next 
    case (Adec_eph Y K') 
    thus ?case by (auto dest!: EpriK_synth)
  qed (insert assms(2), auto)
qed

end