Theory m1_keydist_inrn

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

  Project: Development of Security Protocols by Refinement

  Module:   Key_establish/m1_keydist_iirn.thy (Isabelle/HOL 2016-1)
  ID:       $Id: m1_keydist_inrn.thy 133854 2017-03-20 17:53:50Z csprenge $
  Author:   Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>

  Key distribution protocols
  Level 1, 1st refinement: Abstract server-based key transport protocol with 
  initiator and responder roles. Provides non-injective server authentication 
  to the initiator and responder.

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

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

section ‹Abstract (n/n)-authenticated key transport (L1)›

theory m1_keydist_inrn imports m1_keydist "../Refinement/a0i_agree"
begin

text ‹We add authentication for the initiator and responder to the basic
server-based key transport protocol: 
\begin{enumerate}
\item the initiator injectively agrees with the server on the key and some
additional data
\item the responder non-injectively agrees with the server on the key and 
some additional data.
\end{enumerate}
The "additional data" is a parameter of this model.›

declare option.split [split]
(* declare option.split_asm [split] *)


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

text ‹The state type remains the same, but in this model we will record
nonces and timestamps in the run frame.›

type_synonym m1a_state = "m1x_state"
type_synonym m1a_obs = "m1x_obs"

type_synonym 'x m1a_pred = "'x m1x_pred"
type_synonym 'x m1a_trans = "'x m1x_trans"


text ‹We need some parameters regarding the list of freshness values
stored by the server. These should be defined in further refinements.›

consts 
  is_len :: "nat"   ― ‹num of agreeing list elements for initiator-server›  
  rs_len :: "nat"   ― ‹num of agreeing list elements for responder-server›


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

definition         ― ‹by @{term "A"}, refines @{term "m1x_step1"}›
  m1a_step1 :: "[rid_t, agent, agent] ⇒ 'x m1r_trans"
where
  "m1a_step1 ≡ m1x_step1"

definition       ― ‹by @{term "B"}, refines @{term "m1x_step2"}›
  m1a_step2 :: "[rid_t, agent, agent] ⇒ 'x m1r_trans"
where
  "m1a_step2 ≡ m1x_step2"

definition       ― ‹by @{term "Server"}, refines @{term m1x_step3}›
  m1a_step3 :: "[rid_t, agent, agent, key, atom list] ⇒ 'x m1r_trans"
where
  "m1a_step3 Rs A B Kab al ≡ {(s, s1).
     ― ‹guards:›
     Rs ∉ dom (runs s) ∧                 ― ‹fresh run id›
     Kab = sesK (Rs$sk) ∧                 ― ‹generate session key›

     ― ‹actions:›
     s1 = s⦇ runs := (runs s)(Rs ↦ (Serv, [A, B], al)) ⦈
  }"

definition         ― ‹by @{text "A"}, refines @{term m1x_step4}›
  m1a_step4 :: "[rid_t, agent, agent, key, atom list] ⇒ 'x m1a_trans"
where
  "m1a_step4 Ra A B Kab nla ≡ {(s, s').
     ― ‹guards:›
     runs s Ra = Some (Init, [A, B], []) ∧
     (Kab ∉ leak s ⟶ (Kab, A) ∈ azC (runs s)) ∧      ― ‹authorization guard›

     ― ‹new guard for non-injective agreement with server on ‹(Kab, B, isl)›,›
     ― ‹where ‹isl = take is_len nla››
     (A ∉ bad ⟶ (∃Rs. Kab = sesK (Rs$sk) ∧
        runs s Rs = Some (Serv, [A, B], take is_len nla))) ∧

     ― ‹actions:›
     s' = s⦇ runs := (runs s)(Ra ↦ (Init, [A, B], aKey Kab # nla)) ⦈
  }" 

definition         ― ‹by @{term "B"}, refines @{term m1x_step5}›
  m1a_step5 :: "[rid_t, agent, agent, key, atom list] ⇒ 'x m1a_trans"
