Theory m2_ds

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

  Project: Development of Security Protocols by Refinement

  Module:  Key_establish/m2_ds.thy (Isabelle/HOL 2016-1)
  ID:      $Id: m2_ds.thy 132890 2016-12-24 10:25:57Z csprenge $
  Author:  Ivano Somaini, ETH Zurich <somainii@student.ethz.ch>
           Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>

  Key distribution protocols
  Level 2: channel protocol, parallel version of Denning-Sacco

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

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

section ‹Abstract Denning-Sacco protocol (L2)›

theory m2_ds imports m1_ds "../Refinement/Channels"
begin

text ‹
We model an abstract version of the Denning-Sacco protocol:
\[
\begin{array}{lll}
  \mathrm{M1.} & A \rightarrow S: & A, B \\ 
  \mathrm{M2.} & S \rightarrow A: & \{B, Kab, T,\{Kab, A, T\}_{Kbs} \}_{Kas} \\
  \mathrm{M3.} & A \rightarrow B: & \{Kab, A, T\}_{Kbs} \\
\end{array}
\]

This refinement introduces channels with security properties.  We model 
a parallel version of the DS protocol:
\[
\begin{array}{lll}
  \mathrm{M1.} & A \rightarrow S: & A, B \\ 
  \mathrm{M2a.} & S \rightarrow A: & \{B, Kab, T\}_{Kas} \\
  \mathrm{M2b.} & S \rightarrow B: & \{Kab, A, T\}_{Kbs} \\
\end{array}
\]
Message 1 is sent over an insecure channel, the other two message over
secure channels.
›

declare domIff [simp, iff del]


(******************************************************************************)
subsection ‹State›
(******************************************************************************)

text ‹State and observations›

record m2_state = "m1_state" +
  chan :: "chmsg set"              ― ‹channel messages›

type_synonym 
  m2_obs = "m1_state" 

definition 
  m2_obs :: "m2_state ⇒ m2_obs" where
  "m2_obs s ≡ ⦇ 
     runs = runs s,
     leak = leak s,
     clk = clk s
  ⦈"

type_synonym
  m2_pred = "m2_state set"

type_synonym
  m2_trans = "(m2_state × m2_state) set"


(******************************************************************************)
subsection ‹Events›
(******************************************************************************)

text ‹Protocol events.›

definition     ― ‹by @{term "A"}, refines @{term "m1a_step1"}›
  m2_step1 :: "[rid_t, agent, agent] ⇒ m2_trans"
where
  "m2_step1 Ra A B ≡ {(s, s1).

     ― ‹guards:›
     Ra ∉ dom (runs s) ∧                                ― ‹‹Ra› is fresh›

     ― ‹actions:›
     ― ‹create initiator thread and send message 1›
     s1 = s⦇
       runs := (runs s)(Ra ↦ (Init, [A, B], [])),
       chan := insert (Insec A B (Msg [])) (chan s)     ― ‹send M1›
     ⦈
  }"

definition     ― ‹by @{term "B"}, refines @{term "m1e_step2"}›
  m2_step2 :: "[rid_t, agent, agent] ⇒ m2_trans"
where
  "m2_step2 ≡ m1_step2"

definition     ― ‹by @{text "Server"}, refines @{term m1e_step3}›
  m2_step3 :: "[rid_t, agent, agent, key, time] ⇒ m2_trans"
where
  "m2_step3 Rs A B Kab Ts ≡ {(s, s1). 

     ― ‹guards:›
     Rs ∉ dom (runs s) ∧                           ― ‹fresh server run›
     Kab = sesK (Rs$sk) ∧                          ― ‹fresh session key›
     Ts = clk s ∧                                  ― ‹fresh timestamp› 

     Insec A B (Msg []) ∈ chan s ∧                 ― ‹recv M1›
   
     ― ‹actions:›
     ― ‹record key and send messages 2 and 3›
     s1 = s⦇
       runs := (runs s)(Rs ↦ (Serv, [A, B], [aNum Ts])), 
       chan := {Secure Sv A (Msg [aAgt B, aKey Kab, aNum Ts]),    ― ‹send ‹M2a/b››
                Secure Sv B (Msg [aKey Kab, aAgt A, aNum Ts])} ∪ chan s
     ⦈
  }"

