Theory Channels

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

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  Channels.thy (Isabelle/HOL 2016-1)
  ID:      $Id: Channels.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>
  
  Channel messages and related message derivations (extract and fake).

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

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

section ‹Channel Messages›

theory Channels
imports Message_derivation
begin

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

datatype chan = 
  Chan "tag" "agent" "agent" "msg"


abbreviation 
  Insec :: "[agent, agent, msg] ⇒ chan" where
  "Insec ≡ Chan insec"

abbreviation 
  Confid :: "[agent, agent, msg] ⇒ chan" where
  "Confid ≡ Chan confid"

abbreviation 
  Auth :: "[agent, agent, msg] ⇒ chan" where
  "Auth ≡ Chan auth"

abbreviation 
  Secure :: "[agent, agent, msg] ⇒ chan" where
  "Secure ≡ Chan secure"


(**************************************************************************************************)
subsection ‹Extract›
(**************************************************************************************************)

text ‹The set of payload messages that can be extracted from a set of (crypto) messages 
and a set of channel messages, given a set of bad agents. The second rule states that 
the payload can be extracted from insecure and authentic channels as well as from channels
with a compromised endpoint.›

inductive_set 
  extr :: "agent set ⇒ msg set ⇒ chan set ⇒ msg set"  
  for bad :: "agent set"
  and IK :: "msg set"
  and H :: "chan set"
where 
  extr_Inj: "M ∈ IK ⟹ M ∈ extr bad IK H"
| extr_Chan: 
    "⟦ Chan c A B M ∈ H; c = insec ∨ c = auth ∨ A ∈ bad ∨ B ∈ bad ⟧ ⟹ M ∈ extr bad IK H"

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


lemma extr_empty_chan [simp]: "extr bad IK {} = IK"
by (auto)

lemma IK_subset_extr: "IK ⊆ extr bad IK chan"
by (auto)

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

lemma extr_mono_IK [dest]: "IK1 ⊆ IK2 ⟹ extr bad IK1 H ⊆ extr bad IK2 H"
by (safe) (erule extr.induct, auto)

lemma extr_mono_bad [dest]: "bad ⊆ bad' ⟹ extr bad IK H ⊆ extr bad' IK H"
by (safe, erule extr.induct, auto)

lemmas extr_monotone_chan [elim] = extr_mono_chan [THEN [2] rev_subsetD]
lemmas extr_monotone_IK [elim] = extr_mono_IK [THEN [2] rev_subsetD]
lemmas extr_monotone_bad [elim] = extr_mono_bad [THEN [2] rev_subsetD]

lemma extr_mono [intro]: "⟦ b ⊆ b'; I ⊆ I'; C ⊆ C' ⟧ ⟹ extr b I C ⊆ extr b' I' C'"
by (force)

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

lemma extr_insert [intro]: "M ∈ extr bad IK H ⟹ M ∈ extr bad IK (insert C H)"
by (auto)

lemma extr_insert_Chan [simp]: 
  "extr bad IK (insert (Chan c A B M) H) 
   = (if c = insec ∨ c = auth ∨ A ∈ bad ∨ B ∈ bad 
      then insert M (extr bad IK H) else extr bad IK H)"
by auto

(* do not declare [simp]! *)
lemma extr_insert_chan_eq: "extr bad IK (insert X CH) = extr bad IK {X} ∪ extr bad IK CH"
by (auto)

lemma extr_insert_IK_eq [simp]: "extr bad (insert X IK) CH = insert X (extr bad IK CH)"
by (auto)

lemma extr_insert_bad:
  "extr (insert A bad) IK CH ⊆
   extr bad IK CH ∪ {M. ∃ B. Confid A B M ∈ CH ∨ Confid B A M ∈ CH ∨
                             Secure A B M ∈ CH ∨ Secure B A M ∈ CH}"
by (rule, erule extr.induct, auto intro: tag.exhaust)

lemma extr_insert_Confid [simp]:
  "A ∉ bad ⟹
   B ∉ bad ⟹ 
   extr bad IK (insert (Confid A B X) CH) = extr bad IK CH"
by auto


(**************************************************************************************************)
subsection ‹Fake›
(**************************************************************************************************)

text ‹The set of channel messages that an attacker can fake given a set of compromised
agents, a set of crypto messages and a set of channel messages. The second rule states
that an attacker can fake an insecure or confidential messages or a channel message
with a compromised endpoint using a payload that he knows.›