where
  "m1a_step5 Rb A B Kab nlb ≡ {(s, s1). 
     ― ‹guards:›
     runs s Rb = Some (Resp, [A, B], []) ∧ 
     (Kab ∉ leak s ⟶ (Kab, B) ∈ azC (runs s)) ∧         ― ‹authorization guard›

     ― ‹guard for non-injective agreement with server on ‹(Kab, A, rsl)››
     ― ‹where ‹rsl = take rs_len nlb››
     (B ∉ bad ⟶ (∃Rs. Kab = sesK (Rs$sk) ∧
        runs s Rs = Some (Serv, [A, B], take rs_len nlb))) ∧

     ― ‹actions:›
     s1 = s⦇ runs := (runs s)(Rb ↦ (Resp, [A, B], aKey Kab # nlb)) ⦈
  }"

definition     ― ‹by attacker, refines @{term m1x_leak}›
  m1a_leak :: "rid_t ⇒ 'x m1x_trans"
where
  "m1a_leak = m1x_leak" 


(******************************************************************************)
subsection ‹Specification›
(******************************************************************************)

definition
  m1a_init :: "m1a_state set"
where
  "m1a_init ≡ m1x_init" 

definition 
  m1a_trans :: "'x m1a_trans" where
  "m1a_trans ≡ (⋃A B Ra Rb Rs Kab nls nla nlb.
     m1a_step1 Ra A B ∪
     m1a_step2 Rb A B ∪
     m1a_step3 Rs A B Kab nls ∪
     m1a_step4 Ra A B Kab nla ∪
     m1a_step5 Rb A B Kab nlb ∪
     m1a_leak Rs ∪
     Id
  )"

definition 
  m1a :: "(m1a_state, m1a_obs) spec" where
  "m1a ≡ ⦇
     init = m1a_init,
     trans = m1a_trans,
     obs = id
  ⦈" 

lemma init_m1a: "init m1a = m1a_init"
by (simp add: m1a_def)

lemma trans_m1a: "trans m1a = m1a_trans"
by (simp add: m1a_def)

lemma obs_m1a [simp]: "obs m1a = id"
by (simp add: m1a_def)

lemmas m1a_loc_defs = 
  m1a_def m1a_init_def m1a_trans_def
  m1a_step1_def m1a_step2_def m1a_step3_def m1a_step4_def m1a_step5_def 
  m1a_leak_def

lemmas m1a_defs = m1a_loc_defs m1x_defs


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

subsubsection ‹inv0: Finite domain›
(*inv**************************************************************************)

text ‹There are only finitely many runs. This is needed to establish
the responder/initiator agreement.›

definition 
  m1a_inv0_fin :: "'x m1r_pred"
where
  "m1a_inv0_fin ≡ {s. finite (dom (runs s))}"

lemmas m1a_inv0_finI = m1a_inv0_fin_def [THEN setc_def_to_intro, rule_format]
lemmas m1a_inv0_finE [elim] = m1a_inv0_fin_def [THEN setc_def_to_elim, rule_format]
lemmas m1a_inv0_finD = m1a_inv0_fin_def [THEN setc_def_to_dest, rule_format]

text ‹Invariance proof.›

lemma PO_m1a_inv0_fin_init [iff]:
  "init m1a ⊆ m1a_inv0_fin"
by (auto simp add: m1a_defs intro!: m1a_inv0_finI)

lemma PO_m1a_inv0_fin_trans [iff]:
  "{m1a_inv0_fin} trans m1a {> m1a_inv0_fin}"
by (auto simp add: PO_hoare_defs m1a_defs intro!: m1a_inv0_finI)

lemma PO_m1a_inv0_fin [iff]: "reach m1a ⊆ m1a_inv0_fin"
by (rule inv_rule_incr, auto del: subsetI)


(******************************************************************************)
subsection ‹Refinement of ‹m1x››
(******************************************************************************)

subsubsection ‹Simulation relation›
(******************************************************************************)

text ‹Define run abstraction.›

fun 
  rm1x1a :: "role_t ⇒ atom list ⇒ atom list"
where
  "rm1x1a Init = take 1"         ― ‹take ‹Kab› from ‹Kab # nla››
| "rm1x1a Resp = take 1"         ― ‹take ‹Kab› from ‹Kab # nlb››
| "rm1x1a Serv = take 0"         ― ‹drop all from ‹nls››