definition     ― ‹by @{term "A"}, refines @{term m1e_step4}›
  m2_step4 :: "[rid_t, agent, agent, key, time] ⇒ m2_trans"
where
  "m2_step4 Ra A B Kab Ts ≡ {(s, s1).

     ― ‹guards:›
     runs s Ra = Some (Init, [A, B], []) ∧ 
     Secure Sv A (Msg [aAgt B, aKey Kab, aNum Ts]) ∈ chan s ∧  ― ‹recv ‹M2a››

     clk s < Ts + Ls ∧                              ― ‹ensure key freshness›

     ― ‹actions:›
     ― ‹record session key›
     s1 = s⦇
       runs := (runs s)(Ra ↦ (Init, [A, B], [aKey Kab, aNum Ts]))
     ⦈
  }"

definition     ― ‹by @{term "B"}, refines @{term m1e_step5}›
  m2_step5 :: "[rid_t, agent, agent, key, time] ⇒ m2_trans"
where
  "m2_step5 Rb A B Kab Ts ≡ {(s, s1). 

     ― ‹guards:›
     runs s Rb = Some (Resp, [A, B], []) ∧
     Secure Sv B (Msg [aKey Kab, aAgt A, aNum Ts]) ∈ chan s ∧  ― ‹recv ‹M2b››

     ― ‹ensure freshness of session key›
     clk s < Ts + Ls ∧

     ― ‹actions:›
     ― ‹record session key›
     s1 = s⦇
       runs := (runs s)(Rb ↦ (Resp, [A, B], [aKey Kab, aNum Ts]))
     ⦈
  }"

text ‹Clock tick event›

definition     ― ‹refines @{term m1_tick}›
  m2_tick :: "time ⇒ m2_trans" 
where
  "m2_tick ≡ m1_tick"


text ‹Session key compromise.›

definition     ― ‹refines @{term m1_leak}› 
  m2_leak :: "rid_t ⇒ m2_trans"
where
  "m2_leak Rs ≡ {(s, s1).
    ― ‹guards:›
    Rs ∈ dom (runs s) ∧
    fst (the (runs s Rs)) = Serv ∧         ― ‹compromise server run ‹Rs››

    ― ‹actions:›
    ― ‹record session key as leaked;›
    ― ‹intruder sends himself an insecure channel message containing the key›
    s1 = s⦇ leak := insert (sesK (Rs$sk)) (leak s), 
            chan := insert (Insec undefined undefined (Msg [aKey (sesK (Rs$sk))])) (chan s) ⦈ 
  }"


text ‹Intruder fake event (new).›

definition     ― ‹refines @{term Id}› 
  m2_fake :: "m2_trans"
where
  "m2_fake ≡ {(s, s1). 

     ― ‹actions:›
     s1 = s⦇
       ― ‹close under fakeable messages›
       chan := fake ik0 (dom (runs s)) (chan s) 
     ⦈
  }"


(******************************************************************************)
subsection ‹Transition system›
(******************************************************************************)

definition 
  m2_init :: "m2_pred"
