Theory Implem_lemmas

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

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  Implem_lemmas.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Implem_lemmas.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>
  
  Auxiliary notions and lemmas for channel implementations.
  - message abstraction = inverse of (valid) impl, lifted to sets
  - extractable messages (those of non-confidential and "broken" channels)
  - lemmas for proving L2-L3 intruder refinement

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

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

section ‹Lemmas Following from Channel Message Implementation Assumptions›

theory Implem_lemmas
imports Implem
begin

text ‹These lemmas require the assumptions added in the @{locale "valid_implem"} locale.›

context semivalid_implem
begin
(**************************************************************************************************)
subsection ‹Message implementations and abstractions›
(**************************************************************************************************)

text ‹Abstracting a set of messages into channel messages.›

definition
  abs :: "msg set  chan set"
where
  "abs S  {Chan x A B M | x A B M. M  payload  implem (Chan x A B M)  S}"

lemma absE [elim]: 
  " X  abs H;
      x A B M. X = Chan x A B M  M  payload  implem X  H  P 
   P"
by (auto simp add: abs_def)

lemma absI [intro]: "M  payload  implem (Chan x A B M)  H  Chan x A B M  abs H"
by (auto simp add: abs_def)

lemma abs_mono: "G  H  abs G  abs H"
by (auto simp add: abs_def)

lemmas abs_monotone [simp] = abs_mono [THEN [2] rev_subsetD]

lemma abs_empty [simp]: "abs {} = {}"
by (auto simp add: abs_def)

lemma abs_Un_eq: "abs (G  H) = abs G  abs H"
by (auto simp add: abs_def)

text ‹General lemmas about implementations and @{term abs}.›
lemma abs_insert_payload [simp]: "M  payload  abs (insert M S) = abs S"
by (auto simp add: abs_def)

lemma abs_insert_impl [simp]:
  "M  payload  abs (insert (implem (Chan x A B M)) S) = insert (Chan x A B M) (abs S)"
by (auto simp add: abs_def)

lemma extr_payload [simp, intro]:
  " X  extr Bad NI (abs I); NI  payload   X  payload"
by (erule extr.induct, blast, auto)

lemma abs_Un_LtK:
  "K  range LtK  abs (K  S) = abs S"
by (auto simp add: abs_Un_eq)

lemma abs_Un_keys_of [simp]:
  "abs (keys_of A  S) = abs S"
by (auto intro!: abs_Un_LtK)


text ‹Lemmas about @{term valid} and @{term abs}

lemma abs_validSet: "abs (S  valid) = abs S"
by (auto elim: absE intro: validI)

lemma valid_abs: "M  valid   M'. M'  abs {M}"
by (auto elim: validE)


(**************************************************************************************************)
subsection ‹Extractable messages›
(**************************************************************************************************)

text extractable K I›: subset of messages in $I$ which are implementations 
(not necessarily valid since we do not require that they are payload) and can be extracted 
using the keys in K. It corresponds to L2 @{term extr}.›

definition
  extractable :: "msg set  msg set  msg set"
where
  "extractable K I 
    {implInsec A B M | A B M. implInsec A B M  I} 
    {implAuth A B M | A B M. implAuth A B M  I} 
    {implConfid A B M | A B M. implConfid A B M  I  (A, B)  broken K} 
    {implSecure A B M | A B M. implSecure A B M  I  (A, B)  broken K}"

lemma extractable_red: "extractable K I  I"
by (auto simp add: extractable_def)

lemma extractableI:
  "implem (Chan x A B M)  I 
   x = insec  x = auth  ((x = confid  x = secure)  (A, B)  broken K)    
   implem (Chan x A B M)  extractable K I"
by (auto simp add: extractable_def)

lemma extractableE:
  "X  extractable K I 
   (A B M. X = implInsec A B M  X  I  P) 
   (A B M. X = implAuth A B M  X  I  P) 
   (A B M. X = implConfid A B M  X  I  (A, B)  broken K  P) 
   (A B M. X = implSecure A B M  X  I  (A, B)  broken K  P) 
  P"
by (auto simp add: extractable_def brokenI)

text ‹General lemmas about implementations and extractable.›
lemma implem_extractable [simp]:
  " Keys_bad K Bad; implem (Chan x A B M)  extractable K I; M  payload  
  M  extr Bad NI (abs I)"
by (erule extractableE, auto)


text ‹Auxiliary lemmas about extractable messages: they are implementations.›
lemma valid_extractable [simp]: "I  valid  extractable K I  valid"
by (auto intro: subset_trans extractable_red del: subsetI)

