Theory m1_keydist_iirn

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

  Project: Development of Security Protocols by Refinement

  Module:   Key_establish/m1_keydist_iirn.thy (Isabelle/HOL 2016-1)
  ID:       $Id: m1_keydist_iirn.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 injective server authentication to 
  the initiator and non-injective server authenticaiton to the responder.

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

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

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

theory m1_keydist_iirn 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] *)

consts
  na :: "nat"

(******************************************************************************)
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, nonce]  'x m1r_trans"
where
  "m1a_step1 Ra A B Na  {(s, s1).
    ― ‹guards:›
    Ra  dom (runs s)                 ― ‹Ra› is fresh›
    Na = Ra$na                        ― ‹NEW: generate a nonce›

    ― ‹actions:›
    ― ‹create initiator thread›
    s1 = s runs := (runs s)(Ra  (Init, [A, B], [])) 
  }"

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, nonce, atom list]  'x m1r_trans"
where
  "m1a_step3 Rs A B Kab Na 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], aNon Na # al)) 
  }"

definition         ― ‹by @{text "A"}, refines @{term m1x_step4}
  m1a_step4 :: "[rid_t, agent, agent, nonce, key, atom list]  'x m1a_trans"
where
  "m1a_step4 Ra A B Na Kab nla  {(s, s').
     ― ‹guards:›
     runs s Ra = Some (Init, [A, B], []) 
     (Kab  leak s  (Kab, A)  azC (runs s))   ― ‹authorization guard›
     Na = Ra$na                                    ― ‹fix parameter›

     ― ‹new guard for agreement with server on (Kab, B, Na, isl)›,›
     ― ‹where isl = take is_len nla›; injectiveness by including Na›
     (A  bad  (Rs. Kab = sesK (Rs$sk) 
        runs s Rs = Some (Serv, [A, B], aNon Na # 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 showing agreement with server on (Kab, A, rsl)›,›
     ― ‹where rsl = take rs_len nlb›; this agreement is non-injective›

     (B  bad  (Rs Na. Kab = sesK (Rs$sk) 
        runs s Rs = Some (Serv, [A, B], aNon Na # 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 Na Kab nls nla nlb.
     m1a_step1 Ra A B Na 
     m1a_step2 Rb A B 
     m1a_step3 Rs A B Kab Na nls 
     m1a_step4 Ra A B Na 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 [Na]›

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 Na) 
   {> 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 Na 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 Na 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 A B Rb Kab), (m1a_step5 A B Rb 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)

text ‹By transitivity:›

lemma m1a_implements_s0g [iff]: "implements (med01x o med1x1a) s0g m1a"
by (rule implements_trans, auto)


subsubsection ‹inv (inherited): Secrecy›
(*invh*************************************************************************)

text ‹Secrecy preserved from m1x›.›

lemma knC_runs1x1a [simp]: "knC (runs1x1a runz) = knC runz"
apply (auto simp add: map_runs_def elim!: knC.cases, auto)
― ‹5 subgoals›
apply (rename_tac b, case_tac b, auto)
apply (rename_tac b, case_tac b, auto)
apply (rule knC_init, auto simp add: map_runs_def)
apply (rule knC_resp, auto simp add: map_runs_def)
apply (rule knC_serv, auto simp add: map_runs_def)
done

lemma PO_m1a_obs_secrecy [iff]: "oreach m1a  m1x_secrecy"
apply (rule_tac Q=m1x_secrecy in external_invariant_translation)
apply (auto del: subsetI)
apply (auto simp add: med1x1a_def m1x_secrecy_def)
done

lemma PO_m1a_secrecy [iff]: "reach m1a  m1x_secrecy"
by (rule external_to_internal_invariant) (auto del: subsetI)


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

text ‹For the initiator, we get an injective agreement with the server on 
the session key, the responder name, the initiator's nonce and the list of 
freshness values @{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 × nonce × atom list"

fun
  is_runs2sigs :: "runs_t  issig signal  nat"
where
  "is_runs2sigs runz (Running [A, Sv] (Kab, B, Na, nl)) = 
     (if Rs. Kab = sesK (Rs$sk)  
         runz Rs = Some (Serv, [A, B], aNon Na # nl) 
      then 1 else 0)"

| "is_runs2sigs runz (Commit [A, Sv] (Kab, B, Na, nl)) = 
     (if Ra nla. Na = Ra$na  
         runz Ra = Some (Init, [A, B], aKey Kab # nla)  
         take is_len nla = nl
      then 1 else 0)"

| "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)


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], aNon Na # ils))) = 
     (is_runs2sigs runz)(Running [A, Sv] (sesK (Rs$sk), B, Na, ils) := 1)"
apply (rule ext, (erule rev_mp)+) 
apply (rule is_runs2sigs.induct)
apply (safe, simp_all)+
apply (fastforce simp add: domIff)+
done

lemma is_runs2sigs_upd_init_some [simp]:
  " runz Ra = Some (Init, [A, B], []); ils = take is_len nla 
   is_runs2sigs (runz(Ra  (Init, [A, B], aKey Kab # nla))) =
     (is_runs2sigs runz)(Commit [A, Sv] (Kab, B, Ra$na, ils) := 1)"
apply (rule ext, (erule rev_mp)+)
apply (rule is_runs2sigs.induct)
apply (safe, simp_all)+ 
apply (fastforce)+
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" 
apply (rule ext, erule rev_mp)
apply (rule is_runs2sigs.induct, auto)  
done


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

lemma PO_m1a_step1_refines_a0_is_skip:
  "{R_a0m1a_is} 
     Id, (m1a_step1 Ra A B Na) 
   {> 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} 
     (a0i_running [A, Sv] (Kab, B, Na, nls)), 
     (m1a_step3 Rs A B Kab Na 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} 
     (a0i_commit [A, Sv] (Kab, B, Na, take is_len nla)), 
     (m1a_step4 Ra A B Na Kab nla) 
   {> R_a0m1a_is}"
by (auto simp add: PO_rhoare_defs R_a0m1a_is_defs a0i_defs m1a_defs)

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

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

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 a0i)"
by (auto simp add: R_a0m1a_is_defs a0i_defs m1a_defs)

lemma PO_m1a_refines_trans_a0_is [iff]:
  "{R_a0m1a_is  a0i_inv1_iagree × m1a_inv0_fin} 
     (trans a0i), (trans m1a) 
   {> R_a0m1a_is}"
by (force simp add: m1a_def m1a_trans_def a0i_def a0i_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 a0i m1a"
by (auto simp add: obs_consistent_def R_a0m1a_is_def med_a0m1a_is_def 
                   a0i_def m1a_def)

text ‹Refinement result.›

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

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


subsubsection ‹inv2i (inherited): Initiator and server›
(*invh*************************************************************************)

text ‹This is a translation of the agreement property to Level 1. It
follows from the refinement and is needed to prove inv1.›

definition 
  m1a_inv2i_serv :: "'x m1x_state_scheme set"
where
  "m1a_inv2i_serv  {s. A B Ra Kab nla.
     A  bad 
     runs s Ra = Some (Init, [A, B], aKey Kab # nla) 
       (Rs. Kab = sesK (Rs$sk)  
         runs s Rs = Some (Serv, [A, B], aNon (Ra$na) # take is_len nla))
  }"

lemmas m1a_inv2i_servI = 
  m1a_inv2i_serv_def [THEN setc_def_to_intro, rule_format]
lemmas m1a_inv2i_servE =     (* DO NOT declare elim: leads to slow proofs! *)
  m1a_inv2i_serv_def [THEN setc_def_to_elim, rule_format]
lemmas m1a_inv2i_servD =     (* DO NOT declare dest: leads to slow proofs! *)
  m1a_inv2i_serv_def [THEN setc_def_to_dest, rule_format, rotated -1]


text ‹Invariance proof, see below after init/serv authentication proof.›

lemma PO_m1a_inv2i_serv [iff]:
  "reach m1a  m1a_inv2i_serv"
apply (rule INV_from_Refinement_basic [OF PO_m1a_refines_a0_is])
apply (auto simp add: R_a0m1a_is_def a0i_inv1_iagree_def 
            intro!: m1a_inv2i_servI)
apply (drule_tac x="[A, Sv]" in spec, force)
done


subsubsection ‹inv1: Key freshness for initiator›
(*inv**************************************************************************)

text ‹The initiator obtains key freshness from the injective agreement
with the server AND the fact that there is only one server run with a 
given key.›

definition 
  m1a_inv1_ifresh :: "'x m1a_pred"
where
  "m1a_inv1_ifresh  {s. A A' B B' Ra Ra' Kab nl nl'.
     runs s Ra  = Some (Init, [A,  B],  aKey Kab # nl) 
     runs s Ra' = Some (Init, [A', B'], aKey Kab # nl') 
     A  bad  B  bad  Kab  leak s 
       Ra = Ra'
  }"

lemmas m1a_inv1_ifreshI = m1a_inv1_ifresh_def [THEN setc_def_to_intro, rule_format]
lemmas m1a_inv1_ifreshE [elim] = m1a_inv1_ifresh_def [THEN setc_def_to_elim, rule_format]
lemmas m1a_inv1_ifreshD = m1a_inv1_ifresh_def [THEN setc_def_to_dest, rule_format, rotated 1]


text ‹Invariance proof›

lemma PO_m1a_inv1_ifresh_init [iff]:
  "init m1a  m1a_inv1_ifresh"
by (auto simp add: m1a_defs intro!: m1a_inv1_ifreshI)


lemma PO_m1a_inv1_ifresh_step4:
  "{m1a_inv1_ifresh  m1a_inv2i_serv  m1x_secrecy} 
      m1a_step4 Ra A B Na Kab nla
   {> m1a_inv1_ifresh}"
proof (auto simp add: PO_hoare_defs m1a_defs intro!: m1a_inv1_ifreshI,  (* UGLY *)
       auto dest: m1a_inv1_ifreshD, auto dest: m1a_inv2i_servD)
  fix Rs Ra' A' B' nl' s 
  assume H: 
    "(sesK (Rs $ sk), A)  azC (runs s)" "sesK (Rs $ sk)  leak s" 
    "A  bad" "B  bad" "Ra'  Ra"
    "runs s Ra = Some (Init, [A, B], [])" 
    "runs s Rs = Some (Serv, [A, B], aNon (Ra $ na) # take is_len nla)" 
    "runs s Ra' = Some (Init, [A', B'], aKey (sesK (Rs $ sk)) # nl')"
    "s  m1x_secrecy" "s  m1a_inv2i_serv" 
  thus False
  proof (cases "A'  bad")
    case True 
    from H have "(sesK (Rs$sk), A')  azC (runs s)" by (elim m1x_secrecyE, auto) 
    with H True show ?thesis by (elim azC.cases) (auto dest: m1a_inv2i_servD) 
  next 
    case False thus ?thesis using H by (auto dest: m1a_inv2i_servD)
  qed
next
  fix A' B' Ra' nl s
  assume 
    "(Kab, A)  azC (runs s)" "Kab  leak s" 
    "A'  bad"  "B'  bad" "A  bad" "Ra'  Ra"
    "runs s Ra' = Some (Init, [A', B'], aKey Kab # nl)"
    "runs s Ra = Some (Init, [A, B], [])"
    "s  m1a_inv2i_serv" 
  thus False 
  by (elim azC.cases, auto dest: m1a_inv2i_servD)
qed 

lemma PO_m1a_inv1_ifresh_trans [iff]:
  "{m1a_inv1_ifresh  m1a_inv2i_serv  m1x_secrecy} trans m1a {> m1a_inv1_ifresh}"
proof (simp add: m1a_def m1a_trans_def, safe)
  fix Ra A B Kab Ts nla
  show
    "{m1a_inv1_ifresh  m1a_inv2i_serv  m1x_secrecy} 
        m1a_step4 Ra A B Kab Ts nla
     {> m1a_inv1_ifresh}"
  by (rule PO_m1a_inv1_ifresh_step4)
qed (auto simp add: PO_hoare_defs m1a_defs intro!: m1a_inv1_ifreshI)

lemma PO_m1a_inv1_ifresh [iff]: "reach m1a  m1a_inv1_ifresh"
by (rule_tac J=" m1a_inv2i_serv  m1x_secrecy" in inv_rule_incr) 
   (auto simp add: Int_assoc del: subsetI)


(******************************************************************************)
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 Na. Kab = sesK (Rs$sk)  
           runz Rs = Some (Serv, [A, B], aNon Na # 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], aNon Na # nls))) = 
     (rs_runs2sigs runz)(Running [B, Sv] (sesK (Rs$sk), A, 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)+) 
apply (rule rs_runs2sigs.induct, auto dest: dom_lemmas)
― ‹1 subgoal›
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 Na) 
   {> 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, nls)), 
     (m1a_step3 Rs A B Kab Na nls) 
   {> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs a0i_defs m1a_defs
         dest: dom_lemmas)

lemma PO_m1a_step4_refines_a0_rs_skip:
  "{R_a0m1a_rs} 
     Id, (m1a_step4 Ra A B Na Kab nla) 
   {> R_a0m1a_rs}"
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs a0i_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 a0i_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  a0n_inv1_niagree × m1a_inv0_fin} 
     (trans a0n), (trans m1a) 
   {> R_a0m1a_rs}"
by (force 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  a0n_inv1_niagree × 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  a0n_inv1_niagree × 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)


subsubsection ‹inv2r (inherited): Responder and server›
(*invh*************************************************************************)

text ‹This is a translation of the agreement property to Level 1. It
follows from the refinement and not needed here but later.›

definition 
  m1a_inv2r_serv :: "'x m1x_state_scheme set"
where
  "m1a_inv2r_serv  {s. A B Rb Kab nlb.
     B  bad  
     runs s Rb = Some (Resp, [A, B], aKey Kab # nlb) 
       (Rs Na. Kab = sesK (Rs$sk) 
        runs s Rs = Some (Serv, [A, B], aNon Na # take rs_len nlb))
  }"

lemmas m1a_inv2r_servI = 
  m1a_inv2r_serv_def [THEN setc_def_to_intro, rule_format]
lemmas m1a_inv2r_servE [elim] = 
  m1a_inv2r_serv_def [THEN setc_def_to_elim, rule_format]
lemmas m1a_inv2r_servD = 
  m1a_inv2r_serv_def [THEN setc_def_to_dest, rule_format, rotated -1]


text ‹Invariance proof›

lemma PO_m1a_inv2r_serv [iff]:
  "reach m1a  m1a_inv2r_serv"
apply (rule INV_from_Refinement_basic [OF PO_m1a_refines_a0_rs])
apply (auto simp add: R_a0m1a_rs_def a0n_inv1_niagree_def intro!: m1a_inv2r_servI)
apply (rename_tac x A B Rb Kab nlb a, drule_tac x="[B, Sv]" in spec, clarsimp)
apply (rename_tac x A B Rb Kab nlb a, drule_tac x="Kab" in spec, force)
done


end