Theory dhlvl3

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

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  dhlvl3.thy (Isabelle/HOL 2016-1)
  ID:      $Id: dhlvl3.thy 133183 2017-01-31 13:55:43Z csprenge $
  Author:  Joseph Lallemand, INRIA Nancy <joseph.lallemand@loria.fr>
           Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Level-3 Diffie-Hellman protocol using generic channel implementation.
  Refines dhlvl2 based on channel assumptions.

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

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

section ‹Authenticated Diffie-Hellman Protocol (L3 locale)›

theory dhlvl3
imports dhlvl2 Implem_lemmas
begin

(**************************************************************************************************)
subsection ‹State and Events›
(**************************************************************************************************)

text ‹Level 3 state.›

text ‹(The types have to be defined outside the locale.)›

record l3_state = l1_state +  
  bad :: "agent set"

type_synonym l3_obs = "l3_state"

type_synonym
  l3_pred = "l3_state set"

type_synonym
  l3_trans = "(l3_state × l3_state) set"


text ‹Attacker event.›

definition
  l3_dy :: "msg ⇒ l3_trans"
where
  "l3_dy ≡ ik_dy"



text ‹Compromise events.›

definition
  l3_lkr_others :: "agent ⇒ l3_trans"
where
  "l3_lkr_others A ≡ {(s,s').
    ― ‹guards›
    A ≠ test_owner ∧
    A ≠ test_partner ∧
    ― ‹actions›
    s' = s⦇bad := {A} ∪ bad s,
           ik := keys_of A ∪ ik s⦈
  }"

definition
  l3_lkr_actor :: "agent ⇒ l3_trans"
where
  "l3_lkr_actor A ≡ {(s,s').
    ― ‹guards›
    A = test_owner ∧
    A ≠ test_partner ∧
    ― ‹actions›
    s' = s⦇bad := {A} ∪ bad s,
           ik := keys_of A ∪ ik s⦈
  }"

definition
  l3_lkr_after :: "agent ⇒ l3_trans"
where
  "l3_lkr_after A ≡ {(s,s').
    ― ‹guards›
    test_ended s ∧
    ― ‹actions›
    s' = s⦇bad := {A} ∪ bad s,
           ik := keys_of A ∪ ik s⦈
  }"

definition
  l3_skr :: "rid_t ⇒ msg ⇒ l3_trans"
where
  "l3_skr R K ≡ {(s,s').
    ― ‹guards›
    R ≠ test ∧ R ∉ partners ∧
    in_progress (progress s R) xsk ∧
    guessed_frame R xsk = Some K ∧
    ― ‹actions›
    s' = s⦇ik := {K} ∪ ik s⦈
  }"


text ‹New locale for the level 3 protocol. This locale does not add new assumptions, 
it is only used to separate the level 3 protocol from the implementation locale.›

locale dhlvl3 = valid_implem
begin

text ‹Protocol events: 
\begin{itemize}
  \item step 1: create @{term "Ra"}, @{term "A"} generates @{term "nx"},
    computes and insecurely sends $@{term "g"}^@{term "nx"}$
  \item step 2: create @{term "Rb"}, @{term "B"} receives $@{term "g"}^@{term "nx"}$ insecurely,
    generates @{term "ny"}, computes $@{term "g"}^@{term "ny"}$,
    authentically sends $(@{term "g"}^@{term "ny"}, @{term "g"}^@{term "nx"})$,
    computes $@{term "g"}^@{term "nx*ny"}$,
    emits a running signal for @{term "Init"}, $@{term "g"}^@{term "nx*ny"}$
  \item step 3: @{term "A"} receives $@{term "g"}^@{term "ny"}$ and $@{term "g"}^@{term "nx"}$
    authentically,
    sends $(@{term "g"}^@{term "nx"}, @{term "g"}^@{term "ny"})$ authentically,
    computes $@{term "g"}^@{term "ny*nx"}$, emits a commit signal for @{term "Init"},
    $@{term "g"}^@{term "ny*nx"}$, a running signal for @{term "Resp"}, $@{term "g"}^@{term "ny*nx"}$,
    declares the secret $@{term "g"}^@{term "ny*nx"}$
  \item step 4: @{term "B"} receives $@{term "g"}^@{term "nx"}$ and $@{term "g"}^@{term "ny"}$
    authentically,
    emits a commit signal for @{term "Resp"}, $@{term "g"}^@{term "nx*ny"}$,
    declares the secret $@{term "g"}^@{term "nx*ny"}$
\end{itemize}
›
definition
    l3_step1 :: "rid_t ⇒ agent ⇒ agent ⇒ l3_trans"