lemma LtKeys_parts_extractable:
  "I  valid  parts (extractable K I)  range LtK = {}"
by (auto dest: valid_extractable intro!: parts_valid_LtKeys_disjoint)

lemma LtKeys_parts_extractable_elt [simp]:  
  "I  valid  LtK ltk  parts (extractable K I)"
by (blast dest: LtKeys_parts_extractable)


lemma LtKeys_parts_implSecureSet:   (* FIX: possibly problematic: not in normal form *)
  "parts (implSecureSet Ag payload)  range LtK = {}"
by (auto intro!: parts_valid_LtKeys_disjoint intro: validI)

lemma LtKeys_parts_implSecureSet_elt: 
  "LtK K  parts (implSecureSet Ag payload)"
using LtKeys_parts_implSecureSet
by auto

lemmas LtKeys_parts = LtKeys_parts_payload parts_valid_LtKeys_disjoint
                      LtKeys_parts_extractable LtKeys_parts_implSecureSet 
                      LtKeys_parts_implSecureSet_elt


subsubsection‹Partition $I$ to keep only the extractable messages›
(**************************************************************************************************)

text ‹Partition the implementation set.›

lemma impl_partition:
  " NI  payload; I  valid  
  I  extractable K I 
      implConfidSet (UNIV - broken K) payload 
      implSecureSet (UNIV - broken K) payload"
by (auto dest!: subsetD [where A=I] elim!: valid_cases intro:  extractableI)


subsubsection ‹Partition of @{term "extractable"}
(**************************************************************************************************)

text ‹We partition the @{term "extractable"} set into insecure, confidential, authentic 
implementations.›

lemma extractable_partition:
  "Keys_bad K Bad; NI  payload; I  valid 
  extractable K I  
  implInsecSet (extr Bad NI (abs I)) 
  implConfidSet UNIV (extr Bad NI (abs I)) 
  implAuthSet (extr Bad NI (abs I)) 
  implSecureSet UNIV (extr Bad NI (abs I))"
apply (rule, frule valid_extractable, drule subsetD [where A="extractable K I"], fast)
apply (erule valid_cases, auto)
done


(**************************************************************************************************)
subsection ‹Lemmas for proving intruder refinement (L2-L3)›
(**************************************************************************************************)

text ‹Chain of lemmas used to prove the refinement for l3_dy›. 
The ultimate goal is to show @{prop [display] 
  "synth (analz (NI  I  K  Tags))  synth (analz (extr Bad NI (abs I)))  -payload"
}

subsubsection ‹First: we only keep the extractable messages›

― ‹the ‹synth› is probably not needed›
lemma analz_NI_I_K_analz_NI_EI:
assumes HNI: "NI  payload"
    and HK: "K  range LtK"
    and HI: "I  valid"
shows "analz (NI  I  K  Tags) 
       synth (analz (NI  extractable K I  K  Tags))  -payload"
proof -
  from HNI HI
  have "analz (NI  I  K  Tags)  
        analz (NI  (extractable K I 
                     implConfidSet (UNIV - broken K) payload 
                     implSecureSet (UNIV - broken K) payload)
                 K  Tags)"
    by (intro analz_mono Un_mono impl_partition, simp_all)
  also have "...  analz (implConfidSet (UNIV - broken K) payload 
                    (implSecureSet (UNIV - broken K) payload 
                    (extractable K I  NI  K  Tags)))"
    by (auto)
  also have "...  synth (analz (implSecureSet (UNIV - broken K) payload 
                  (extractable K I  NI  K  Tags)))  -payload"
    proof (rule analz_Un_implConfidSet_2)
      show "Enc_keys_clean (implSecureSet (UNIV - broken K) payload 
                               (extractable K I  NI  K  Tags))"
        by (auto simp add: HNI HI HK intro: validI)
    next
      from HK HI HNI 
      show "(UNIV - broken K)  
            broken (parts (
              implSecureSet (UNIV - broken K) payload 
              (extractable K I  NI  K  Tags))  range LtK)  = {}"
        by (auto simp add: LtKeys_parts 
               LtKeys_parts_implSecureSet_elt [where Ag="- broken K", simplified])
    qed (auto)
  also have "...  synth (analz (extractable K I  NI  K  Tags))  -payload"
    proof (rule Un_least, rule synth_idem_payload)
      show "analz (implSecureSet (UNIV - broken K) payload  
                   (extractable K I  NI  K  Tags))
             synth (analz (extractable K I  NI  K  Tags))  -payload"
        proof (rule analz_Un_implSecureSet_2)
          show "Enc_keys_clean (extractable K I  NI  K  Tags)"
            using HNI HK HI by auto
        next  
          from HI HK HNI 
          show "(UNIV - broken K)  
                broken (parts (extractable K I  NI  K  Tags)  range LtK) = {}"
          by (auto simp add: LtKeys_parts)
        qed (auto)
    next
      show "-payload  synth (analz (extractable K I  NI  K  Tags))  -payload"
        by auto
    qed
  also have "...  synth (analz (NI  extractable K I  K  Tags))  -payload"
    by (simp add: sup.left_commute sup_commute)
  finally show ?thesis .