where
  "m2_init ≡ { ⦇
     runs = Map.empty,
     leak = corrKey,
     clk = 0,
     chan = {}              ― ‹‹Channels.ik0› contains ‹aKey`corrKey››
  ⦈ }"

definition 
  m2_trans :: "m2_trans" where
  "m2_trans ≡ (⋃A B Ra Rb Rs Kab Ts T.
     m2_step1 Ra A B ∪
     m2_step2 Rb A B ∪
     m2_step3 Rs A B Kab Ts ∪
     m2_step4 Ra A B Kab Ts ∪
     m2_step5 Rb A B Kab Ts ∪
     m2_tick T ∪
     m2_leak Rs ∪
     m2_fake ∪
     Id
  )"

definition 
  m2 :: "(m2_state, m2_obs) spec" where
  "m2 ≡ ⦇
    init = m2_init,
    trans = m2_trans,
    obs = m2_obs
  ⦈"

lemmas m2_loc_defs = 
  m2_def m2_init_def m2_trans_def m2_obs_def
  m2_step1_def m2_step2_def m2_step3_def m2_step4_def m2_step5_def 
  m2_tick_def m2_leak_def m2_fake_def 

lemmas m2_defs = m2_loc_defs m1_defs


(******************************************************************************)
subsection ‹Invariants and simulation relation›
(******************************************************************************)

(*
subsubsection {* inv1: Key definedness [UNUSED] *}
(******************************************************************************)

text {* All session keys in channel messages stem from existing runs. *}

definition 
  m2_inv1_keys :: "m2_state set"
where 
  "m2_inv1_keys ≡ {s. ∀R.
     aKey (sesK (R$sk)) ∈ atoms (chan s) (* ∨ sesK (R$sk) ∈ leak s *) ⟶ 
       R ∈ dom (runs s)
  }"

lemmas m2_inv1_keysI = 
  m2_inv1_keys_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv1_keysE [elim] = 
  m2_inv1_keys_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv1_keysD = 
  m2_inv1_keys_def [THEN setc_def_to_dest, rule_format]


text {* Invariance proof. *}

lemma PO_m2_inv1_keys_init [iff]:
  "init m2 ⊆ m2_inv1_keys"
by (auto simp add: m2_defs intro!: m2_inv1_keysI)

lemma PO_m2_inv1_keys_trans [iff]:
  "{m2_inv1_keys} trans m2 {> m2_inv1_keys}"
by (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv1_keysI)
   (auto simp add: ik0_def dest: m2_inv1_keysD dom_lemmas)

lemma PO_m2_inv1_keys [iff]: "reach m2 ⊆ m2_inv1_keys"
by (rule inv_rule_basic) (auto)


subsubsection {* inv2: Definedness of used keys [UNUSED] *}
(******************************************************************************)

definition 
  m2_inv2_keys_for :: "m2_state set"
where 
  "m2_inv2_keys_for ≡ {s. ∀R.
     sesK (R$sk) ∈ keys_for (chan s) ⟶ R ∈ dom (runs s)
  }"

lemmas m2_inv2_keys_forI = 
  m2_inv2_keys_for_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv2_keys_forE [elim] = 
  m2_inv2_keys_for_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv2_keys_forD = 
  m2_inv2_keys_for_def [THEN setc_def_to_dest, rule_format, rotated 1]


text {* Invariance proof. *}

lemma PO_m2_inv2_keys_for_init [iff]:
  "init m2 ⊆ m2_inv2_keys_for"
by (auto simp add: m2_defs intro!: m2_inv2_keys_forI)

lemma PO_m2_inv2_keys_for_trans [iff]:
  "{m2_inv2_keys_for ∩ m2_inv1_keys} trans m2 {> m2_inv2_keys_for}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv2_keys_forI) 
-- {* 1 subgoal, from fake *}
apply (auto simp add: keys_for_def ik0_def, erule fake.cases, fastforce+)
done

lemma PO_m2_inv2_keys_for [iff]: "reach m2 ⊆ m2_inv2_keys_for"
by (rule inv_rule_incr) (auto del: subsetI)


text {* Useful application of invariant. *}

lemma m2_inv2_keys_for__extr_insert_key:                   (* OBSOLETE?! *)
  "⟦ R ∉ dom (runs s); s ∈ m2_inv2_keys_for ⟧
 ⟹ extr (insert (aKey (sesK (R$sk))) T) (chan s) 
     = insert (aKey (sesK (R$sk))) (extr T (chan s))"
by (subgoal_tac "sesK (R$sk) ∉ keys_for (chan s)") 
   (auto)
*)

subsubsection ‹inv3a: Session key compromise›
(******************************************************************************)

text ‹A L2 version of a session key comprise invariant. Roughly, it states
that adding a set of keys @{term KK} to the parameter ‹T› of @{term extr} 
does not help the intruder to extract keys other than those in @{term KK} or
extractable without adding @{term KK}.
›

definition 
  m2_inv3a_sesK_compr :: "m2_state set"
where 
  "m2_inv3a_sesK_compr ≡ {s. ∀K KK.
     aKey K ∈ extr (aKey`KK ∪ ik0) (chan s) ⟷ (K ∈ KK ∨ aKey K ∈ extr ik0 (chan s)) 
  }"