where
  "l3_step1 Ra A B ≡ {(s, s').
    ― ‹guards:›
    Ra ∉ dom (progress s) ∧
    guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
    ― ‹actions:›
    s' = s⦇
      progress := (progress s)(Ra ↦ {xnx, xgnx}),
      ik := {implInsec A B (Exp Gen (NonceF (Ra$nx)))} ∪ ik s
      ⦈
  }"

definition
  l3_step2 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ l3_trans"
where
  "l3_step2 Rb A B gnx ≡ {(s, s').
    ― ‹guards:›
    guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
    Rb ∉ dom (progress s) ∧
    guessed_frame Rb xgnx = Some gnx ∧
    guessed_frame Rb xsk = Some (Exp gnx (NonceF (Rb$ny))) ∧
    implInsec A B gnx ∈ ik s ∧
    ― ‹actions:›
    s' = s⦇ progress := (progress s)(Rb ↦ {xny, xgny, xgnx, xsk}),
            ik := {implAuth B A ⟨Number 0, Exp Gen (NonceF (Rb$ny)), gnx⟩} ∪ ik s,
            signalsInit := if can_signal s A B then
                          addSignal (signalsInit s) (Running A B (Exp gnx (NonceF (Rb$ny))))
                       else
                          signalsInit s
         ⦈
  }"  


definition
  l3_step3 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ l3_trans"
where
  "l3_step3 Ra A B gny ≡ {(s, s').
    ― ‹guards:›
    guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
    progress s Ra = Some {xnx, xgnx} ∧
    guessed_frame Ra xgny = Some gny ∧
    guessed_frame Ra xsk = Some (Exp gny (NonceF (Ra$nx))) ∧
    implAuth B A ⟨Number 0, gny, Exp Gen (NonceF (Ra$nx))⟩ ∈ ik s ∧
    ― ‹actions:›
    s' = s⦇ progress := (progress s)(Ra ↦ {xnx, xgnx, xgny, xsk, xEnd}),
            ik := {implAuth A B ⟨Number 1, Exp Gen (NonceF (Ra$nx)), gny⟩} ∪ ik s,
            secret := {x. x = Exp gny (NonceF (Ra$nx)) ∧ Ra = test} ∪ secret s,
            signalsInit := if can_signal s A B then
                         addSignal (signalsInit s) (Commit A B (Exp gny (NonceF (Ra$nx))))
                       else
                         signalsInit s,
            signalsResp := if can_signal s A B then
                         addSignal (signalsResp s) (Running A B (Exp gny (NonceF (Ra$nx))))
                       else
                         signalsResp s
          ⦈
  }"


definition
  l3_step4 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ l3_trans"
where
  "l3_step4 Rb A B gnx ≡ {(s, s').
    ― ‹guards:›
    guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
    progress s Rb = Some {xny, xgnx, xgny, xsk} ∧
    guessed_frame Rb xgnx = Some gnx ∧
    implAuth A B ⟨Number 1, gnx, Exp Gen (NonceF (Rb$ny))⟩ ∈ ik s ∧

    ― ‹actions:›
    s' = s⦇ progress := (progress s)(Rb ↦ {xny, xgnx, xgny, xsk, xEnd}),
            secret := {x. x = Exp gnx (NonceF (Rb$ny)) ∧ Rb = test} ∪ secret s,
            signalsResp := if can_signal s A B then
                             addSignal (signalsResp s) (Commit A B (Exp gnx (NonceF (Rb$ny))))
                           else
                             signalsResp s
          ⦈
  }"


text ‹Specification.›

text ‹Initial compromise.›
definition
  ik_init :: "msg set"
where
  "ik_init ≡ {priK C |C. C ∈ bad_init} ∪ {pubK A | A. True} ∪ 
             {shrK A B |A B. A ∈ bad_init ∨ B ∈ bad_init} ∪ Tags"

text ‹Lemmas about @{term "ik_init"}.›
lemma parts_ik_init [simp]: "parts ik_init = ik_init"
by (auto elim!: parts.induct, auto simp add: ik_init_def)

lemma analz_ik_init [simp]: "analz ik_init = ik_init"
by (auto dest: analz_into_parts)

lemma abs_ik_init [iff]: "abs ik_init = {}"
apply (auto elim!: absE)
apply (auto simp add: ik_init_def)
done

lemma payloadSet_ik_init [iff]: "ik_init ∩ payload = {}"
by (auto simp add: ik_init_def)

lemma validSet_ik_init [iff]: "ik_init ∩ valid= {}"
by (auto simp add: ik_init_def)


definition 
  l3_init :: "l3_state set"
where
  "l3_init ≡ { ⦇
    ik = ik_init,
    secret = {},
    progress = Map.empty,
    signalsInit = λx. 0,
    signalsResp = λx. 0,
    bad = bad_init
    ⦈}"