abbreviation
  runs1x1a :: "runs_t ⇒ runs_t" where 
  "runs1x1a ≡ map_runs rm1x1a"

text ‹med1x1: The mediator function maps a concrete observation to an 
abstract one.›

definition
  med1x1a :: "m1a_obs ⇒ m1x_obs" where
  "med1x1a t ≡ ⦇ runs = runs1x1a (runs t), leak = leak t ⦈"

text ‹R1x1a: The simulation relation is defined in terms of the mediator
function.›

definition
  R1x1a :: "(m1x_state × m1a_state) set" where
  "R1x1a ≡ {(s, t). s = med1x1a t}"

lemmas R1x1a_defs = 
  R1x1a_def med1x1a_def 


subsubsection ‹Refinement proof›
(******************************************************************************)

lemma PO_m1a_step1_refines_m1x_step1:
  "{R1x1a} 
     (m1x_step1 Ra A B), (m1a_step1 Ra A B) 
   {> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs)

lemma PO_m1a_step2_refines_m1x_step2:
  "{R1x1a} 
     (m1x_step2 Rb A B), (m1a_step2 Rb A B) 
   {> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs)

lemma PO_m1a_step3_refines_m1x_step3:
  "{R1x1a} 
     (m1x_step3 Rs A B Kab), (m1a_step3 Rs A B Kab nls)
   {> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs)

lemma PO_m1a_step4_refines_m1x_step4:
  "{R1x1a} 
     (m1x_step4 Ra A B Kab), (m1a_step4 Ra A B Kab nla) 
   {> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs map_runs_def)

lemma PO_m1a_step5_refines_m1x_step5:
  "{R1x1a} 
     (m1x_step5 Rb A B Kab), (m1a_step5 Rb A B Kab nlb) 
   {> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs map_runs_def)

lemma PO_m1a_leak_refines_m1x_leak:
  "{R1x1a} 
     (m1x_leak Rs), (m1a_leak Rs) 
   {> R1x1a}"
by (auto simp add: PO_rhoare_defs R1x1a_defs m1a_defs map_runs_def)


text ‹All together now...›

lemmas PO_m1a_trans_refines_m1x_trans = 
  PO_m1a_step1_refines_m1x_step1 PO_m1a_step2_refines_m1x_step2
  PO_m1a_step3_refines_m1x_step3 PO_m1a_step4_refines_m1x_step4
  PO_m1a_step5_refines_m1x_step5 PO_m1a_leak_refines_m1x_leak


lemma PO_m1a_refines_init_m1x [iff]:
  "init m1a ⊆  R1x1a``(init m1x)"
by (auto simp add: R1x1a_defs m1a_defs)

lemma PO_m1a_refines_trans_m1x [iff]:
  "{R1x1a} 
     (trans m1x), (trans m1a) 
   {> R1x1a}"
apply (auto simp add: m1a_def m1a_trans_def m1x_def m1x_trans_def
         intro!: PO_m1a_trans_refines_m1x_trans)
apply (force intro!: PO_m1a_trans_refines_m1x_trans)+
done

text ‹Observation consistency.›

lemma obs_consistent_med1x1a [iff]: 
  "obs_consistent R1x1a med1x1a m1x m1a"
by (auto simp add: obs_consistent_def R1x1a_def m1a_defs)


text ‹Refinement result.›

lemma PO_m1a_refines_m1x [iff]: 
  "refines R1x1a med1x1a m1x m1a"
by (rule Refinement_basic) (auto del: subsetI)

lemma  m1a_implements_m1x [iff]: "implements med1x1a m1x m1a"
by (rule refinement_soundness) (fast)


(******************************************************************************)
subsection ‹Refinement of ‹a0n› for initiator/server›
(******************************************************************************)

text ‹For the initiator, we get an non-injective agreement with the server on 
the session key, the responder name, and the atom list @{term "isl"}.›


subsubsection ‹Simulation relation›
(******************************************************************************)

text ‹We define two auxiliary functions to reconstruct the signals of the
initial model from completed initiator and server runs.›

type_synonym
  issig = "key × agent × atom list"

abbreviation
  is_commit :: "[runs_t, agent, agent, key, atom list] ⇒ rid_t set" 
