Theory CompLocalSecrets

(*
   Title:  Theory  CompLocalSecrets.thy
   Author: Maria Spichkova <maria.spichkova at rmit.edu.au>, 2014
*)
section ‹Local Secrets of a component›

theory CompLocalSecrets
imports Secrecy 
begin

― ‹Set of local secrets: the set of secrets which does not belong to›
― ‹the set of private keys and unguessable values, but are transmitted›
― ‹via local channels or belongs to the local secrets of its subcomponents›
axiomatization
  LocalSecrets :: "specID  ⇒ KS set"
where
LocalSecretsDef:
 "LocalSecrets A =
  {(m :: KS). m ∉ specKeysSecrets A  ∧ 
              ((∃ x y. ((x ∈ loc A) ∧ m = (kKS y) ∧ (exprChannel x (kE y)))) 
              |(∃ x z. ((x ∈ loc A) ∧ m = (sKS z) ∧ (exprChannel x (sE z)) )) )} 
   ∪  (⋃ (LocalSecrets ` (subcomponents A) ))"

lemma LocalSecretsComposition1:
assumes "ls ∈ LocalSecrets P"
       and "subcomponents PQ = {P, Q}"
shows    "ls ∈ LocalSecrets PQ"
using assms by (simp (no_asm) only: LocalSecretsDef, auto)

lemma  LocalSecretsComposition_exprChannel_k:
assumes "exprChannel x (kE Keys)"
       and "¬ ine P (kE Keys)"
       and "¬ ine Q (kE Keys)"
       and "¬ (x ∉ ins P ∧ x ∉ ins Q)"
shows "False"
using assms by (metis ine_def)

lemma  LocalSecretsComposition_exprChannel_s:
assumes "exprChannel x (sE Secrets)"
       and "¬ ine P (sE Secrets)"
       and "¬ ine Q (sE Secrets)"
       and "¬ (x ∉ ins P ∧ x ∉ ins Q)"
shows "False"
using assms by (metis ine_ins_neg1)

lemma LocalSecretsComposition_neg1_k:
assumes "subcomponents PQ = {P, Q}"
       and "correctCompositionLoc PQ"
       and "¬ ine P (kE Keys)"
       and "¬ ine Q (kE Keys)"
       and "kKS Keys ∉ LocalSecrets P"
       and "kKS Keys ∉ LocalSecrets Q"
shows    "kKS Keys ∉ LocalSecrets PQ"
proof - 
  from assms show ?thesis 
    apply (simp (no_asm) only: LocalSecretsDef, 
           simp add: correctCompositionLoc_def, clarify)
    by (rule LocalSecretsComposition_exprChannel_k, auto)
qed

lemma LocalSecretsComposition_neg_k:
assumes "subcomponents PQ = {P,Q}"
       and "correctCompositionLoc PQ"
       and "correctCompositionKS PQ"
       and "(kKS m) ∉ specKeysSecrets P"
       and "(kKS m) ∉ specKeysSecrets Q"
       and "¬ ine P (kE m)"
       and "¬ ine Q (kE m)"
       and "(kKS m) ∉ ((LocalSecrets P) ∪ (LocalSecrets Q))"
shows    "(kKS m) ∉ (LocalSecrets PQ)"
proof -
  from assms show ?thesis 
    apply (simp (no_asm) only: LocalSecretsDef, 
           simp add: correctCompositionLoc_def, clarify)
    by (rule LocalSecretsComposition_exprChannel_k, auto)
qed  

lemma LocalSecretsComposition_neg_s:
assumes subPQ:"subcomponents PQ = {P,Q}"
       and cCompLoc:"correctCompositionLoc PQ"
       and cCompKS:"correctCompositionKS PQ"
       and notKSP:"(sKS m) ∉ specKeysSecrets P"
       and notKSQ:"(sKS m) ∉ specKeysSecrets Q"
       and "¬ ine P (sE m)"
       and "¬ ine Q (sE m)"
       and notLocSeqPQ:"(sKS m) ∉ ((LocalSecrets P) ∪ (LocalSecrets Q))"
shows   "(sKS m) ∉ (LocalSecrets PQ)"
proof -
  from subPQ and cCompKS and notKSP and notKSQ
  have sg1:"sKS m ∉ specKeysSecrets PQ"
    by (simp add: correctCompositionKS_neg1) 
  from subPQ and cCompLoc and notLocSeqPQ have sg2:
   "sKS m ∉  ⋃ (LocalSecrets ` subcomponents PQ)"
    by simp
  from sg1 and sg2 and assms show ?thesis 
    apply (simp (no_asm) only: LocalSecretsDef, 
           simp add: correctCompositionLoc_def, clarify)
    by (rule LocalSecretsComposition_exprChannel_s, auto)
qed  

lemma LocalSecretsComposition_neg:
assumes "subcomponents PQ = {P,Q}" 
       and "correctCompositionLoc PQ" 
       and "correctCompositionKS PQ"
       and "ks ∉ specKeysSecrets P"
       and "ks ∉ specKeysSecrets Q"
       and h1:"∀ m. ks = kKS m ⟶ (¬ ine P (kE m) ∧ ¬ ine Q (kE m))"
       and h2:"∀ m. ks = sKS m ⟶ (¬ ine P (sE m) ∧ ¬ ine Q (sE m))"
       and "ks ∉ ((LocalSecrets P) ∪ (LocalSecrets Q))"
shows   "ks ∉ (LocalSecrets PQ)"
proof (cases "ks")
  fix m
  assume a1:"ks = kKS m"
  from this and h1 have "¬ ine P (kE m) ∧ ¬ ine Q (kE m)" by simp
  from this and a1 and assms show ?thesis
    by (simp add: LocalSecretsComposition_neg_k)
next
  fix m
  assume a2:"ks = sKS m"
  from this and h2 have "¬ ine P (sE m) ∧ ¬ ine Q (sE m)" by simp
  from this and a2 and assms show ?thesis
    by (simp add: LocalSecretsComposition_neg_s)
qed

lemma LocalSecretsComposition_neg1_s:
assumes "subcomponents PQ = {P, Q}"
       and "correctCompositionLoc PQ"
       and "¬ ine P (sE s)"
       and "¬ ine Q (sE s)"
       and "sKS s ∉ LocalSecrets P" 
       and "sKS s ∉ LocalSecrets Q"
shows    "sKS s ∉ LocalSecrets PQ"
proof - 
  from assms have 
   "sKS s ∉  ⋃ (LocalSecrets ` subcomponents PQ)"
    by simp
    from  assms and this show ?thesis 
    apply (simp (no_asm) only: LocalSecretsDef, 
              simp add: correctCompositionLoc_def, clarify)
    by (rule LocalSecretsComposition_exprChannel_s, auto)
qed  

lemma LocalSecretsComposition_neg1:
assumes "subcomponents PQ = {P, Q}"
       and "correctCompositionLoc PQ"
       and h1:"∀ m. ks = kKS m ⟶ (¬ ine P (kE m) ∧ ¬ ine Q (kE m))" 
       and h2:"∀ m. ks = sKS m ⟶ (¬ ine P (sE m) ∧ ¬ ine Q (sE m))"
       and "ks ∉ LocalSecrets P"
       and "ks ∉ LocalSecrets Q"
shows    "ks ∉ LocalSecrets PQ"
proof (cases "ks")
  fix m
  assume a1:"ks = kKS m"
  from this and h1 have "¬ ine P (kE m) ∧ ¬ ine Q (kE m)" by simp
  from this and a1 and assms show ?thesis 
    by (simp add: LocalSecretsComposition_neg1_k)
next
  fix m
  assume a2:"ks = sKS m"
  from this and h2 have "¬ ine P (sE m) ∧ ¬ ine Q (sE m)" by simp
  from this and a2 and assms show ?thesis 
    by (simp add: LocalSecretsComposition_neg1_s)
qed

lemma LocalSecretsComposition_ine1_k:
assumes "kKS k ∈ LocalSecrets PQ" 
       and "subcomponents PQ = {P, Q}"
       and "correctCompositionLoc PQ" 
       and "¬ ine Q (kE k)"
       and "kKS k ∉ LocalSecrets P"
       and "kKS k ∉ LocalSecrets Q"
shows    "ine P (kE k)"
using assms by (metis LocalSecretsComposition_neg1_k)

lemma LocalSecretsComposition_ine1_s:
assumes "sKS s ∈ LocalSecrets PQ" 
       and "subcomponents PQ = {P, Q}"
       and "correctCompositionLoc PQ" 
       and "¬ ine Q (sE s)"
       and "sKS s ∉ LocalSecrets P"
       and "sKS s ∉ LocalSecrets Q"
shows    "ine P (sE s)"
using assms by (metis LocalSecretsComposition_neg1_s)

lemma LocalSecretsComposition_ine2_k:
assumes "kKS k ∈ LocalSecrets PQ"
       and "subcomponents PQ = {P, Q}"
       and "correctCompositionLoc PQ"
       and "¬ ine P (kE k)"
       and "kKS k ∉ LocalSecrets P"
       and "kKS k ∉ LocalSecrets Q"
shows   "ine Q (kE k)" 
using assms  by (metis LocalSecretsComposition_ine1_k)

lemma LocalSecretsComposition_ine2_s:
assumes "sKS s ∈ LocalSecrets PQ" 
       and "subcomponents PQ = {P, Q}"
       and "correctCompositionLoc PQ"
       and "¬ ine P (sE s)"
       and "sKS s ∉ LocalSecrets P"
       and "sKS s ∉ LocalSecrets Q"
shows    "ine Q (sE s)"
using assms by (metis LocalSecretsComposition_ine1_s)

lemma LocalSecretsComposition_neg_loc_k:
assumes "kKS key ∉ LocalSecrets P"
       and "exprChannel ch (kE key)"
       and "kKS key ∉ specKeysSecrets P"
shows    "ch ∉ loc P"
using assms by (simp only: LocalSecretsDef, auto)

lemma LocalSecretsComposition_neg_loc_s:
assumes "sKS secret ∉ LocalSecrets P"
       and "exprChannel ch (sE secret)"
       and "sKS secret ∉ specKeysSecrets P"
shows    "ch ∉ loc P"
using assms by (simp only: LocalSecretsDef, auto)

lemma correctCompositionKS_exprChannel_k_P:
assumes "subcomponents PQ = {P,Q}" 
       and "correctCompositionKS PQ"
       and "kKS key ∉ LocalSecrets PQ"
       and "ch ∈ ins P"
       and "exprChannel ch (kE key)"
       and "kKS key ∉ specKeysSecrets PQ"
       and "correctCompositionIn PQ"
shows    "ch ∈ ins PQ ∧ exprChannel ch (kE key)"
using assms
by (metis LocalSecretsComposition_neg_loc_k correctCompositionIn_L1)

lemma correctCompositionKS_exprChannel_k_Pex:
assumes "subcomponents PQ = {P,Q}" 
       and "correctCompositionKS PQ"
       and "kKS key ∉ LocalSecrets PQ"
       and "ch ∈ ins P"
       and "exprChannel ch (kE key)"
       and "kKS key ∉ specKeysSecrets PQ"
       and "correctCompositionIn PQ"
shows    "∃ch. ch ∈ ins PQ ∧ exprChannel ch (kE key)"
using assms
by (metis correctCompositionKS_exprChannel_k_P)

lemma correctCompositionKS_exprChannel_k_Q:
assumes "subcomponents PQ = {P,Q}" 
       and "correctCompositionKS PQ"
       and "kKS key ∉ LocalSecrets PQ"
       and "ch ∈ ins Q"
       and h1:"exprChannel ch (kE key)"
       and "kKS key ∉ specKeysSecrets PQ"
       and "correctCompositionIn PQ"
shows    "ch ∈ ins PQ ∧ exprChannel ch (kE key)"
proof - 
  from assms have "ch ∉ loc PQ" 
    by (simp add: LocalSecretsComposition_neg_loc_k)
  from this and assms have "ch ∈ ins PQ" 
    by (simp add: correctCompositionIn_def) 
  from this and h1 show ?thesis by simp
qed

lemma correctCompositionKS_exprChannel_k_Qex:
assumes "subcomponents PQ = {P,Q}" 
        and "correctCompositionKS PQ"
        and "kKS key ∉ LocalSecrets PQ"
        and "ch ∈ ins Q"
        and "exprChannel ch (kE key)"
        and "kKS key ∉ specKeysSecrets PQ"
        and "correctCompositionIn PQ"
shows    "∃ch. ch ∈ ins PQ ∧ exprChannel ch (kE key)"
using assms
by (metis correctCompositionKS_exprChannel_k_Q)

lemma correctCompositionKS_exprChannel_s_P:
assumes "subcomponents PQ = {P,Q}" 
       and "correctCompositionKS PQ"
       and "sKS secret ∉ LocalSecrets PQ"
       and "ch ∈ ins P"
       and "exprChannel ch (sE secret)"
       and "sKS secret ∉ specKeysSecrets PQ"
       and "correctCompositionIn PQ"
shows    "ch ∈ ins PQ ∧ exprChannel ch (sE secret)"
using assms
by (metis LocalSecretsComposition_neg_loc_s correctCompositionIn_L1)

lemma correctCompositionKS_exprChannel_s_Pex:
assumes "subcomponents PQ = {P,Q}" 
       and "correctCompositionKS PQ"
       and "sKS secret ∉ LocalSecrets PQ"
       and "ch ∈ ins P"
       and "exprChannel ch (sE secret)"
       and "sKS secret ∉ specKeysSecrets PQ"
       and "correctCompositionIn PQ"
shows    "∃ch. ch ∈ ins PQ ∧ exprChannel ch (sE secret)"
using assms  
by (metis correctCompositionKS_exprChannel_s_P)

lemma correctCompositionKS_exprChannel_s_Q:
assumes "subcomponents PQ = {P,Q}" 
       and "correctCompositionKS PQ"
       and "sKS secret ∉ LocalSecrets PQ"
       and "ch ∈ ins Q"
       and h1:"exprChannel ch (sE secret)"
       and "sKS secret ∉ specKeysSecrets PQ"
       and "correctCompositionIn PQ"
shows    "ch ∈ ins PQ ∧ exprChannel ch (sE secret)"
proof - 
  from assms have "ch ∉ loc PQ" 
    by (simp add: LocalSecretsComposition_neg_loc_s)
  from this and assms have "ch ∈ ins PQ" 
    by (simp add: correctCompositionIn_def) 
  from this and h1 show ?thesis by simp
qed

lemma correctCompositionKS_exprChannel_s_Qex:
assumes "subcomponents PQ = {P,Q}" 
       and "correctCompositionKS PQ"
       and "sKS secret ∉ LocalSecrets PQ"
       and "ch ∈ ins Q"
       and "exprChannel ch (sE secret)"
       and "sKS secret ∉ specKeysSecrets PQ"
       and "correctCompositionIn PQ"
shows    "∃ch. ch ∈ ins PQ ∧ exprChannel ch (sE secret)"
using assms
by (metis correctCompositionKS_exprChannel_s_Q)

end