lemmas m2_inv3a_sesK_comprI = 
  m2_inv3a_sesK_compr_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv3a_sesK_comprE [elim] = 
  m2_inv3a_sesK_compr_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv3a_sesK_comprD = 
  m2_inv3a_sesK_compr_def [THEN setc_def_to_dest, rule_format]

text ‹Additional lemma›
lemmas insert_commute_aKey = insert_commute [where x="aKey K" for K] 

lemmas m2_inv3a_sesK_compr_simps = 
  m2_inv3a_sesK_comprD
  m2_inv3a_sesK_comprD [where KK="insert Kab KK" for Kab KK, simplified]
  m2_inv3a_sesK_comprD [where KK="{Kab}" for Kab, simplified]
  insert_commute_aKey   ― ‹to get the keys to the front›

lemma PO_m2_inv3a_sesK_compr_init [iff]:
  "init m2 ⊆ m2_inv3a_sesK_compr"
by (auto simp add: m2_defs intro!: m2_inv3a_sesK_comprI)

lemma PO_m2_inv3a_sesK_compr_trans [iff]:
  "{m2_inv3a_sesK_compr} trans m2 {> m2_inv3a_sesK_compr}"
by (auto simp add: PO_hoare_defs m2_defs m2_inv3a_sesK_compr_simps intro!: m2_inv3a_sesK_comprI)

lemma PO_m2_inv3a_sesK_compr [iff]: "reach m2 ⊆ m2_inv3a_sesK_compr"
by (rule inv_rule_basic) (auto) 


subsubsection ‹inv3: Extracted session keys›
(******************************************************************************)

text ‹inv3: Extracted non-leaked session keys were generated by the server 
for at least one bad agent. This invariant is needed in the proof of the 
strengthening of the authorization guards in steps 4 and 5 
(e.g., @{term "(Kab, A) ∈ azC (runs s)"} for the initiator's step4).›

definition 
  m2_inv3_extrKey :: "m2_state set"
where
  "m2_inv3_extrKey ≡ {s. ∀K.
     aKey K ∈ extr ik0 (chan s) ⟶  K ∉ leak s ⟶ ― ‹was: ‹K ∉ corrKey ⟶››
       (∃R A' B' Ts'. K = sesK (R$sk) ∧
          runs s R = Some (Serv, [A', B'], [aNum Ts']) ∧ 
                    (A' ∈ bad ∨ B' ∈ bad))
  }"

lemmas m2_inv3_extrKeyI = 
  m2_inv3_extrKey_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv3_extrKeyE [elim] = 
  m2_inv3_extrKey_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv3_extrKeyD = 
  m2_inv3_extrKey_def [THEN setc_def_to_dest, rule_format, rotated 1]

lemma PO_m2_inv3_extrKey_init [iff]:
  "init m2 ⊆ m2_inv3_extrKey"
by (auto simp add: m2_defs ik0_def intro!: m2_inv3_extrKeyI)

lemma PO_m2_inv3_extrKey_trans [iff]:
  "{m2_inv3_extrKey ∩ m2_inv3a_sesK_compr} 
      trans m2 
   {> m2_inv3_extrKey}"
proof (simp add: m2_def m2_trans_def, safe)
  fix Rs A B Kab Ts
  show
    "{m2_inv3_extrKey ∩ m2_inv3a_sesK_compr} m2_step3 Rs A B Kab Ts {> m2_inv3_extrKey}"
  apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv3_extrKeyI)
  apply (auto simp add: m2_inv3a_sesK_compr_simps 
              dest!: m2_inv3_extrKeyD dest: dom_lemmas)
  done
next
  fix Ra A B Kab Ts
  show 
    "{m2_inv3_extrKey ∩ m2_inv3a_sesK_compr} m2_step4 Ra A B Kab Ts {> m2_inv3_extrKey}"
  apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv3_extrKeyI)
  apply (auto simp add: dest!: m2_inv3_extrKeyD dest: dom_lemmas) 
  apply (auto intro!: exI)
  done