where
  "is_commit runz A B Kab sl ≡ {Ra. ∃nla. 
     runz Ra = Some (Init, [A, B], aKey Kab # nla) ∧ take is_len nla = sl
  }"

fun
  is_runs2sigs :: "runs_t ⇒ issig signal ⇒ nat"
where
  "is_runs2sigs runz (Running [A, Sv] (Kab, B, sl)) = 
     (if ∃Rs nls. Kab = sesK (Rs$sk) ∧ 
         runz Rs = Some (Serv, [A, B], nls) ∧ take is_len nls = sl
      then 1 else 0)"

| "is_runs2sigs runz (Commit [A, Sv] (Kab, B, sl)) = 
     card (is_commit runz A B Kab sl)"

| "is_runs2sigs runz _ = 0"


text ‹Simulation relation and mediator function. We map completed initiator 
and responder runs to commit and running signals, respectively.›

definition 
  med_a0m1a_is :: "m1a_obs ⇒ issig a0i_obs" where
  "med_a0m1a_is o1 ≡ ⦇ signals = is_runs2sigs (runs o1), corrupted = {} ⦈"

definition
  R_a0m1a_is :: "(issig a0i_state × m1a_state) set" where
  "R_a0m1a_is ≡ {(s, t). signals s = is_runs2sigs (runs t) ∧ corrupted s = {} }"

lemmas R_a0m1a_is_defs = R_a0m1a_is_def med_a0m1a_is_def 


subsubsection ‹Lemmas about the auxiliary functions›
(******************************************************************************)

lemma is_runs2sigs_empty [simp]: 
  "runz = Map.empty ⟹ is_runs2sigs runz = (λs. 0)"
by (rule ext, erule rev_mp) 
   (rule is_runs2sigs.induct, auto)

lemma is_commit_finite [simp, intro]:
  "finite (dom runz) ⟹ finite (is_commit runz A B Kab nls)"
by (auto intro: finite_subset dest: dom_lemmas)


text ‹Update lemmas›

lemma is_runs2sigs_upd_init_none [simp]:
  "⟦ Ra ∉ dom runz ⟧
  ⟹ is_runs2sigs (runz(Ra ↦ (Init, [A, B], []))) = is_runs2sigs runz"
by (rule ext, erule rev_mp) 
   (rule is_runs2sigs.induct, auto dest: dom_lemmas)

lemma is_runs2sigs_upd_resp_none [simp]:
  "⟦ Rb ∉ dom runz ⟧
  ⟹ is_runs2sigs (runz(Rb ↦ (Resp, [A, B], []))) = is_runs2sigs runz"
by (rule ext, erule rev_mp) 
   (rule is_runs2sigs.induct, auto dest: dom_lemmas)

lemma is_runs2sigs_upd_serv [simp]:
  "⟦ Rs ∉ dom runz ⟧
  ⟹ is_runs2sigs (runz(Rs ↦ (Serv, [A, B], nls))) = 
     (is_runs2sigs runz)(Running [A, Sv] (sesK (Rs$sk), B, take is_len nls) := 1)"
by (rule ext, erule rev_mp) 
   (rule is_runs2sigs.induct, auto dest: dom_lemmas)