lemmas l3_init_defs = l3_init_def ik_init_def

definition 
l3_trans :: "l3_trans"
where
  "l3_trans ≡ (⋃ M X Rb Ra A B K.
     l3_step1 Ra A B ∪
     l3_step2 Rb A B X ∪
     l3_step3 Ra A B X ∪
     l3_step4 Rb A B X ∪
     l3_dy M ∪
     l3_lkr_others A ∪
     l3_lkr_after A ∪
     l3_skr Ra K ∪
     Id
  )"


definition 
  l3 :: "(l3_state, l3_obs) spec" where
  "l3 ≡ ⦇
    init = l3_init,
    trans = l3_trans,
    obs = id
  ⦈"

lemmas l3_loc_defs = 
  l3_step1_def l3_step2_def l3_step3_def l3_step4_def
  l3_def l3_init_defs l3_trans_def
  l3_dy_def
  l3_lkr_others_def l3_lkr_after_def l3_skr_def

lemmas l3_defs = l3_loc_defs ik_dy_def
lemmas l3_nostep_defs = l3_def l3_init_def l3_trans_def


lemma l3_obs_id [simp]: "obs l3 = id"
by (simp add: l3_def)


(**************************************************************************************************)
subsection ‹Invariants›
(**************************************************************************************************)

subsubsection ‹inv1: No long-term keys as message parts›
(**************************************************************************************************)

definition
  l3_inv1 :: "l3_state set"
where
  "l3_inv1 ≡ {s.
     parts (ik s) ∩ range LtK ⊆ ik s
  }"

lemmas l3_inv1I = l3_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv1E [elim] = l3_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv1D = l3_inv1_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv1D' [dest]: "⟦ LtK K ∈ parts (ik s); s ∈ l3_inv1⟧ ⟹ LtK K ∈ ik s"
by (auto simp add: l3_inv1_def)

lemma l3_inv1_init [iff]:
  "init l3 ⊆ l3_inv1"
by (auto simp add: l3_def l3_init_def intro!:l3_inv1I)

lemma l3_inv1_trans [iff]:
  "{l3_inv1} trans l3 {> l3_inv1}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs intro!: l3_inv1I)
apply (auto simp add: l3_defs dy_fake_msg_def dy_fake_chan_def
        parts_insert [where H="ik _"] parts_insert [where H="insert _ (ik _)"]
        dest!: Fake_parts_insert)
apply (auto dest:analz_into_parts)
done

lemma PO_l3_inv1 [iff]:
  "reach l3 ⊆ l3_inv1"
by (rule inv_rule_basic) (auto)


subsubsection ‹inv2: @{term "bad s"} indeed contains "bad" keys›
(**************************************************************************************************)

definition
  l3_inv2 :: "l3_state set"
where
  "l3_inv2 ≡ {s.
    Keys_bad (ik s) (bad s)
  }"

lemmas l3_inv2I = l3_inv2_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv2E [elim] = l3_inv2_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv2D = l3_inv2_def [THEN setc_def_to_dest, rule_format]


lemma l3_inv2_init [simp,intro!]:
  "init l3 ⊆ l3_inv2"
by (auto simp add: l3_def l3_init_defs intro!:l3_inv2I Keys_badI)

lemma l3_inv2_trans [simp,intro!]:
  "{l3_inv2 ∩ l3_inv1} trans l3 {> l3_inv2}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs intro!: l3_inv2I)
apply (auto simp add: l3_defs dy_fake_msg_def dy_fake_chan_def)
text ‹4 subgoals: dy, lkr*, skr›
apply (auto intro: Keys_bad_insert_Fake Keys_bad_insert_keys_of)
apply (auto intro!: Keys_bad_insert_payload)
done

lemma PO_l3_inv2 [iff]: "reach l3 ⊆ l3_inv2"
by (rule_tac J="l3_inv1" in inv_rule_incr) (auto)



subsubsection ‹inv3›
(**************************************************************************************************)

text ‹If a message can be analyzed from the intruder knowledge then it can
be derived (using @{term "synth"}/@{term "analz"}) from the sets of implementation, 
non-implementation, and long-term key messages and the tags. That is, intermediate messages 
are not needed.
›

definition
  l3_inv3 :: "l3_state set"      
where
  "l3_inv3 ≡ {s.
    analz (ik s) ⊆ 
    synth (analz ((ik s ∩ payload) ∪ ((ik s) ∩ valid) ∪ (ik s ∩ range LtK) ∪ Tags))
  }"

lemmas l3_inv3I = l3_inv3_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv3E = l3_inv3_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv3D = l3_inv3_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv3_init [iff]:
  "init l3 ⊆ l3_inv3"