next 
  fix Rb A B Kab Ts
  show 
    "{m2_inv3_extrKey ∩ m2_inv3a_sesK_compr} m2_step5 Rb A B Kab Ts {> m2_inv3_extrKey}"
  apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv3_extrKeyI)
  apply (auto dest!: m2_inv3_extrKeyD dest: dom_lemmas) 
  apply (auto intro!: exI)
  done
next 
  fix Rs
  show
    "{m2_inv3_extrKey ∩ m2_inv3a_sesK_compr} m2_leak Rs {> m2_inv3_extrKey}"
  apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv3_extrKeyI)
  apply (auto simp add: m2_inv3a_sesK_compr_simps)
  done
qed (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv3_extrKeyI,
     auto dest!: m2_inv3_extrKeyD dest: dom_lemmas)


lemma PO_m2_inv3_extrKey [iff]: "reach m2 ⊆ m2_inv3_extrKey"
by (rule_tac J="m2_inv3a_sesK_compr" in inv_rule_incr) (auto) 



subsubsection ‹inv4: Messages M2a/M2b for good agents and server state›
(******************************************************************************)

text ‹inv4: Secure messages to honest agents and server state; one variant 
for each of M2a and M2b. These invariants establish guard strengthening for
server authentication by the initiator and the responder.›

definition 
  m2_inv4_M2a :: "m2_state set"
where
  "m2_inv4_M2a ≡ {s. ∀A B Kab Ts.
     Secure Sv A (Msg [aAgt B, aKey Kab, aNum Ts]) ∈ chan s ⟶ A ∈ good ⟶
       (∃Rs. Kab = sesK (Rs$sk) ∧
          runs s Rs = Some (Serv, [A, B], [aNum Ts]))
  }"

definition 
  m2_inv4_M2b :: "m2_state set"
where
  "m2_inv4_M2b ≡ {s. ∀A B Kab Ts.
     Secure Sv B (Msg [aKey Kab, aAgt A, aNum Ts]) ∈ chan s ⟶ B ∈ good ⟶
        (∃Rs. Kab = sesK (Rs$sk) ∧
           runs s Rs = Some (Serv, [A, B], [aNum Ts]))
  }"

lemmas m2_inv4_M2aI = 
  m2_inv4_M2a_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv4_M2aE [elim] = 
  m2_inv4_M2a_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv4_M2aD = 
  m2_inv4_M2a_def [THEN setc_def_to_dest, rule_format, rotated 1]

lemmas m2_inv4_M2bI = m2_inv4_M2b_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv4_M2bE [elim] = 
  m2_inv4_M2b_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv4_M2bD = 
  m2_inv4_M2b_def [THEN setc_def_to_dest, rule_format, rotated 1]


text ‹Invariance proofs.›

lemma PO_m2_inv4_M2a_init [iff]:
  "init m2 ⊆ m2_inv4_M2a"
by (auto simp add: m2_defs intro!: m2_inv4_M2aI)

lemma PO_m2_inv4_M2a_trans [iff]:
  "{m2_inv4_M2a} trans m2 {> m2_inv4_M2a}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv4_M2aI)
apply (auto dest!: m2_inv4_M2aD dest: dom_lemmas)
― ‹3 subgoals›
apply (force dest!: spec)+
done

lemma PO_m2_inv4_M2a [iff]: "reach m2 ⊆ m2_inv4_M2a"
by (rule inv_rule_basic) (auto)


lemma PO_m2_inv4_M2b_init [iff]:
  "init m2 ⊆ m2_inv4_M2b"
by (auto simp add: m2_defs intro!: m2_inv4_M2bI)