lemma is_runs2sigs_upd_init_some [simp]:
  "⟦ runz Ra = Some (Init, [A, B], []); finite (dom runz); 
     ils = take is_len nla ⟧
  ⟹ is_runs2sigs (runz(Ra ↦ (Init, [A, B], aKey Kab # nla))) =
     (is_runs2sigs runz)(
        Commit [A, Sv] (Kab, B, ils) := 
          Suc (card (is_commit runz A B Kab ils)))"
apply (rule ext, erule rev_mp, erule rev_mp, erule rev_mp)
apply (rename_tac s)
apply (rule_tac ?a0.0=runz and ?a1.0=s in is_runs2sigs.induct, auto)
― ‹1 subgoal›
apply (rename_tac runz)
apply (rule_tac s="card (insert Ra (is_commit runz A B Kab (take is_len nla)))" 
      in trans, fast, auto)
done

lemma is_runs2sigs_upd_resp_some [simp]:
  "⟦ runz Rb = Some (Resp, [A, B], []) ⟧
  ⟹ is_runs2sigs (runz(Rb ↦ (Resp, [A, B], aKey Kab # nlb))) =
     is_runs2sigs runz" 
by (rule ext, erule rev_mp)
   (rule is_runs2sigs.induct, auto dest: dom_lemmas)  


subsubsection ‹Refinement proof›
(******************************************************************************)

lemma PO_m1a_step1_refines_a0_is_skip:
  "{R_a0m1a_is} 
     Id, (m1a_step1 Ra A B) 
   {> R_a0m1a_is}"
by (auto simp add: PO_rhoare_defs R_a0m1a_is_defs m1a_defs)

lemma PO_m1a_step2_refines_a0_is_skip:
  "{R_a0m1a_is} 
     Id, (m1a_step2 Rb A B) 
   {> R_a0m1a_is}"
by (auto simp add: PO_rhoare_defs R_a0m1a_is_defs m1a_defs)

lemma PO_m1a_step3_refines_a0_is_running:
  "{R_a0m1a_is} 
     (a0n_running [A, Sv] (Kab, B, take is_len nls)), 
     (m1a_step3 Rs A B Kab nls) 
   {> R_a0m1a_is}"
by (auto simp add: PO_rhoare_defs R_a0m1a_is_defs a0i_defs m1a_defs
         dest: dom_lemmas)

lemma PO_m1a_step4_refines_a0_is_commit:
  "{R_a0m1a_is ∩ UNIV × m1a_inv0_fin} 
     (a0n_commit [A, Sv] (Kab, B, take is_len nla)), 
     (m1a_step4 Ra A B Kab nla) 
   {> R_a0m1a_is}"
by (simp add: PO_rhoare_defs R_a0m1a_is_defs a0i_defs m1a_defs, safe, auto)

lemma PO_m1a_step5_refines_a0_is_skip:
  "{R_a0m1a_is} 
     Id, (m1a_step5 Rb A B Kab nlb) 
   {> R_a0m1a_is}"
by (simp add: PO_rhoare_defs R_a0m1a_is_defs m1a_defs, safe, auto)

lemma PO_m1a_leak_refines_a0_is_skip:
  "{R_a0m1a_is} 
     Id, (m1a_leak Rs) 
   {> R_a0m1a_is}"
by (simp add: PO_rhoare_defs R_a0m1a_is_defs m1a_defs, safe, auto)


text ‹All together now...›

lemmas PO_m1a_trans_refines_a0_is_trans = 
  PO_m1a_step1_refines_a0_is_skip PO_m1a_step2_refines_a0_is_skip
  PO_m1a_step3_refines_a0_is_running PO_m1a_step4_refines_a0_is_commit
  PO_m1a_step5_refines_a0_is_skip PO_m1a_leak_refines_a0_is_skip
  

lemma PO_m1a_refines_init_a0_is [iff]:
  "init m1a ⊆  R_a0m1a_is``(init a0n)"
by (auto simp add: R_a0m1a_is_defs a0n_defs m1a_defs)

lemma PO_m1a_refines_trans_a0_is [iff]:
  "{R_a0m1a_is ∩ UNIV × m1a_inv0_fin} 
     (trans a0n), (trans m1a) 
   {> R_a0m1a_is}"
by (auto simp add: m1a_def m1a_trans_def a0n_def a0n_trans_def
         intro!: PO_m1a_trans_refines_a0_is_trans)

lemma obs_consistent_med_a0m1a_is [iff]: 
  "obs_consistent R_a0m1a_is med_a0m1a_is a0n m1a"
by (auto simp add: obs_consistent_def R_a0m1a_is_def med_a0m1a_is_def 
                   a0n_def m1a_def)

text ‹Refinement result.›

lemma PO_m1a_refines_a0_is [iff]: 
  "refines (R_a0m1a_is ∩ UNIV × m1a_inv0_fin) med_a0m1a_is a0n m1a"
by (rule Refinement_using_invariants) (auto del: subsetI)

lemma  m1a_implements_a0_is: "implements med_a0m1a_is a0n m1a"
by (rule refinement_soundness) (fast)


(******************************************************************************)
subsection ‹Refinement of ‹a0n› for responder/server›
(******************************************************************************)

text ‹For the responder, we get a non-injective agreement with the server on 
the session key, the initiator's name, and additional data.›


subsubsection ‹Simulation relation›
(******************************************************************************)

text ‹We define two auxiliary functions to reconstruct the signals of the
initial model from completed responder and server runs.›

type_synonym
  rssig = "key × agent × atom list"

abbreviation
  rs_commit :: "[runs_t, agent, agent, key, atom list] ⇒ rid_t set" 
where
  "rs_commit runz A B Kab rsl ≡ {Rb. ∃nlb. 
     runz Rb = Some (Resp, [A, B], aKey Kab # nlb) ∧ take rs_len nlb = rsl 
  }"

fun
  rs_runs2sigs :: "runs_t ⇒ rssig signal ⇒ nat"
where
  "rs_runs2sigs runz (Running [B, Sv] (Kab, A, rsl)) = 
     (if ∃Rs nls. Kab = sesK (Rs$sk) ∧
         runz Rs = Some (Serv, [A, B], nls) ∧ take rs_len nls = rsl
      then 1 else 0)"

| "rs_runs2sigs runz (Commit [B, Sv] (Kab, A, rsl)) = 
     card (rs_commit runz A B Kab rsl)"

| "rs_runs2sigs runz _ = 0"


text ‹Simulation relation and mediator function. We map completed initiator 
and responder runs to commit and running signals, respectively.›

definition 
  med_a0m1a_rs :: "m1a_obs ⇒ rssig a0n_obs" where
  "med_a0m1a_rs o1 ≡ ⦇ signals = rs_runs2sigs (runs o1), corrupted = {} ⦈"

definition
  R_a0m1a_rs :: "(rssig a0n_state × m1a_state) set" where
  "R_a0m1a_rs ≡ {(s, t). signals s = rs_runs2sigs (runs t) ∧ corrupted s = {} }"

lemmas R_a0m1a_rs_defs = R_a0m1a_rs_def med_a0m1a_rs_def 


subsubsection ‹Lemmas about the auxiliary functions›
(******************************************************************************)

text ‹Other lemmas›

lemma rs_runs2sigs_empty [simp]: 
  "runz = Map.empty ⟹ rs_runs2sigs runz = (λs. 0)"
by (rule ext, erule rev_mp) 
   (rule rs_runs2sigs.induct, auto)

lemma rs_commit_finite [simp, intro]:
  "finite (dom runz) ⟹ finite (rs_commit runz A B Kab nls)"
by (auto intro: finite_subset dest: dom_lemmas)


text ‹Update lemmas›

lemma rs_runs2sigs_upd_init_none [simp]:
  "⟦ Ra ∉ dom runz ⟧
  ⟹ rs_runs2sigs (runz(Ra ↦ (Init, [A, B], []))) = rs_runs2sigs runz"
by (rule ext, erule rev_mp) 
   (rule rs_runs2sigs.induct, auto dest: dom_lemmas)

lemma rs_runs2sigs_upd_resp_none [simp]:
  "⟦ Rb ∉ dom runz ⟧
  ⟹ rs_runs2sigs (runz(Rb ↦ (Resp, [A, B], []))) = rs_runs2sigs runz"
by (rule ext, erule rev_mp) 
   (rule rs_runs2sigs.induct, auto dest: dom_lemmas)

lemma rs_runs2sigs_upd_serv [simp]:
  "⟦ Rs ∉ dom runz ⟧
  ⟹ rs_runs2sigs (runz(Rs ↦ (Serv, [A, B], nls))) = 
     (rs_runs2sigs runz)(Running [B, Sv] (sesK (Rs$sk), A, take rs_len nls) := 1)"
by (rule ext, erule rev_mp) 
   (rule rs_runs2sigs.induct, auto dest: dom_lemmas)

lemma rs_runs2sigs_upd_init_some [simp]:
  "⟦ runz Ra = Some (Init, [A, B], []) ⟧
  ⟹ rs_runs2sigs (runz(Ra ↦ (Init, [A, B], aKey Kab # nl))) =
     rs_runs2sigs runz" 
by (rule ext, erule rev_mp)
   (rule rs_runs2sigs.induct, auto dest: dom_lemmas)  

lemma rs_runs2sigs_upd_resp_some [simp]:
  "⟦ runz Rb = Some (Resp, [A, B], []); finite (dom runz);
     rsl = take rs_len nlb ⟧
 ⟹ rs_runs2sigs (runz(Rb ↦ (Resp, [A, B], aKey Kab # nlb))) =
   (rs_runs2sigs runz)(
      Commit [B, Sv] (Kab, A, rsl) := Suc (card (rs_commit runz A B Kab rsl)))"
apply (rule ext, erule rev_mp, erule rev_mp, erule rev_mp) 
apply (rule rs_runs2sigs.induct, auto dest: dom_lemmas)
― ‹1 subgoal›
apply (rename_tac runz)
apply (rule_tac s="card (insert Rb (rs_commit runz A B Kab (take rs_len nlb)))" 
       in trans, fast, auto)
done


subsubsection ‹Refinement proof›
(******************************************************************************)

lemma PO_m1a_step1_refines_a0_rs_skip:
  "{R_a0m1a_rs} 
     Id, (m1a_step1 Ra A B) 
   {> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs m1a_defs)

lemma PO_m1a_step2_refines_a0_rs_skip:
  "{R_a0m1a_rs} 
     Id, (m1a_step2 Rb A B) 
   {> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs m1a_defs)

lemma PO_m1a_step3_refines_a0_rs_running:
  "{R_a0m1a_rs} 
     (a0n_running [B, Sv] (Kab, A, take rs_len nls)), 
     (m1a_step3 Rs A B Kab nls) 
   {> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs a0n_defs m1a_defs
         dest: dom_lemmas)

lemma PO_m1a_step4_refines_a0_rs_skip:
  "{R_a0m1a_rs} 
     Id, (m1a_step4 Ra A B Kab nla) 
   {> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs m1a_defs)

lemma PO_m1a_step5_refines_a0_rs_commit:
  "{R_a0m1a_rs ∩ UNIV × m1a_inv0_fin} 
     (a0n_commit [B, Sv] (Kab, A, take rs_len nlb)), 
     (m1a_step5 Rb A B Kab nlb) 
   {> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs a0n_defs m1a_defs)

lemma PO_m1a_leak_refines_a0_rs_skip:
  "{R_a0m1a_rs} 
     Id, (m1a_leak Rs) 
   {> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs a0i_defs m1a_defs)


text ‹All together now...›

lemmas PO_m1a_trans_refines_a0_rs_trans = 
  PO_m1a_step1_refines_a0_rs_skip PO_m1a_step2_refines_a0_rs_skip
  PO_m1a_step3_refines_a0_rs_running PO_m1a_step4_refines_a0_rs_skip
  PO_m1a_step5_refines_a0_rs_commit PO_m1a_leak_refines_a0_rs_skip


lemma PO_m1a_refines_init_ra0n [iff]:
  "init m1a ⊆  R_a0m1a_rs``(init a0n)"
by (auto simp add: R_a0m1a_rs_defs a0n_defs m1a_defs)

lemma PO_m1a_refines_trans_ra0n [iff]:
  "{R_a0m1a_rs ∩ UNIV × m1a_inv0_fin} 
     (trans a0n), (trans m1a) 
   {> R_a0m1a_rs}"
by (auto simp add: m1a_def m1a_trans_def a0n_def a0n_trans_def
         intro!: PO_m1a_trans_refines_a0_rs_trans)

lemma obs_consistent_med_a0m1a_rs [iff]: 
  "obs_consistent (R_a0m1a_rs ∩ UNIV × m1a_inv0_fin) med_a0m1a_rs a0n m1a"
by (auto simp add: obs_consistent_def R_a0m1a_rs_def med_a0m1a_rs_def 
                   a0n_def m1a_def)


text ‹Refinement result.›

lemma PO_m1a_refines_a0_rs [iff]: 
  "refines (R_a0m1a_rs ∩ UNIV × m1a_inv0_fin) med_a0m1a_rs a0n m1a"
by (rule Refinement_using_invariants) (auto)

lemma  m1a_implements_ra0n: "implements med_a0m1a_rs a0n m1a"
by (rule refinement_soundness) (fast)


end