inductive_set 
  fake :: "agent set ⇒ msg set ⇒ chan set ⇒ chan set"
  for bad :: "agent set"
  and IK :: "msg set"
  and chan :: "chan set"
where 
  fake_Inj: "M ∈ chan ⟹ M ∈ fake bad IK chan"
| fake_New: 
    "⟦ M ∈ IK; c = insec ∨ c = confid ∨ A ∈ bad ∨ B ∈ bad  ⟧ 
   ⟹ Chan c A B M ∈ fake bad IK chan"

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

lemmas fake_intros = fake_Inj fake_New

lemma fake_mono_bad [intro]: 
  "bad ⊆ bad' ⟹ fake bad IK chan ⊆ fake bad' IK chan" 
by (auto)

lemma fake_mono_ik [intro]: 
  "IK ⊆ IK' ⟹ fake bad IK chan ⊆ fake bad IK' chan" 
by (auto)

lemma fake_mono_chan [intro]: 
  "chan ⊆ chan' ⟹ fake bad IK chan ⊆ fake bad IK chan'" 
by (auto)

lemma fake_mono [intro]: 
  "⟦ bad ⊆ bad'; IK ⊆ IK'; chan ⊆ chan'⟧ ⟹ fake bad IK chan ⊆ fake bad' IK' chan'" 
by (auto, erule fake.cases, auto)

lemmas fake_monotone_bad [elim] = fake_mono_bad [THEN [2] rev_subsetD]
lemmas fake_monotone_ik [elim] = fake_mono_ik [THEN [2] rev_subsetD]
lemmas fake_monotone_chan [elim] = fake_mono_chan [THEN [2] rev_subsetD]
lemmas fake_monotone [elim] = fake_mono [THEN [2] rev_subsetD]


lemma chan_subset_fake: "chan ⊆ fake bad IK chan"
by auto

lemma extr_fake:
  "X ∈ fake bad IK chan ⟹ extr bad IK' {X} ⊆ IK ∪ extr bad IK' chan"
by auto

lemmas extr_fake_2 [elim] = extr_fake [THEN [2] rev_subsetD]

lemma fake_parts_extr_singleton:  
  "X ∈ fake bad IK chan ⟹ parts (extr bad IK' {X}) ⊆ parts IK ∪ parts (extr bad IK' chan)"
by (rule extr_fake [THEN parts_mono, simplified])

lemmas fake_parts_extr_singleton_2 [elim] = fake_parts_extr_singleton [THEN [2] rev_subsetD]


lemma fake_parts_extr_insert: 
assumes "X ∈ fake bad IK CH"
shows "parts (extr bad IK' (insert X CH)) ⊆ parts (extr bad IK' CH) ∪ parts IK"
proof -
  have "parts (extr bad IK' (insert X CH)) ⊆ parts (extr bad IK' {X}) ∪ parts (extr bad IK' CH)" 
    by (auto simp: extr_insert_chan_eq [where CH=CH])
  also have "... ⊆ parts (extr bad IK' CH) ∪ parts IK" using assms
    by (auto dest!: fake_parts_extr_singleton)
  finally show ?thesis .
qed


lemma fake_synth_analz_extr: 
assumes  "X ∈ fake bad (synth (analz (extr bad IK CH))) CH"
shows "synth (analz (extr bad IK (insert X CH))) = synth (analz (extr bad IK CH))"
using assms
proof (intro equalityI) 
  have "synth (analz (extr bad IK (insert X CH))) 
     ⊆ synth (analz (extr bad IK {X} ∪ extr bad IK CH))"
    by - (rule synth_analz_mono, auto)
  also have "... ⊆ synth (analz (synth (analz (extr bad IK CH)) ∪ extr bad IK CH))" using assms
    by - (rule synth_analz_mono, auto)
  also have "... ⊆ synth (analz (synth (analz (extr bad IK CH))))"
    by - (rule synth_analz_mono, auto)
  also have "... ⊆ synth (analz (extr bad IK CH))" by simp
  finally show "synth (analz (extr bad IK (insert X CH))) ⊆ synth (analz (extr bad IK CH))" .
next
  have "extr bad IK CH ⊆ extr bad IK (insert X CH)"
    by auto
  then show "synth (analz (extr bad IK CH)) ⊆ synth (analz (extr bad IK (insert X CH)))"
    by - (rule synth_analz_mono, auto)
qed