qed


subsubsection ‹Only keep the extracted messages (instead of extractable)›
(**************************************************************************************************)

lemma analz_NI_EI_K_synth_analz_NI_E_K:
assumes HNI: "NI  payload"
    and HK: "K  range LtK"
    and HI: "I  valid"
    and Hbad: "Keys_bad K Bad"
shows "analz (NI  extractable K I  K  Tags)
     synth (analz (extr Bad NI (abs I)  K  Tags))  -payload"
proof -
  from HNI HI Hbad
  have "analz (NI  extractable K I  K  Tags)  
        analz (NI  (implInsecSet (extr Bad NI (abs I)) 
                     implConfidSet UNIV (extr Bad NI (abs I)) 
                     implAuthSet (extr Bad NI (abs I)) 
                     implSecureSet UNIV (extr Bad NI (abs I))) 
                    K  Tags)"
    by (intro analz_mono Un_mono extractable_partition) (auto)

  also have "...  analz (implInsecSet (extr Bad NI (abs I)) 
                     (implConfidSet UNIV (extr Bad NI (abs I)) 
                     (implAuthSet (extr Bad NI (abs I)) 
                     (implSecureSet UNIV (extr Bad NI (abs I)) 
                     (NI  K  Tags)))))"
    by (auto)
  also have "...  synth (analz (extr Bad NI (abs I) 
                   (implConfidSet UNIV (extr Bad NI (abs I)) 
                   (implAuthSet (extr Bad NI (abs I)) 
                   (implSecureSet UNIV (extr Bad NI (abs I))  (NI  K  Tags)))))) 
                  -payload"
    by (rule analz_Un_implInsecSet)
       (auto simp only: Un_commute [of "extr _ _ _" _] Un_assoc Un_absorb, 
        auto simp add: HNI HK HI intro!: validI)
  also have "...  synth (analz (extr Bad NI (abs I) 
                   (implAuthSet (extr Bad NI (abs I)) 
                   (implSecureSet UNIV (extr Bad NI (abs I))  (NI  K  Tags))))) 
                  -payload"
    proof (rule Un_least, rule synth_idem_payload)
      have "analz (implConfidSet UNIV (extr Bad NI (abs I)) 
                   (implAuthSet (extr Bad NI (abs I)) 
                   (implSecureSet UNIV (extr Bad NI (abs I))  
                   (NI  (K  extr Bad NI (abs I)  Tags)))))
             synth (analz (extr Bad NI (abs I) 
                           (implAuthSet (extr Bad NI (abs I)) 
                           (implSecureSet UNIV (extr Bad NI (abs I))  
                           (NI  (K  extr Bad NI (abs I)  Tags)))))) 
               -payload"
        by (rule analz_Un_implConfidSet)
           (auto simp only: Un_commute [of "extr _ _ _" _] Un_assoc Un_absorb,
            auto simp add: HK HI HNI  intro!: validI)
      then show "analz (extr Bad NI (abs I) 
                        (implConfidSet UNIV (extr Bad NI (abs I)) 
                        (implAuthSet (extr Bad NI (abs I)) 
                        (implSecureSet UNIV (extr Bad NI (abs I))  (NI  K  Tags)))))
                  synth (analz (extr Bad NI (abs I) 
                         (implAuthSet (extr Bad NI (abs I)) 
                         (implSecureSet UNIV (extr Bad NI (abs I))  
                         (NI  K  Tags))))) 
                    -payload"
        by (simp add: inf_sup_aci(6) inf_sup_aci(7))
    next
      show "-payload
             synth (analz (extr Bad NI (abs I) 
                           (implAuthSet (extr Bad NI (abs I)) 
                           (implSecureSet UNIV (extr Bad NI (abs I))  (NI  K  Tags))))) 
               -payload"
        by blast
    qed
  also have "...  synth (analz (extr Bad NI (abs I) 
                   (implSecureSet UNIV (extr Bad NI (abs I))  (NI  K  Tags)))) 
                  -payload"
    proof (rule Un_least, rule synth_idem_payload)
      have "analz (implAuthSet (extr Bad NI (abs I)) 
                   (implSecureSet UNIV (extr Bad NI (abs I))  
                   (NI  (K  (extr Bad NI (abs I)  Tags)))))
             synth (analz (extr Bad NI (abs I) 
                           (implSecureSet UNIV (extr Bad NI (abs I))  
                           (NI  (K  (extr Bad NI (abs I)  Tags)))))) 
               -payload"
        by (rule analz_Un_implAuthSet)
           (auto simp only: Un_commute [of "extr _ _ _" _] Un_assoc Un_absorb,
            auto simp add: HI HNI HK intro!: validI)
      then show "analz (extr Bad NI (abs I) 
                        (implAuthSet (extr Bad NI (abs I)) 
                        (implSecureSet UNIV (extr Bad NI (abs I))  (NI  K  Tags))))
                  synth (analz (extr Bad NI (abs I) 
                         (implSecureSet UNIV (extr Bad NI (abs I))  
                         (NI  K  Tags)))) 
                    -payload"
        by (simp add: inf_sup_aci(6) inf_sup_aci(7))
    next
      show "-payload
             synth (analz (extr Bad NI (abs I) 
                           (implSecureSet UNIV (extr Bad NI (abs I)) 
                             (NI  K  Tags))))  
               -payload"
        by blast
    qed
  also have "...  synth (analz (extr Bad NI (abs I)  (NI  K  Tags))) 
                  -payload"
    proof (rule Un_least, rule synth_idem_payload)
      have "analz (implSecureSet UNIV (extr Bad NI (abs I))  
                   (NI  (K  (extr Bad NI (abs I)  Tags))))
             synth (analz (extr Bad NI (abs I) 
                           (NI  (K  (extr Bad NI (abs I)  Tags))))) 
                -payload"
        by (rule analz_Un_implSecureSet)
           (auto simp only: Un_commute [of "extr _ _ _" _] Un_assoc Un_absorb,
            auto simp add: HI HNI HK intro!: validI)
      then show "analz (extr Bad NI (abs I) 
                        (implSecureSet UNIV (extr Bad NI (abs I))  (NI  K  Tags)))
                  synth (analz (extr Bad NI (abs I)  (NI  K  Tags))) 
                    -payload"
        by (simp add: inf_sup_aci(6) inf_sup_aci(7))
    next
      show "-payload
             synth (analz (extr Bad NI (abs I) (NI  K  Tags))) 
               -payload"
        by blast
    qed
  also have "...  synth (analz (extr Bad NI (abs I)  K  Tags))  -payload"
    by (metis IK_subset_extr inf_sup_aci(6) set_eq_subset sup.absorb1)
  finally show ?thesis .
