Theory Channels

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

  Project: Development of Security Protocols by Refinement

  Module:  Refinement/Channels.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Channels.thy 132773 2016-12-09 15:30:22Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Channel messages for Level 2 protocols

  Copyright (c) 2009-2016 Christoph Sprenger 
  Licence: LGPL

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

section ‹Channel Messages›

theory Channels imports Atoms
begin

(******************************************************************************)
subsection ‹Channel messages›
(******************************************************************************)

datatype secprop = auth | confid

type_synonym 
  chtyp = "secprop set"

abbreviation 
  secure :: chtyp where
  "secure ≡ {auth, confid}"

datatype payload = Msg "atom list"
 
datatype chmsg = 
  StatCh "chtyp" "agent" "agent" "payload"
| DynCh "chtyp" "key" "payload" 


text ‹Abbreviations for use in protocol defs›

abbreviation 
  Insec :: "[agent, agent, payload] ⇒ chmsg" where
  "Insec ≡ StatCh {}"

abbreviation 
  Confid :: "[agent, agent, payload] ⇒ chmsg" where
  "Confid ≡ StatCh {confid}"

abbreviation 
  Auth :: "[agent, agent, payload] ⇒ chmsg" where
  "Auth ≡ StatCh {auth}"

abbreviation 
  Secure :: "[agent, agent, payload] ⇒ chmsg" where
  "Secure ≡ StatCh {auth, confid}"

abbreviation 
  dConfid :: "[key, payload] ⇒ chmsg" where
  "dConfid ≡ DynCh {confid}"

abbreviation 
  dAuth :: "[key, payload] ⇒ chmsg" where
  "dAuth ≡ DynCh {auth}"

abbreviation 
  dSecure :: "[key, payload] ⇒ chmsg" where
  "dSecure ≡ DynCh {auth, confid}"


(******************************************************************************)
subsection ‹Keys used in dynamic channel messages›
(******************************************************************************)

definition 
  keys_for :: "chmsg set ⇒ key set" where
  "keys_for H ≡ {K. ∃c M. DynCh c K M ∈ H}"

lemma keys_forI [dest]: "DynCh c K M ∈ H ⟹ K ∈ keys_for H"
by (auto simp add: keys_for_def)


lemma keys_for_empty [simp]: "keys_for {} = {}"
by (simp add: keys_for_def)

lemma keys_for_monotone: "G ⊆ H ⟹ keys_for G ⊆ keys_for H"
by (auto simp add: keys_for_def)

lemmas keys_for_mono [elim] = keys_for_monotone [THEN [2] rev_subsetD]


lemma keys_for_insert_StatCh [simp]: 
  "keys_for (insert (StatCh c A B M) H) = keys_for H"
by (auto simp add: keys_for_def)

lemma keys_for_insert_DynCh [simp]: 
  "keys_for (insert (DynCh c K M) H) = insert K (keys_for H)"
by (auto simp add: keys_for_def)


(******************************************************************************)
subsection ‹Atoms in a set of channel messages›
(******************************************************************************)

text ‹The set of atoms contained in a set of channel messages. We also 
include the public atoms, i.e., the agent names, numbers, and corrupted keys. 
›

inductive_set 
  atoms :: "chmsg set ⇒ atom set"
  for H :: "chmsg set"
where
  at_StatCh: "⟦ StatCh c A B (Msg M) ∈ H; At ∈ set M ⟧ ⟹ At ∈ atoms H"
| at_DynCh: "⟦ DynCh c K (Msg M) ∈ H; At ∈ set M ⟧ ⟹ At ∈ atoms H"

declare atoms.intros [intro]

lemma atoms_empty [simp]: "atoms {} = {}"
by (auto elim!: atoms.cases)

lemma atoms_monotone: "G ⊆ H ⟹ atoms G ⊆ atoms H"
by (auto elim!: atoms.cases)

lemmas atoms_mono [elim] = atoms_monotone [THEN [2] rev_subsetD]


lemma atoms_insert_StatCh [simp]: 
  "atoms (insert (StatCh c A B (Msg M)) H) = set M ∪ atoms H"
by (auto elim!: atoms.cases)

lemma atoms_insert_DynCh [simp]: 
  "atoms (insert (DynCh c K (Msg M)) H) = set M ∪ atoms H"
by (auto elim!: atoms.cases)


(******************************************************************************)
subsection ‹Intruder knowledge (atoms)›
(******************************************************************************)

text ‹Atoms that the intruder can extract from a set of channel messages.›

inductive_set 
  extr :: "atom set ⇒ chmsg set ⇒ atom set"
  for T :: "atom set" 
  and H :: "chmsg set"
where 
  extr_Inj: "At ∈ T ⟹ At ∈ extr T H"