(**************************************************************************************************)
subsection ‹Closure of Dolev-Yao, extract and fake›
(**************************************************************************************************)

subsubsection ‹‹dy_fake_msg›: returns messages, closure of DY and extr is sufficient›
(**************************************************************************************************)

text ‹Close @{term extr} under Dolev-Yao closure using @{term synth} and @{term analz}. 
This will be used in Level 2 attacker events to fake crypto messages.›

definition 
  dy_fake_msg :: "agent set ⇒ msg set ⇒ chan set ⇒ msg set"
where
  "dy_fake_msg b i c = synth (analz (extr b i c))"


lemma dy_fake_msg_empty [simp]: "dy_fake_msg bad {} {} = synth {}"
by (auto simp add: dy_fake_msg_def)

lemma dy_fake_msg_mono_bad [dest]: "bad ⊆ bad' ⟹ dy_fake_msg bad I C ⊆ dy_fake_msg bad' I C"
by (auto simp add: dy_fake_msg_def intro!: synth_analz_mono)

lemma dy_fake_msg_mono_ik [dest]: "G ⊆ H ⟹ dy_fake_msg bad G C ⊆ dy_fake_msg bad H C"
by (auto simp add: dy_fake_msg_def intro!: synth_analz_mono)

lemma dy_fake_msg_mono_chan [dest]: "G ⊆ H ⟹ dy_fake_msg bad I G ⊆ dy_fake_msg bad I H"
by (auto simp add: dy_fake_msg_def intro!: synth_analz_mono)
 
lemmas dy_fake_msg_monotone_bad [elim] = dy_fake_msg_mono_bad [THEN [2] rev_subsetD]
lemmas dy_fake_msg_monotone_ik [elim] = dy_fake_msg_mono_ik [THEN [2] rev_subsetD]
lemmas dy_fake_msg_monotone_chan [elim] = dy_fake_msg_mono_chan [THEN [2] rev_subsetD]

lemma dy_fake_msg_insert [intro]: 
  "M ∈ dy_fake_msg bad I C ⟹ M ∈ dy_fake_msg bad I (insert X C)"
by (auto)

lemma dy_fake_msg_mono [intro]: 
  "⟦ b ⊆ b'; I ⊆ I'; C ⊆ C' ⟧ ⟹ dy_fake_msg b I C ⊆ dy_fake_msg b' I' C'"
by (force simp add: dy_fake_msg_def intro!: synth_analz_mono)

lemmas dy_fake_msg_monotone [elim] = dy_fake_msg_mono [THEN [2] rev_subsetD]

lemma dy_fake_msg_insert_chan:
  "x = insec ∨ x = auth ⟹
   M ∈ dy_fake_msg bad IK (insert (Chan x A B M) CH)"
by (auto simp add: dy_fake_msg_def)


subsubsection ‹‹dy_fake_chan›: returns channel messages›
(**************************************************************************************************)

text ‹The set of all channel messages that an attacker can fake is obtained using
@{term fake} with the sets of possible payload messages derived with @{term dy_fake_msg}
defined above. This will be used in Level 2 attacker events to fake channel messages.›

definition
  dy_fake_chan :: "agent set ⇒ msg set ⇒ chan set ⇒ chan set"
where
  "dy_fake_chan b i c = fake b (dy_fake_msg b i c) c"


lemma dy_fake_chan_mono_bad [intro]: 
  "bad ⊆ bad' ⟹ dy_fake_chan bad I C ⊆ dy_fake_chan bad' I C" 
by (auto simp add: dy_fake_chan_def)

lemma dy_fake_chan_mono_ik [intro]: 
  "T ⊆ T' ⟹ dy_fake_chan bad T C ⊆ dy_fake_chan bad T' C" 
by (auto simp add: dy_fake_chan_def)

lemma dy_fake_chan_mono_chan [intro]: 
  "C ⊆ C' ⟹ dy_fake_chan bad T C ⊆ dy_fake_chan bad T C'" 
by (auto simp add: dy_fake_chan_def)

lemmas dy_fake_chan_monotone_bad [elim] = dy_fake_chan_mono_bad [THEN [2] rev_subsetD]
lemmas dy_fake_chan_monotone_ik [elim] = dy_fake_chan_mono_ik [THEN [2] rev_subsetD]
lemmas dy_fake_chan_monotone_chan [elim] = dy_fake_chan_mono_chan [THEN [2] rev_subsetD]