apply (auto simp add: l3_def l3_init_def intro!: l3_inv3I)
apply (auto simp add: ik_init_def intro!: synth_increasing [THEN [2] rev_subsetD])
done

declare domIff [iff del]

text ‹Most of the cases in this proof are simple and very similar.
The proof could probably be shortened.›
lemma l3_inv3_trans [simp,intro!]:
  "{l3_inv3} trans l3 {> l3_inv3}"
proof (simp add: l3_nostep_defs, safe)
  fix Ra A B
  show "{l3_inv3} l3_step1 Ra A B {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (auto intro!: validI dest!: analz_insert_partition [THEN [2] rev_subsetD])
    done
next
  fix Rb A B gnx
  show "{l3_inv3} l3_step2 Rb A B gnx {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (auto intro!: validI dest!: analz_insert_partition [THEN [2] rev_subsetD])
    done
next
  fix Ra A B gny
  show "{l3_inv3} l3_step3 Ra A B gny {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (auto intro!: validI dest!: analz_insert_partition [THEN [2] rev_subsetD])
    done
next
  fix Rb A B gnx
  show "{l3_inv3} l3_step4 Rb A B gnx {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    done
next
  fix m 
  show "{l3_inv3} l3_dy m {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs dy_fake_chan_def dy_fake_msg_def
                intro!: l3_inv3I dest!: l3_inv3D)
    apply (drule synth_analz_insert)
    apply (blast intro: synth_analz_monotone dest: synth_monotone)
    done
next
  fix A
  show "{l3_inv3} l3_lkr_others A {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (drule analz_Un_partition [of _ "keys_of A"], auto)
    done
next
  fix A
  show "{l3_inv3} l3_lkr_after A {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (drule analz_Un_partition [of _ "keys_of A"], auto)
    done
next
  fix R K
  show "{l3_inv3} l3_skr R K {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (auto dest!: analz_insert_partition [THEN [2] rev_subsetD])
    done
qed

lemma PO_l3_inv3 [iff]: "reach l3 ⊆ l3_inv3"
by (rule inv_rule_basic) (auto)



subsubsection ‹inv4: the intruder knows the tags›
(**************************************************************************************************)

definition
  l3_inv4 :: "l3_state set"
where
  "l3_inv4 ≡ {s.
    Tags ⊆ ik s
  }"

lemmas l3_inv4I = l3_inv4_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv4E [elim] = l3_inv4_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv4D = l3_inv4_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv4_init [simp,intro!]:
  "init l3 ⊆ l3_inv4"
by (auto simp add: l3_def l3_init_def ik_init_def intro!:l3_inv4I)

lemma l3_inv4_trans [simp,intro!]:
  "{l3_inv4} trans l3 {> l3_inv4}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs intro!: l3_inv4I)
apply (auto simp add: l3_defs dy_fake_chan_def dy_fake_msg_def)
done

lemma PO_l3_inv4 [simp,intro!]: "reach l3 ⊆ l3_inv4"
by (rule inv_rule_basic) (auto)


text ‹The remaining invariants are derived from the others.
They are not protocol dependent provided the previous invariants hold.›


subsubsection ‹inv5›
(**************************************************************************************************)

text ‹The messages that the L3 DY intruder can derive from the intruder knowledge 
(using @{term "synth"}/@{term "analz"}), are either implementations or intermediate messages or
can also be derived by the L2 intruder from the set 
@{term "extr (bad s) ((ik s) ∩ payload) (abs (ik s))"}, that is, given the 
non-implementation messages and the abstractions of (implementation) messages
in the intruder knowledge. 
›

definition
  l3_inv5 :: "l3_state set"
where
  "l3_inv5 ≡ {s.
    synth (analz (ik s)) ⊆ 
    dy_fake_msg (bad s) (ik s ∩ payload) (abs (ik s)) ∪ -payload
  }"

lemmas l3_inv5I = l3_inv5_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv5E = l3_inv5_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv5D = l3_inv5_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv5_derived: "l3_inv2 ∩ l3_inv3 ⊆ l3_inv5"
by (auto simp add: abs_validSet dy_fake_msg_def intro!: l3_inv5I
            dest!: l3_inv3D [THEN synth_mono, THEN [2] rev_subsetD]
            dest!: synth_analz_NI_I_K_synth_analz_NI_E [THEN [2] rev_subsetD])

lemma PO_l3_inv5 [simp,intro!]: "reach l3 ⊆ l3_inv5"
using l3_inv5_derived PO_l3_inv2 PO_l3_inv3 
by blast


subsubsection ‹inv6›
(**************************************************************************************************)

text ‹If the level 3 intruder can deduce a message implementing an insecure channel message, then:
\begin{itemize}
  \item either the message is already in the intruder knowledge;
  \item or the message is constructed, and the payload can also be deduced by the intruder.