lemma PO_m2_inv4_M2b_trans [iff]:
  "{m2_inv4_M2b} trans m2 {> m2_inv4_M2b}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv4_M2bI) 
apply (auto dest!: m2_inv4_M2bD dest: dom_lemmas)
― ‹3 subgoals›
apply (force dest!: spec)+
done

lemma PO_m2_inv4_M2b [iff]: "reach m2 ⊆ m2_inv4_M2b"
by (rule inv_rule_incr) (auto del: subsetI)


text ‹Consequence needed in proof of inv8/step5 and inv9/step4: The 
session key uniquely identifies other fields in M2a and M2b, provided it 
is secret.›

lemma m2_inv4_M2a_M2b_match:
  "⟦ Secure Sv A' (Msg [aAgt B', aKey Kab, aNum Ts']) ∈ chan s; 
     Secure Sv B (Msg [aKey Kab, aAgt A, aNum Ts]) ∈ chan s; 
     aKey Kab ∉ extr ik0 (chan s); s ∈ m2_inv4_M2a; s ∈ m2_inv4_M2b ⟧
  ⟹ A = A' ∧ B = B' ∧ Ts = Ts'"
apply (subgoal_tac "A' ∉ bad ∧ B ∉ bad", auto)
apply (auto dest!: m2_inv4_M2aD m2_inv4_M2bD)
done


text ‹More consequences of invariants. Needed in ref/step4 and ref/step5 
respectively to show the strengthening of the authorization guards.›

lemma m2_inv34_M2a_authorized:
  assumes "Secure Sv A (Msg [aAgt B, aKey K, aNum T]) ∈ chan s" 
          "s ∈ m2_inv3_extrKey" "s ∈ m2_inv4_M2a" "K ∉ leak s"  
  shows   "(K, A) ∈ azC (runs s)"
proof (cases "A ∈ bad")
  case True 
  from assms(1) ‹A ∈ bad› have "aKey K ∈ extr ik0 (chan s)" by auto
  with ‹s ∈ m2_inv3_extrKey› ‹K ∉ leak s› show ?thesis by auto 
next
  case False 
  with assms show ?thesis by (auto dest: m2_inv4_M2aD) 
qed

lemma m2_inv34_M2b_authorized:
  assumes "Secure Sv B (Msg [aKey K, aAgt A, aNum T]) ∈ chan s" 
          "s ∈ m2_inv3_extrKey" "s ∈ m2_inv4_M2b" "K ∉ leak s"  
  shows  "(K, B) ∈ azC (runs s)"
proof (cases "B ∈ bad")
  case True 
  from assms(1) ‹B ∈ bad› have "aKey K ∈ extr ik0 (chan s)" by auto
  with ‹s ∈ m2_inv3_extrKey› ‹K ∉ leak s› show ?thesis by auto 
next
  case False 
  with assms show ?thesis by (auto dest: m2_inv4_M2bD) 
qed


subsubsection ‹inv5: Key secrecy for server›
(******************************************************************************)

text ‹inv5: Key secrecy from server perspective. This invariant links the 
abstract notion of key secrecy to the intruder key knowledge.›

definition 
  m2_inv5_ikk_sv :: "m2_state set"
where
  "m2_inv5_ikk_sv ≡ {s. ∀R A B al.
     runs s R = Some (Serv, [A, B], al) ⟶ A ∈ good ⟶ B ∈ good ⟶
     aKey (sesK (R$sk)) ∈ extr ik0 (chan s) ⟶
       sesK (R$sk) ∈ leak s
  }"

lemmas m2_inv5_ikk_svI = 
  m2_inv5_ikk_sv_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv5_ikk_svE [elim] = 
  m2_inv5_ikk_sv_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv5_ikk_svD = 
  m2_inv5_ikk_sv_def [THEN setc_def_to_dest, rule_format, rotated 1]


text ‹Invariance proof.›

lemma PO_m2_inv5_ikk_sv_init [iff]:
  "init m2 ⊆ m2_inv5_ikk_sv"
by (auto simp add: m2_defs intro!: m2_inv5_ikk_svI)