lemma dy_fake_chan_mono [intro]: 
  assumes "b ⊆ b'" and "I ⊆ I'" and "C ⊆ C'"
  shows "dy_fake_chan b I C ⊆ dy_fake_chan b' I' C'"
proof -
  have "dy_fake_chan b I C ⊆ dy_fake_chan b' I C" using ‹b ⊆ b'› by auto
  also have "... ⊆ dy_fake_chan b' I' C" using ‹I ⊆ I'› by auto
  also have "... ⊆ dy_fake_chan b' I' C'" using ‹C ⊆ C'› by auto
  finally show ?thesis .
qed

lemmas dy_fake_chan_monotone [elim] = dy_fake_chan_mono [THEN [2] rev_subsetD]

lemma dy_fake_msg_subset_synth_analz: 
  "⟦extr bad IK chan ⊆ T ⟧ ⟹ dy_fake_msg bad IK chan ⊆ synth (analz T)"
by (auto simp add: dy_fake_msg_def synth_analz_mono)

lemma dy_fake_chan_mono2:
  "⟦ extr bad IK chan ⊆ synth (analz y); chan ⊆ fake bad (synth (analz y)) z ⟧
 ⟹ dy_fake_chan bad IK chan ⊆ fake bad (synth (analz y)) z"
apply (auto simp add: dy_fake_chan_def, erule fake.cases, auto)
apply (auto intro!: fake_New dest!: dy_fake_msg_subset_synth_analz)
done

lemma extr_subset_dy_fake_msg: "extr bad IK chan ⊆ dy_fake_msg bad IK chan"
by (auto simp add: dy_fake_msg_def)


lemma dy_fake_chan_extr_insert: 
  "M ∈ dy_fake_chan bad IK CH ⟹ extr bad IK (insert M CH) ⊆ dy_fake_msg bad IK CH"
by (auto simp add: dy_fake_chan_def dy_fake_msg_def dest: fake_synth_analz_extr)

lemma dy_fake_chan_extr_insert_parts:
  "M ∈ dy_fake_chan bad IK CH ⟹
   parts (extr bad IK (insert M CH)) ⊆ parts (extr bad IK CH) ∪ dy_fake_msg bad IK CH"
by (drule dy_fake_chan_extr_insert [THEN parts_mono], auto simp add: dy_fake_msg_def)

lemma dy_fake_msg_extr: 
  "extr bad ik chan ⊆ synth (analz X) ⟹ dy_fake_msg bad ik chan ⊆ synth (analz X)"
by (drule synth_analz_mono) (auto simp add: dy_fake_msg_def)

lemma extr_insert_dy_fake_msg:
  "M ∈ dy_fake_msg bad IK CH ⟹ extr bad (insert M IK) CH ⊆ dy_fake_msg bad IK CH"
by (auto simp add: dy_fake_msg_def)

lemma dy_fake_msg_insert_dy_fake_msg:
  "M ∈ dy_fake_msg bad IK CH ⟹ dy_fake_msg bad (insert M IK) CH ⊆ dy_fake_msg bad IK CH"
by (drule synth_analz_mono [OF extr_insert_dy_fake_msg], auto simp add: dy_fake_msg_def)

lemma synth_analz_insert_dy_fake_msg:
  "M ∈ dy_fake_msg bad IK CH ⟹ synth (analz (insert M IK)) ⊆ dy_fake_msg bad IK CH"
by (auto dest!: dy_fake_msg_insert_dy_fake_msg, erule subsetD, 
    auto simp add: dy_fake_msg_def elim: synth_analz_monotone)

lemma Fake_insert_dy_fake_msg:
  "M ∈ dy_fake_msg bad IK CH ⟹
   extr bad IK CH ⊆ synth (analz X) ⟹
   synth (analz (insert M IK)) ⊆ synth (analz X)"
by (auto dest!: synth_analz_insert_dy_fake_msg dy_fake_msg_extr)

lemma dy_fake_chan_insert_chan:
  "x = insec ∨ x = auth ⟹
   Chan x A B M ∈ dy_fake_chan bad IK (insert (Chan x A B M) CH)"
by (auto simp add: dy_fake_chan_def)

lemma dy_fake_chan_subset:
  "CH ⊆ fake bad (dy_fake_msg bad IK CH) CH' ⟹
   dy_fake_chan bad IK CH ⊆ fake bad (dy_fake_msg bad IK CH) CH'"
by (auto simp add: dy_fake_chan_def)


end