\end{itemize}
›

definition
  l3_inv6 :: "l3_state set"
where
  "l3_inv6 ≡ {s. ∀ A B M. 
     (implInsec A B M ∈ synth (analz (ik s)) ∧ M ∈ payload) ⟶ 
     (implInsec A B M ∈ ik s ∨ M ∈ synth (analz (ik s)))
  }"

lemmas l3_inv6I = l3_inv6_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv6E = l3_inv6_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv6D = l3_inv6_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv6_derived [simp,intro!]:
  "l3_inv3 ∩ l3_inv4 ⊆ l3_inv6"
apply (auto intro!: l3_inv6I dest!: l3_inv3D)
text ‹1 subgoal›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implInsec_synth_analz [rotated 1, where H="_ ∪ _"])
apply (auto dest!: synth_analz_monotone [of _ "_ ∪ _" "ik _"])
done

lemma PO_l3_inv6 [simp,intro!]: "reach l3 ⊆ l3_inv6"
using l3_inv6_derived PO_l3_inv3 PO_l3_inv4
by (blast)

subsubsection ‹inv7›
(**************************************************************************************************)

text ‹If the level 3 intruder can deduce a message implementing a confidential channel message,
then either 
\begin{itemize}
 \item the message is already in the intruder knowledge, or
 \item the message is constructed, and the payload can also be deduced by the intruder.
\end{itemize}
›

definition
  l3_inv7 :: "l3_state set"
where
  "l3_inv7 ≡ {s. ∀ A B M. 
     (implConfid A B M ∈ synth (analz (ik s)) ∧ M ∈ payload) ⟶ 
     (implConfid A B M ∈ ik s ∨ M ∈ synth (analz (ik s)))
  }"

lemmas l3_inv7I = l3_inv7_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv7E = l3_inv7_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv7D = l3_inv7_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv7_derived [simp,intro!]:
  "l3_inv3 ∩ l3_inv4 ⊆ l3_inv7"
apply (auto intro!: l3_inv7I dest!: l3_inv3D)
text ‹1 subgoal›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implConfid_synth_analz [rotated 1, where H="_ ∪ _"])
apply (auto dest!: synth_analz_monotone [of _ "_ ∪ _" "ik _"])
done

lemma PO_l3_inv7 [simp,intro!]: "reach l3 ⊆ l3_inv7"
using l3_inv7_derived PO_l3_inv3 PO_l3_inv4
by (blast)


subsubsection ‹inv8›
(**************************************************************************************************)

text ‹If the level 3 intruder can deduce a message implementing an authentic channel message 
then either
\begin{itemize}
  \item the message is already in the intruder knowledge, or
  \item the message is constructed, and in this case the payload can also be deduced
     by the intruder, and one of the agents is bad.
\end{itemize}
›

definition
  l3_inv8 :: "l3_state set"
where
  "l3_inv8 ≡ {s. ∀ A B M. 
     (implAuth A B M ∈ synth (analz (ik s)) ∧ M ∈ payload) ⟶ 
     (implAuth A B M ∈ ik s ∨ (M ∈ synth (analz (ik s)) ∧ (A ∈ bad s ∨ B ∈ bad s)))
  }"

lemmas l3_inv8I = l3_inv8_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv8E = l3_inv8_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv8D = l3_inv8_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv8_derived [iff]:
  "l3_inv2 ∩ l3_inv3 ∩ l3_inv4 ⊆ l3_inv8"
apply (auto intro!: l3_inv8I dest!: l3_inv3D l3_inv2D)
text ‹2 subgoals: M is deducible and the agents are bad›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implAuth_synth_analz [rotated 1, where H="_ ∪ _"] elim!: synth_analz_monotone)

apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implAuth_synth_analz [rotated 1, where H="_ ∪ _"] elim!: synth_analz_monotone)
done

lemma PO_l3_inv8 [iff]: "reach l3 ⊆ l3_inv8"
using l3_inv8_derived
  PO_l3_inv3 PO_l3_inv2 PO_l3_inv4
by blast


subsubsection ‹inv9›
(**************************************************************************************************)

text ‹If the level 3 intruder can deduce a message implementing a secure channel message 
then either:
\begin{itemize}
  \item the message is already in the intruder knowledge, or
  \item the message is constructed, and in this case the payload can also be deduced 
 by the intruder, and one of the agents is bad.
\end{itemize}
›

definition
  l3_inv9 :: "l3_state set"
where
  "l3_inv9 ≡ {s. ∀ A B M. 
     (implSecure A B M ∈ synth (analz (ik s)) ∧ M ∈ payload) ⟶ 
     (implSecure A B M ∈ ik s ∨ (M ∈ synth (analz (ik s)) ∧ (A ∈ bad s ∨ B ∈ bad s)))
  }"