| extr_StatCh: 
    "⟦ StatCh c A B (Msg M) ∈ H; At ∈ set M; confid ∉ c ∨ A ∈ bad ∨ B ∈ bad ⟧ 
   ⟹ At ∈ extr T H"
| extr_DynCh: 
    "⟦ DynCh c K (Msg M) ∈ H; At ∈ set M; confid ∉ c ∨ aKey K ∈ extr T H ⟧ 
   ⟹ At ∈ extr T H"

declare extr.intros [intro]
declare extr.cases [elim]


text‹Typical parameter describing initial intruder knowledge.›

definition
  ik0 :: "atom set" where 
  "ik0 ≡ range aAgt ∪ range aNum ∪ aKey`corrKey"

lemma ik0_aAgt [iff]: "aAgt A ∈ ik0"
by (auto simp add: ik0_def)

lemma ik0_aNum [iff]: "aNum T ∈ ik0"
by (auto simp add: ik0_def)

lemma ik0_aNon [iff]: "aNon N ∉ ik0"
by (auto simp add: ik0_def)

lemma ik0_aKey_corr [simp]: "(aKey K ∈ ik0) = (K ∈ corrKey)"
by (auto simp add: ik0_def)


subsubsection ‹Basic lemmas›
(******************************************************************************)

lemma extr_empty [simp]: "extr T {} = T"
by (auto)

lemma extr_monotone [dest]: "G ⊆ H ⟹ extr T G ⊆ extr T H"
by (safe, erule extr.induct, auto)

lemmas extr_mono [elim] = extr_monotone [THEN [2] rev_subsetD]

lemma extr_monotone_param [dest]: "T ⊆ U ⟹ extr T H ⊆ extr U H"
by (safe, erule extr.induct, auto)

lemmas extr_mono_param [elim] = extr_monotone_param [THEN [2] rev_subsetD]

lemma extr_insert [intro]: "At ∈ extr T H ⟹ At ∈ extr T (insert C H)"
by (erule extr_mono) (auto)

lemma extr_into_atoms [dest]: "At ∈ extr T H ⟹ At ∈ T ∪ atoms H"
by (erule extr.induct, auto)


subsubsection ‹Insertion lemmas for atom parameters›
(******************************************************************************)

lemma extr_insert_non_key_param [simp]:
  assumes "At ∈ range aNon ∪ range aAgt ∪ range aNum"
  shows "extr (insert At T) H = insert At (extr T H)"
proof -
  { fix Bt
    assume "Bt ∈ extr (insert At T) H"
    hence "Bt ∈ insert At (extr T H)" 
      using assms by induct auto
  }
  thus ?thesis by auto
qed

lemma extr_insert_unused_key_param [simp]:
  assumes "K ∉ keys_for H"
  shows "extr (insert (aKey K) T) H = insert (aKey K) (extr T H)"
proof -
  { fix At
    assume "At ∈ extr (insert (aKey K) T) H"
    hence "At ∈ insert (aKey K) (extr T H)" 
      using assms by induct (auto simp add: keys_for_def)
  }
  thus ?thesis by auto
qed



subsubsection ‹Insertion lemmas for each type of channel message›
(******************************************************************************)

text ‹Note that the parameter accumulates the extracted atoms. In particular, 
these may include keys that may open further dynamically confidential messages. 
›

lemma extr_insert_StatCh [simp]: 
  "extr T (insert (StatCh c A B (Msg M)) H) 
   = (if confid ∉ c ∨ A ∈ bad ∨ B ∈ bad then extr (set M ∪ T) H else extr T H)"
proof (cases "confid ∉ c ∨ A ∈ bad ∨ B ∈ bad")
  case True
  moreover 
  {
    fix At
    assume "At ∈ extr T (insert (StatCh c A B (Msg M)) H)"
    hence "At ∈ extr (set M ∪ T) H" by induct auto
  }
  moreover
  {
    fix At
    assume "At ∈ extr (set M ∪ T) H" 
    and    "confid ∉ c ∨ A ∈ bad ∨ B ∈ bad"
    hence "At ∈ extr T (insert (StatCh c A B (Msg M)) H)" by induct auto
  }
  ultimately show ?thesis by auto
next 
  case False
  moreover
  {
    fix At
    assume "At ∈ extr T (insert (StatCh c A B (Msg M)) H)"
    and "confid ∈ c" "A ∉ bad" "B ∉ bad"
    hence "At ∈ extr T H" by induct auto
  }
  ultimately show ?thesis by auto
qed

lemma extr_insert_DynCh [simp]: 
  "extr T (insert (DynCh c K (Msg M)) H) 
   = (if confid ∉ c ∨ aKey K ∈ extr T H then extr (set M ∪ T) H else extr T H)"