lemma PO_m2_inv5_ikk_sv_trans [iff]:
  "{m2_inv5_ikk_sv ∩ m2_inv3a_sesK_compr ∩ m2_inv3_extrKey} 
     trans m2 
   {> m2_inv5_ikk_sv}"
by (simp add: PO_hoare_defs m2_defs, safe intro!: m2_inv5_ikk_svI)
   (auto simp add: m2_inv3a_sesK_compr_simps dest: dom_lemmas)

lemma PO_m2_inv5_ikk_sv [iff]: "reach m2 ⊆ m2_inv5_ikk_sv"
by (rule_tac J="m2_inv3_extrKey ∩ m2_inv3a_sesK_compr" in inv_rule_incr) (auto)


subsubsection ‹inv6/7: Key secrecy for initiator and responder›
(******************************************************************************)

text ‹These invariants are derivable.›

definition 
  m2_inv6_ikk_init :: "m2_state set"
where
  "m2_inv6_ikk_init ≡ {s. ∀A B Ra K Ts nl.
     runs s Ra = Some (Init, [A, B], aKey K # aNum Ts # nl) ⟶ 
     A ∈ good ⟶ B ∈ good ⟶ aKey K ∈ extr ik0 (chan s) ⟶ 
       K ∈ leak s
  }"

lemmas m2_inv6_ikk_initI = m2_inv6_ikk_init_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv6_ikk_initE [elim] = m2_inv6_ikk_init_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv6_ikk_initD = m2_inv6_ikk_init_def [THEN setc_def_to_dest, rule_format, rotated 1]


definition 
  m2_inv7_ikk_resp :: "m2_state set"
where
  "m2_inv7_ikk_resp ≡ {s. ∀A B Rb K Ts nl.
     runs s Rb = Some (Resp, [A, B], aKey K # aNum Ts # nl) ⟶ 
     A ∈ good ⟶ B ∈ good ⟶ aKey K ∈ extr ik0 (chan s) ⟶
       K ∈ leak s
  }"

lemmas m2_inv7_ikk_respI = m2_inv7_ikk_resp_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv7_ikk_respE [elim] = m2_inv7_ikk_resp_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv7_ikk_respD = m2_inv7_ikk_resp_def [THEN setc_def_to_dest, rule_format, rotated 1]


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

text ‹The simulation relation. This is a pure superposition refinement.›

definition
  R12 :: "(m1_state × m2_state) set" where
  "R12 ≡ {(s, t). runs s = runs t ∧ leak s = leak t ∧ clk s = clk t}"

text ‹The mediator function is the identity.›

definition 
  med21 :: "m2_obs ⇒ m1_obs" where
  "med21 = id"


text ‹Refinement proof.›

lemma PO_m2_step1_refines_m1_step1:
  "{R12} 
     (m1_step1 Ra A B), (m2_step1 Ra A B) 
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, auto)

lemma PO_m2_step2_refines_m1_step2:
  "{R12} 
     (m1_step2 Rb A B), (m2_step2 Rb A B)
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, auto)

lemma PO_m2_step3_refines_m1_step3:
  "{R12} 
     (m1_step3 Rs A B Kab Ts), (m2_step3 Rs A B Kab Ts)
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, auto)

lemma PO_m2_step4_refines_m1_step4:
  "{R12 ∩ UNIV × (m2_inv4_M2a ∩ m2_inv3_extrKey)} 
     (m1_step4 Ra A B Kab Ts), (m2_step4 Ra A B Kab Ts)  
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, simp_all)
   (auto dest: m2_inv34_M2a_authorized)

lemma PO_m2_step5_refines_m1_step5:
  "{R12 ∩ UNIV × (m2_inv4_M2b ∩ m2_inv3_extrKey)}          ― ‹REMOVED!: ‹m2_inv5_ikk_sv››
     (m1_step5 Rb A B Kab Ts), (m2_step5 Rb A B Kab Ts) 
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, simp_all)
   (auto dest: m2_inv34_M2b_authorized)