qed


subsubsection ‹Keys and Tags can be moved out of the @{term "analz"}

lemma analz_LtKeys_Tag:
assumes "NI  payload" and "K  range LtK"
shows "analz (NI  K  Tags)  analz NI  K  Tags"
proof 
  fix X
  assume H: "X  analz (NI  K  Tags) "
  thus "X  analz NI  K  Tags" 
  proof (induction X rule: analz.induct)
    case (Dec X Y) 
    hence "Enc X Y  payload" using assms by auto
    moreover
    from Dec.IH(2) have "Y  synth (analz NI  (K  Tags))"
      by (auto simp add: Collect_disj_eq dest!: synth_Int2 )
    ultimately show ?case using Dec.IH(1) assms(2) 
      by (auto dest!: synth_payload [THEN [2] rev_subsetD])
  next
    case (Adec_lt X Y)
    hence "Aenc X (pubK Y)  payload  range LtK  Tags" using assms
      by auto
    then show ?case by auto
  next
    case (Sign_getmsg X Y)
    hence "Sign X (priK Y)  payload  range LtK  Tags" using assms by auto
    then show ?case by auto
  next
    case (Adec_eph X Y)
    then show ?case using assms by (auto dest!: EpriK_synth)
  qed (insert assms, auto)
qed

lemma analz_NI_E_K_analz_NI_E:
  " NI  payload; K  range LtK; I  valid  
  analz (extr Bad NI (abs I)  K  Tags)  analz (extr Bad NI (abs I))  K  Tags"