lemmas l3_inv9I = l3_inv9_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv9E = l3_inv9_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv9D = l3_inv9_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv9_derived [iff]:
  "l3_inv2 ∩ l3_inv3 ∩ l3_inv4 ⊆ l3_inv9"
apply (auto intro!: l3_inv9I dest!:l3_inv3D l3_inv2D)
text ‹2 subgoals: M is deducible and the agents are bad›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implSecure_synth_analz [rotated 1, where H="_ ∪ _"] 
            elim!: synth_analz_monotone)

apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implSecure_synth_analz [rotated 1, where H="_ ∪ _"])
done

lemma PO_l3_inv9 [iff]: "reach l3 ⊆ l3_inv9"
using l3_inv9_derived
  PO_l3_inv3 PO_l3_inv2 PO_l3_inv4
by blast


(**************************************************************************************************)
subsection ‹Refinement›
(**************************************************************************************************)

text ‹Mediator function.›
definition 
  med23s :: "l3_obs ⇒ l2_obs"
where
  "med23s t ≡ ⦇
    ik = ik t ∩ payload,
    secret = secret t,
    progress = progress t,
    signalsInit = signalsInit t,
    signalsResp = signalsResp t,
    chan = abs (ik t),
    bad = bad t
    ⦈"

text ‹Relation between states.›
definition
  R23s :: "(l2_state * l3_state) set"
where
  "R23s ≡ {(s, s').
    s = med23s s'
    }"

lemmas R23s_defs = R23s_def med23s_def

lemma R23sI: 
  "⟦ ik s = ik t ∩ payload; secret s = secret t; progress s = progress t; 
     signalsInit s = signalsInit t; signalsResp s = signalsResp t; 
     chan s = abs (ik t); l2_state.bad s = bad t ⟧ 
 ⟹ (s, t) ∈ R23s"
by (auto simp add: R23s_def med23s_def)

lemma R23sD: 
  "(s, t) ∈ R23s ⟹
    ik s = ik t ∩ payload ∧ secret s = secret t ∧ progress s = progress t ∧ 
    signalsInit s = signalsInit t ∧ signalsResp s = signalsResp t ∧ 
    chan s = abs (ik t) ∧ l2_state.bad s = bad t"
by (auto simp add: R23s_def med23s_def)

lemma R23sE [elim]: 
  "⟦ (s, t) ∈ R23s;
     ⟦ ik s = ik t ∩ payload; secret s = secret t; progress s = progress t; 
       signalsInit s = signalsInit t; signalsResp s = signalsResp t; 
       chan s = abs (ik t); l2_state.bad s = bad t ⟧ ⟹ P ⟧ 
 ⟹ P"
by (auto simp add: R23s_def med23s_def)

lemma can_signal_R23 [simp]:
  "(s2, s3) ∈ R23s ⟹
   can_signal s2 A B ⟷ can_signal s3 A B"
by (auto simp add: can_signal_def)


subsubsection ‹Protocol events›
(**************************************************************************************************)

lemma l3_step1_refines_step1:
  "{R23s} l2_step1 Ra A B, l3_step1 Ra A B {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_step1_def)
done

lemma l3_step2_refines_step2:
  "{R23s} l2_step2 Rb A B gnx, l3_step2 Rb A B gnx{>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs l2_step2_def)
apply (auto simp add: l3_step2_def)
done

lemma l3_step3_refines_step3:
  "{R23s} l2_step3 Ra A B gny, l3_step3 Ra A B gny {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs l2_step3_def)
apply (auto simp add: l3_step3_def)
done

lemma l3_step4_refines_step4:
  "{R23s} l2_step4 Rb A B gnx, l3_step4 Rb A B gnx {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs l2_step4_def)
apply (auto simp add: l3_step4_def)
done

subsubsection ‹Intruder events›
(**************************************************************************************************)

lemma l3_dy_payload_refines_dy_fake_msg:
  "M ∈ payload ⟹
   {R23s ∩ UNIV × l3_inv5} l2_dy_fake_msg M, l3_dy M {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_dy_fake_msg_def dest: l3_inv5D)
done

lemma l3_dy_valid_refines_dy_fake_chan:
  "⟦ M ∈ valid; M' ∈ abs {M} ⟧ ⟹
   {R23s ∩ UNIV × (l3_inv5 ∩ l3_inv6 ∩ l3_inv7 ∩ l3_inv8 ∩ l3_inv9)} 
      l2_dy_fake_chan M', l3_dy M 
   {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs, simp add: l2_dy_fake_chan_def)
