Theory Implem

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

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  Implem.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Implem.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>
  
  Parametric channel message implementation
  - definition of 'valid' implementations
  - assumptions for channel implementations (formulated as locales)

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

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

section ‹Assumptions for Channel Message Implementation›

text ‹We define a series of locales capturing our assumptions on channel message 
implementations.›

theory Implem
imports Channels Payloads
begin

subsection ‹First step: basic implementation locale›
(**************************************************************************************************)

text ‹This locale has no assumptions, it only fixes an implementation function and 
defines some useful abbreviations (impl*, impl*Set) and valid›.
›

locale basic_implem =
  fixes implem :: "chan  msg"
begin

abbreviation "implInsec A B M  implem (Insec A B M)"
abbreviation "implConfid A B M  implem (Confid A B M)"
abbreviation "implAuth A B M  implem (Auth A B M)"
abbreviation "implSecure A B M  implem (Secure A B M)"

abbreviation implInsecSet :: "msg set  msg set"
where "implInsecSet G  {implInsec A B M | A B M. M  G}"

abbreviation implConfidSet :: "(agent * agent) set  msg set  msg set"
where "implConfidSet Ag G  {implConfid A B M | A B M.  (A, B)  Ag  M  G}"

abbreviation implAuthSet :: "msg set  msg set"
where "implAuthSet G  {implAuth A B M | A B M. M  G}"

abbreviation implSecureSet :: "(agent * agent) set  msg set  msg set"
where "implSecureSet Ag G  {implSecure A B M | A B M. (A, B)  Ag  M  G}"

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

lemma validI:
  "M  payload  implem (Chan x A B M)  valid"
by (auto simp add: valid_def)

lemma validE:
  "X  valid  ( x A B M. X = implem (Chan x A B M)  M  payload  P)  P"
by (auto simp add: valid_def)

lemma valid_cases:
fixes X P
assumes "X  valid"
        "(A B M. X = implInsec A B M  M  payload  P)"
        "(A B M. X = implConfid A B M  M  payload  P)"
        "(A B M. X = implAuth A B M  M  payload  P)"
        "(A B M. X = implSecure A B M  M  payload  P)"
shows "P"
proof -
  from assms have "( x A B M. X = implem (Chan x A B M)  M  payload  P)  P"
  by (auto elim: validE)
  moreover from assms have " x A B M. X = implem (Chan x A B M)  M  payload  P"
    proof -
      fix x A B M
      assume "X = implem (Chan x A B M)" "M  payload"
      with assms show "P" by (cases x, auto)
    qed
  ultimately show ?thesis .
qed

end

subsection ‹Second step: basic and analyze assumptions›
(**************************************************************************************************)

text ‹This locale contains most of the assumptions on implem, i.e.:
\begin{itemize}
\item impl_inj›: injectivity
\item parts_impl_inj›: injectivity through parts
\item Enc_parts_valid_impl›: if Enc X Y appears in parts of an implem, then it is 
  in parts of the payload, or the key is either long term or payload
\item impl_composed›: the implementations are composed (not nonces, agents, tags etc.)
\item analz_Un_implXXXSet›: move the impl*Set out of the analz (only keep the payloads)
\item impl_Impl›: implementations contain implementation material
\item LtK_parts_impl›: no exposed long term keys in the implementations 
  (i.e., they are only used as keys, or under hashes)
\end{itemize}
›

locale semivalid_implem = basic_implem +
― ‹injectivity›
assumes impl_inj:
  "implem (Chan x A B M) = implem (Chan x' A' B' M') 
    x = x'  A = A'  B = B'  M = M'"
― ‹implementations and parts›
and parts_impl_inj:
  "M'  payload 
   implem (Chan x A B M)  parts {implem (Chan x' A' B' M')}  
   x = x'  A = A'  B = B'  M = M'"
and Enc_keys_clean_valid: "I  valid  Enc_keys_clean I"
and impl_composed: "composed (implem Z)"
and impl_Impl: "implem (Chan x A B M)  payload"
― ‹no ltk in the parts of an implementation›
and LtK_parts_impl: "X  valid  LtK K  parts {X}"

― ‹analyze assumptions:›
and analz_Un_implInsecSet:
  " G  payload; Enc_keys_clean H  
  analz (implInsecSet G  H)  synth (analz (G  H))  -payload"
and analz_Un_implConfidSet:
  " G  payload; Enc_keys_clean H  
  analz (implConfidSet Ag G  H)  synth (analz (G  H))  -payload"
and analz_Un_implConfidSet_2:
  " G  payload; Enc_keys_clean H; Ag  broken (parts H  range LtK) = {} 
  analz (implConfidSet Ag G  H)  synth (analz H)  -payload"