lemma PO_m2_tick_refines_m1_tick:
  "{R12}
    (m1_tick T), (m2_tick T)
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, simp_all)

lemma PO_m2_leak_refines_m1_leak:
  "{R12} 
     (m1_leak Rs), (m2_leak Rs)
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, auto)

lemma PO_m2_fake_refines_skip:
  "{R12} 
     Id, m2_fake
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, auto)


text ‹All together now...›

lemmas PO_m2_trans_refines_m1_trans = 
  PO_m2_step1_refines_m1_step1 PO_m2_step2_refines_m1_step2
  PO_m2_step3_refines_m1_step3 PO_m2_step4_refines_m1_step4
  PO_m2_step5_refines_m1_step5 PO_m2_tick_refines_m1_tick 
  PO_m2_leak_refines_m1_leak PO_m2_fake_refines_skip 

lemma PO_m2_refines_init_m1 [iff]:
  "init m2 ⊆ R12``(init m1)"
by (auto simp add: R12_def m1_defs m2_loc_defs)

lemma PO_m2_refines_trans_m1 [iff]:
  "{R12 ∩ 
    UNIV × (m2_inv4_M2b ∩ m2_inv4_M2a ∩ m2_inv3_extrKey)} 
     (trans m1), (trans m2) 
   {> R12}"
by (auto simp add: m2_def m2_trans_def m1_def m1_trans_def)
   (blast intro!: PO_m2_trans_refines_m1_trans)+


lemma PO_obs_consistent_R12 [iff]: 
  "obs_consistent R12 med21 m1 m2"
by (auto simp add: obs_consistent_def R12_def med21_def m2_defs)


text ‹Refinement result.›

lemma m2_refines_m1 [iff]:
  "refines 
     (R12 ∩ 
      (UNIV × (m2_inv4_M2b ∩ m2_inv4_M2a ∩ m2_inv3_extrKey ∩ m2_inv3a_sesK_compr)))
     med21 m1 m2"
by (rule Refinement_using_invariants) (auto)

lemma m2_implements_m1 [iff]:
  "implements med21 m1 m2"
by (rule refinement_soundness) (auto)


(******************************************************************************)
subsection ‹Inherited and derived invariants›
(******************************************************************************)
(*
text {* Show preservation of invariants @{term "m1_inv2i_serv"} and
@{term "m1_inv2r_serv"} from @{text "m1"}. *}

lemma PO_m2_sat_m1_inv2i_serv [iff]: "reach m2 ⊆ m1_inv2i_serv"
by (rule_tac Pa=m1_inv2i_serv and Qa=m1_inv2i_serv and Q=m1_inv2i_serv 
       in m2_implements_m1 [THEN [5] internal_invariant_translation])
   (auto simp add: m2_loc_defs med21_def intro!: m1_inv2i_servI)

lemma PO_m2_sat_m1_inv2r_serv [iff]: "reach m2 ⊆ m1_inv2r_serv"
by (rule_tac Pa=m1_inv2r_serv and Qa=m1_inv2r_serv and Q=m1_inv2r_serv
       in m2_implements_m1 [THEN [5] internal_invariant_translation])
   (fastforce simp add: m2_loc_defs med21_def intro!: m1_inv2r_servI)+


text {* Now we derive the L2 key secrecy invariants for the initiator 
and the responder (for definition, see above). *}

lemma PO_m2_inv6_init_ikk [iff]: "reach m2 ⊆ m2_inv6_ikk_init"
apply (rule_tac B=" m1_inv2i_serv ∩ m2_inv5_ikk_sv" in subset_trans, auto)
apply (rule m2_inv6_ikk_initI, auto)
apply (blast dest!: m1_inv2i_servD) 
done

lemma PO_m2_inv6_resp_ikk [iff]: "reach m2 ⊆ m2_inv7_ikk_resp"
apply (rule_tac B=" m1_inv2r_serv ∩ m2_inv5_ikk_sv" in subset_trans, auto)
apply (rule m2_inv7_ikk_respI, auto)
apply (blast dest!: m1_inv2r_servD) 
done
*)

end