apply (auto simp add: l3_defs)
text ‹1 subgoal›
apply (erule valid_cases, simp_all add: dy_fake_chan_def)
  text ‹Insec›
  apply (blast dest: l3_inv6D l3_inv5D)
  text ‹Confid›
  apply (blast dest: l3_inv7D l3_inv5D)
  text ‹Auth›
  apply (blast dest: l3_inv8D l3_inv5D)
  text ‹Secure›
  apply (blast dest: l3_inv9D l3_inv5D)
done


lemma l3_dy_valid_refines_dy_fake_chan_Un:
  "M ∈ valid ⟹
   {R23s ∩ UNIV × (l3_inv5 ∩ l3_inv6 ∩ l3_inv7 ∩ l3_inv8 ∩ l3_inv9)} 
      ⋃M'. l2_dy_fake_chan M', l3_dy M 
   {>R23s}"
by (auto dest: valid_abs intro: l3_dy_valid_refines_dy_fake_chan)


lemma l3_dy_isLtKey_refines_skip:
  "{R23s} Id, l3_dy (LtK ltk) {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs l3_defs)
apply (auto elim!: absE)
done

lemma l3_dy_others_refines_skip:
  "⟦ M ∉ range LtK; M ∉ valid; M ∉ payload ⟧ ⟹ 
   {R23s} Id, l3_dy M {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)     (* auto SLOW *)
apply (auto simp add: l3_defs)
apply (auto elim!: absE intro: validI)
done


lemma l3_dy_refines_dy_fake_msg_dy_fake_chan_skip:
   "{R23s ∩ UNIV × (l3_inv5 ∩ l3_inv6 ∩ l3_inv7 ∩ l3_inv8 ∩ l3_inv9)} 
      l2_dy_fake_msg M ∪ (⋃M'. l2_dy_fake_chan M') ∪ Id, l3_dy M 
    {>R23s}"
by (cases "M ∈ payload ∪ valid ∪ range LtK")
   (auto dest: l3_dy_payload_refines_dy_fake_msg l3_dy_valid_refines_dy_fake_chan_Un 
         intro: l3_dy_isLtKey_refines_skip dest!: l3_dy_others_refines_skip)


subsubsection ‹Compromise events›
(**************************************************************************************************)

lemma l3_lkr_others_refines_lkr_others:
  "{R23s} l2_lkr_others A, l3_lkr_others A {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_lkr_others_def)
done

lemma l3_lkr_after_refines_lkr_after:
  "{R23s} l2_lkr_after A, l3_lkr_after A {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_lkr_after_def)
done

lemma l3_skr_refines_skr:
  "{R23s} l2_skr R K, l3_skr R K {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_skr_def)
done



lemmas l3_trans_refines_l2_trans = 
  l3_step1_refines_step1 l3_step2_refines_step2 l3_step3_refines_step3 l3_step4_refines_step4
  l3_dy_refines_dy_fake_msg_dy_fake_chan_skip
  l3_lkr_others_refines_lkr_others l3_lkr_after_refines_lkr_after l3_skr_refines_skr



lemma l3_refines_init_l2 [iff]:
  "init l3 ⊆ R23s `` (init l2)"
by (auto simp add: R23s_defs l2_defs l3_def l3_init_def)

lemma l3_refines_trans_l2 [iff]:
  "{R23s ∩ (UNIV × (l3_inv1 ∩ l3_inv2 ∩ l3_inv3 ∩ l3_inv4))} trans l2, trans l3 {> R23s}"
proof -
  let ?pre' = "R23s ∩ (UNIV × (l3_inv5 ∩ l3_inv6 ∩ l3_inv7 ∩ l3_inv8 ∩ l3_inv9))"
  show ?thesis (is "{?pre} ?t1, ?t2 {>?post}")
  proof (rule relhoare_conseq_left)
    show "?pre ⊆ ?pre'"
      using l3_inv5_derived l3_inv6_derived l3_inv7_derived l3_inv8_derived l3_inv9_derived 
      by blast
  next 
    show "{?pre'} ?t1, ?t2 {> ?post}" 
      by (auto simp add: l2_def l3_def l2_trans_def l3_trans_def
               intro!: l3_trans_refines_l2_trans)
  qed
qed    

lemma PO_obs_consistent_R23s [iff]: 
  "obs_consistent R23s med23s l2 l3"
by (auto simp add: obs_consistent_def R23s_def med23s_def l2_defs)


lemma l3_refines_l2 [iff]:
  "refines 
     (R23s ∩ 
      (reach l2 × (l3_inv1 ∩ l3_inv2 ∩ l3_inv3 ∩ l3_inv4)))
     med23s l2 l3"
by (rule Refinement_using_invariants, auto)

