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) 


subsectionkeys_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