proof (cases "confid ∉ c ∨ aKey K ∈ extr T H")
  case True
  moreover
  {
    fix At
    assume "At ∈ extr T (insert (DynCh c K (Msg M)) H)"
    hence "At ∈ extr (set M ∪ T) H" by induct auto
  }
  moreover
  {
    fix At
    assume "At ∈ extr (set M ∪ T) H"
    hence "At ∈ extr T (insert (DynCh c K (Msg M)) H)" 
      using True by induct auto
  }
  ultimately show ?thesis by auto
next
  case False
  moreover
  hence "extr T (insert (DynCh c K (Msg M)) H) = extr T H" 
    by (intro equalityI subsetI) (erule extr.induct, auto)+
  ultimately show ?thesis by auto
qed


declare extr.cases [rule del, elim]


(******************************************************************************)
subsection ‹Faking messages›
(******************************************************************************)

text ‹Channel messages that are fakeable from a given set of channel
messages.  Parameters are a set of atoms and a set of freshness identifiers.

For faking messages on dynamic non-authentic channels, we cannot allow the
intruder to use arbitrary keys. Otherwise, we would lose the possibility to 
generate fresh values in our model. Therefore, the chosen keys must correspond
to session keys associated with existing runs (i.e., from set 
@{term "rkeys U"}).
›

abbreviation 
  rkeys :: "fid_t set ⇒ key set" where
  "rkeys U ≡ sesK`(λ(x, y). x $ y)`(U × (UNIV::nat set))"

lemma rkeys_sesK [simp, dest]: "sesK (R$i) ∈ rkeys U ⟹ R ∈ U"
by (auto simp add: image_def)


inductive_set 
  fake :: "atom set ⇒ fid_t set ⇒ chmsg set ⇒ chmsg set"
  for T :: "atom set"
  and U :: "fid_t set"
  and H :: "chmsg set"
where 
  fake_Inj:
    "M ∈ H ⟹ M ∈ fake T U H"
| fake_StatCh: 
    "⟦ set M ⊆ extr T H; auth ∉ c ∨ A ∈ bad ∨ B ∈ bad  ⟧ 
   ⟹ StatCh c A B (Msg M) ∈ fake T U H"
| fake_DynCh:  
    "⟦ set M ⊆ extr T H; auth ∉ c ∧ K ∈ rkeys U ∨ aKey K ∈ extr T H ⟧ 
   ⟹ DynCh c K (Msg M) ∈ fake T U H"

declare fake.cases [elim]
declare fake.intros [intro]

lemmas fake_intros = fake_StatCh fake_DynCh

lemma fake_expanding [intro]: "H ⊆ fake T U H"
by (auto)

lemma fake_monotone [intro]: "G ⊆ H ⟹ fake T U G ⊆ fake T U H"
by (safe, erule fake.cases, auto intro!: fake_intros)

lemma fake_monotone_param1 [intro]: 
  "T ⊆ T' ⟹ fake T U H ⊆ fake T' U H" 
by (safe, erule fake.cases, auto intro!: fake_intros)

lemmas fake_mono [elim] = fake_monotone [THEN [2] rev_subsetD]
lemmas fake_mono_param1 [elim] = fake_monotone_param1 [THEN [2] rev_subsetD]


subsubsection ‹Atoms and extr together with fake›
(******************************************************************************)

lemma atoms_fake [simp]: "atoms (fake T U H) = T ∪ atoms H"
proof -
  {
    fix At 
    assume "At ∈ T"
    hence "At ∈ atoms (fake T U H)"
    proof -
      {
        fix A B 
        have "Insec A B (Msg [At]) ∈ fake T U H" using ‹At ∈ T›
        by (intro fake_StatCh) (auto)
      }
      thus ?thesis by (intro at_StatCh) (auto)
    qed
  }
  moreover
  {
    fix At
    assume "At ∈ atoms (fake T U H) "
    hence "At ∈ T ∪ atoms H" by cases blast+
  }
  ultimately show ?thesis by auto
qed


lemma extr_fake [simp]: 
  assumes "T' ⊆ T" shows "extr T (fake T' U H) = extr T H"
proof (intro equalityI subsetI) 
  fix At
  assume "At ∈ extr T (fake T' U H)"
  with assms have "At ∈ extr T (fake T U H)" by auto
  thus "At ∈ extr T H" by induct auto
qed auto

(*
lemma extr_fake [simp]: "extr T (fake T U H) = extr T H"
proof -
  {
    fix At
    assume "At ∈ extr T (fake T U H)"
    hence "At ∈ extr T H" by induct auto
  }
  thus ?thesis by auto
qed
*)

end