by (rule analz_LtKeys_Tag) auto


subsubsection ‹Final lemmas, using all the previous ones›
(**************************************************************************************************)

lemma analz_NI_I_K_synth_analz_NI_E:
assumes
  Hbad: "Keys_bad K Bad" and 
  HNI: "NI  payload" and 
  HK:  "K  range LtK" and 
  HI: "I  valid"
shows 
  "analz (NI  I  K  Tags)  synth (analz (extr Bad NI (abs I)))  -payload"
proof -
  from HNI HK HI have "analz (NI  I  K  Tags) 
        synth (analz (NI  extractable K I  K  Tags))  -payload"
    by (rule analz_NI_I_K_analz_NI_EI)
  also have "...  synth (analz (extr Bad NI (abs I)  K  Tags))  -payload"
    proof (rule Un_least, simp_all)
      from Hbad HNI HK HI have "analz (NI  extractable K I  K  Tags) 
            synth (analz (extr Bad NI (abs I)  K  Tags))  -payload"
        by (intro analz_NI_EI_K_synth_analz_NI_E_K)
      then show "synth (analz (NI  extractable K I  K  Tags)) 
                 synth (analz (extr Bad NI (abs I)  K  Tags))  -payload"
        by (rule synth_idem_payload)
    qed
  also have "...  synth (analz (extr Bad NI (abs I)))  -payload"
    proof (rule Un_least, simp_all)
      from HNI HK HI have "analz (extr Bad NI (abs I)  K  Tags) 
                           analz (extr Bad NI (abs I))  K  Tags"
        by (rule analz_NI_E_K_analz_NI_E)
      also from HK have "...  analz (extr Bad NI (abs I))  -payload"
        by auto
      also have "...  synth (analz (extr Bad NI (abs I)))  -payload"
        by auto
      finally show "synth (analz (extr Bad NI (abs I)  K  Tags)) 
                  synth (analz (extr Bad NI (abs I)))  -payload"
        by (rule synth_idem_payload)
    qed
  finally show ?thesis .
qed


text ‹Lemma actually used to prove the refinement.›
lemma synth_analz_NI_I_K_synth_analz_NI_E:
  " Keys_bad K Bad; NI  payload; K  range LtK; I  valid
  synth (analz (NI  I  K  Tags)) 
    synth (analz (extr Bad NI (abs I)))  -payload"
by (intro synth_idem_payload analz_NI_I_K_synth_analz_NI_E) (assumption+)


subsubsection ‹Partitioning @{term "analz (ik)"}
(**************************************************************************************************)
text ‹Two lemmas useful for proving the invariant
  @{term [display] "analz ik  synth (analz (ik  payload  ik  valid  ik  range LtK  Tags))"}

lemma analz_Un_partition:
  "analz S  synth (analz ((S  payload)  (S  valid)  (S  range LtK)  Tags)) 
  H  payload  valid  range LtK 
  analz (H  S) 
    synth (analz (((H  S)  payload)  ((H  S)  valid)  ((H  S)  range LtK)  Tags))"
proof -
  assume "H  payload  valid  range LtK"
  then have HH:"H = (H  payload)  (H  valid)  (H  range LtK)"
    by auto
  assume HA:
    "analz S  synth (analz ((S  payload)  (S  valid)  (S  range LtK)  Tags))"
  then have 
   "analz (H  S)  
    synth (analz (H  ((S  payload)  (S  valid)  (S  range LtK)  Tags)))"
    by (rule analz_synth_subset_Un2)
  also with HH have 
    "...  synth (analz (((H  payload)  (H  valid)  (H  range LtK))  
                         ((S  payload)  (S  valid)  (S  range LtK)  Tags)))"
    by auto
  also have "... = synth (analz (((H  S)  payload)  ((H  S)  valid)  
                                 ((H  S)  range LtK)  Tags))"
    by (simp add: Un_left_commute sup.commute Int_Un_distrib2)
  finally show ?thesis .
qed

lemma analz_insert_partition:
  "analz S  synth (analz ((S  payload)  (S  valid)  (S  range LtK)  Tags)) 
  x  payload  valid  range LtK 
  analz (insert x S) 
    synth (analz (((insert x S)  payload)  ((insert x S)  valid)  
                  ((insert x S)  range LtK)  Tags))"
by (simp only: insert_is_Un [of x S], erule analz_Un_partition, auto)

end
end