lemma l3_implements_l2 [iff]:
  "implements med23s l2 l3"
by (rule refinement_soundness) (auto)


(**************************************************************************************************)
subsection ‹Derived invariants›
(**************************************************************************************************)

subsubsection ‹inv10: secrets contain no implementation material›
(**************************************************************************************************)

definition
  l3_inv10 :: "l3_state set"
where
  "l3_inv10 ≡ {s.
    secret s ⊆ payload
  }"

lemmas l3_inv10I = l3_inv10_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv10E = l3_inv10_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv10D = l3_inv10_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv10_init [iff]: 
  "init l3 ⊆ l3_inv10"
by (auto simp add: l3_def l3_init_def ik_init_def intro!:l3_inv10I)

lemma l3_inv10_trans [iff]:
  "{l3_inv10} trans l3 {> l3_inv10}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs)
apply (auto simp add: l3_defs l3_inv10_def)
done

lemma PO_l3_inv10 [iff]: "reach l3 ⊆ l3_inv10"
by (rule inv_rule_basic) (auto)

lemma l3_obs_inv10 [iff]: "oreach l3 ⊆ l3_inv10"
by (auto simp add: oreach_def)



subsubsection ‹Partial secrecy›
(**************************************************************************************************)

text ‹We want to prove @{term "l3_secrecy"}, i.e.,
  @{term "synth (analz (ik s)) ∩ secret s = {}"},
  but by refinement we only get @{term "l3_partial_secrecy"}: 
    @{term "dy_fake_msg (bad s) (payloadSet (ik s)) (abs (ik s)) ∩ secret s = {}"}.
  This is fine if secrets contain no implementation material.
  Then, by @{term "inv5"}, a message in @{term "synth (analz (ik s))"} is in
    @{term "dy_fake_msg (bad s) (payloadSet (ik s)) (abs (ik s)) ∪ -payload"},
  and @{term "l3_partial_secrecy"} proves it is not a secret.
›

definition
  l3_partial_secrecy :: "('a l3_state_scheme) set"
where
  "l3_partial_secrecy ≡ {s. 
    dy_fake_msg (bad s) (ik s ∩ payload) (abs (ik s)) ∩ secret s = {}
  }"


lemma l3_obs_partial_secrecy [iff]: "oreach l3 ⊆ l3_partial_secrecy"
apply (rule external_invariant_translation [OF l2_obs_secrecy _ l3_implements_l2])
apply (auto simp add: med23s_def l2_secrecy_def l3_partial_secrecy_def)
done


subsubsection ‹Secrecy›
(**************************************************************************************************)

definition 
  l3_secrecy :: "('a l3_state_scheme) set"
where
  "l3_secrecy ≡ l1_secrecy"

lemma l3_obs_inv5: "oreach l3 ⊆ l3_inv5"
by (auto simp add: oreach_def)

lemma l3_obs_secrecy [iff]: "oreach l3 ⊆ l3_secrecy"
apply (rule, frule l3_obs_inv5 [THEN [2] rev_subsetD], frule l3_obs_inv10 [THEN [2] rev_subsetD])
apply (auto simp add: med23s_def l2_secrecy_def l3_secrecy_def s0_secrecy_def l3_inv10_def)
using l3_partial_secrecy_def apply (blast dest!: l3_inv5D subsetD [OF l3_obs_partial_secrecy])
done

lemma l3_secrecy [iff]: "reach l3 ⊆ l3_secrecy"
by (rule external_to_internal_invariant [OF l3_obs_secrecy], auto)


subsubsection ‹Injective agreement›
(**************************************************************************************************)

abbreviation "l3_iagreement_Init ≡ l1_iagreement_Init"

lemma l3_obs_iagreement_Init [iff]: "oreach l3 ⊆ l3_iagreement_Init"
apply (rule external_invariant_translation 
         [OF l2_obs_iagreement_Init _ l3_implements_l2])
apply (auto simp add: med23s_def l1_iagreement_Init_def)
done

lemma l3_iagreement_Init [iff]: "reach l3 ⊆ l3_iagreement_Init"
by (rule external_to_internal_invariant [OF l3_obs_iagreement_Init], auto)

abbreviation "l3_iagreement_Resp ≡ l1_iagreement_Resp"

lemma l3_obs_iagreement_Resp [iff]: "oreach l3 ⊆ l3_iagreement_Resp"
apply (rule external_invariant_translation 
         [OF l2_obs_iagreement_Resp _ l3_implements_l2])
apply (auto simp add: med23s_def l1_iagreement_Resp_def)
done

lemma l3_iagreement_Resp [iff]: "reach l3 ⊆ l3_iagreement_Resp"
by (rule external_to_internal_invariant [OF l3_obs_iagreement_Resp], auto)

end
end