and analz_Un_implAuthSet:
  " G  payload; Enc_keys_clean H 
  analz (implAuthSet G  H)  synth (analz (G  H))  -payload"
and analz_Un_implSecureSet:
  " G  payload; Enc_keys_clean H 
  analz (implSecureSet Ag G  H)  synth (analz (G  H))  -payload"
and analz_Un_implSecureSet_2:
  " G  payload; Enc_keys_clean H; Ag  broken (parts H  range LtK) = {} 
  analz (implSecureSet Ag G  H)  synth (analz H)  -payload"

begin
― ‹declare some attributes and abbreviations for the hypotheses›
― ‹and prove some simple consequences of the hypotheses›
declare impl_inj [simp]

lemmas parts_implE [elim] = parts_impl_inj [rotated 1]

declare impl_composed [simp, intro]

lemma composed_arg_cong: "X = Y  composed X  composed Y"
by (rule arg_cong)

lemma implem_Tags_aux: "implem (Chan x A B M)  Tags" by (cases x, auto dest: composed_arg_cong)
lemma implem_Tags [simp]: "implem x  Tags" by (cases x, auto simp add: implem_Tags_aux)
lemma implem_LtK_aux: "implem (Chan x A B M)  LtK K" by (cases x, auto dest: composed_arg_cong)
lemma implem_LtK [simp]: "implem x  LtK K" by (cases x, auto simp add: implem_LtK_aux)
lemma implem_LtK2 [simp]: "implem x  range LtK" by (cases x, auto simp add: implem_LtK_aux)

declare impl_Impl [simp]

lemma LtK_parts_impl_insert:
  "LtK K  parts (insert (implem (Chan x A B M)) S)  M  payload  LtK K  parts S"
apply (simp add: parts_insert [of _ S], clarify)
apply (auto dest: validI LtK_parts_impl)
done


declare LtK_parts_impl_insert [dest]
declare Enc_keys_clean_valid [simp, intro]

lemma valid_composed [simp,dest]: "M  valid  composed M"
by (auto elim: validE)

― ‹lemmas: valid/payload are mutually exclusive›
lemma valid_payload [dest]: " X  valid; X  payload   P"
by (auto elim!: validE)
    
― ‹valid/LtK are mutually exclusive›
lemma valid_isLtKey [dest]: " X  valid; X  range LtK   P"
by (auto)

lemma analz_valid:
  "H  payload  valid  range LtK  Tags 
   implem (Chan x A B M)  analz H 
   implem (Chan x A B M)  H"
apply (drule analz_into_parts, 
       drule parts_monotone [of _ H "payload  H  valid  range LtK  Tags"], auto)
apply (drule parts_singleton, auto elim!:validE dest: parts_impl_inj)
done

lemma parts_valid_LtKeys_disjoint:
  "I  valid  parts I  range LtK = {}"
apply (safe, drule parts_singleton, clarsimp)
apply (auto dest: subsetD LtK_parts_impl)
done

lemma analz_LtKeys:
  "H  payload  valid  range LtK  Tags 
   analz H  range LtK  H"
apply auto
apply (drule analz_into_parts, drule parts_monotone [of _ H "payload  valid  H  range LtK  Tags"], auto)
apply (drule parts_singleton, auto elim!:validE dest: parts_impl_inj)
done

end


subsection ‹Third step: valid_implem›
(**************************************************************************************************)

text ‹This extends @{locale "semivalid_implem"} with four new assumptions, which under certain 
  conditions give information on $A$, $B$, $M$ when @{term "implXXX A B M  synth (analz Z)"}.
  These assumptions are separated because interpretations are more easily proved, if the 
  conclusions that follow from the @{locale "semivalid_implem"} assumptions are already 
  available.
›

locale valid_implem = semivalid_implem +

― ‹Synthesize assumptions: conditions on payloads $M$ implied by derivable›
― ‹channel messages with payload $M$.›
assumes implInsec_synth_analz:
  "H  payload  valid  range LtK  Tags 
   implInsec A B M  synth (analz H) 
   implInsec A B M  H  M  synth (analz H)"
and implConfid_synth_analz:
  "H  payload  valid  range LtK  Tags 
   implConfid A B M  synth (analz H) 
   implConfid A B M  H  M  synth (analz H)"
and implAuth_synth_analz:
  "H  payload  valid  range LtK  Tags 
   implAuth A B M  synth (analz H) 
   implAuth A B M  H  (M  synth (analz H)  (A, B)  broken H)"
and implSecure_synth_analz:
  "H  payload  valid  range LtK  Tags 
   implSecure A B M  synth (analz H) 
   implSecure A B M  H  (M  synth (analz H)  (A, B)  broken H)"

end