Theory m1_kerberos

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

  Project: Development of Security Protocols by Refinement

  Module:   Key_establish/m1_kerberos.thy (Isabelle/HOL 2016)
  ID:       $Id: m1_kerberos.thy 133856 2017-03-20 18:05:54Z csprenge $
  Author:   Ivano Somaini, ETH Zurich <somainii@student.ethz.ch>
            Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>

  Key distribution protocols
  Abstract version of Kerberos protocol with server-authentication and
  mutual initiator and responder authentication.

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

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

section ‹Abstract Kerberos core protocol (L1)›

theory m1_kerberos imports m1_keydist_iirn
begin

text ‹We augment the basic abstract key distribution model such that 
the server sends a timestamp along with the session key. We use a cache to 
guard against replay attacks and timestamp validity checks to ensure recentness
of the session key. 

We establish three refinements for this model, namely that this model refines
\begin{enumerate}
\item the authenticated key distribution model ‹m1_keydist_iirn›, 

\item the injective agreement model ‹a0i›, instantiated such that 
the responder agrees with the initiator on the session key, its timestamp
and the initiator's authenticator timestamp.

\item the injective agreement model ‹a0i›, instantiated such that 
the initiator agrees with the responder on the session key, its timestamp
and the initiator's authenticator timestamp.
\end{enumerate}
›

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

text ‹We extend the basic key distribution by adding timestamps. 
We add a clock variable modeling the current time and an authenticator
replay cache recording triples @{term "(A, Kab, Ta)"} of agents, session keys,
and authenticator timestamps. The inclusion of the session key avoids false
replay rejections for different keys with identical authenticator timestamps.

The frames, runs, and observations remain the same as in the previous model, 
but we will use the @{typ "nat list"}'s to store timestamps. 
›

type_synonym
  time = "nat"                     ― ‹for clock and timestamps›

consts
  Ls :: "time"                     ― ‹life time for session keys›
  La :: "time"                     ― ‹life time for authenticators›


text ‹State and observations›

record
  m1_state = "m1r_state" +
    leak :: "(key × agent × agent × nonce × time) set"   ― ‹key leaked plus context›
    clk :: "time" 
    cache :: "(agent × key × time) set" 

type_synonym m1_obs = "m1_state"

type_synonym 'x m1_pred = "'x m1_state_scheme set"
type_synonym 'x m1_trans = "('x m1_state_scheme × 'x m1_state_scheme) set"

consts
  END :: "atom"                    ― ‹run end marker (for initiator)›


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

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

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

definition       ― ‹by @{term "Server"}, refines @{term m1x_step3}›
  m1_step3 :: "[rid_t, agent, agent, key, nonce, time] ⇒ 'x m1_trans"
where
  "m1_step3 Rs A B Kab Na Ts ≡ {(s, s').
     ― ‹new guards:›
     Ts = clk s ∧                      ― ‹fresh timestamp›

     ― ‹rest as before:›
     (s, s') ∈ m1a_step3 Rs A B Kab Na [aNum Ts]
  }"

definition         ― ‹by @{text "A"}, refines @{term m1x_step5}›
  m1_step4 :: "[rid_t, agent, agent, nonce, key, time, time] ⇒ 'x m1_trans"
where
  "m1_step4 Ra A B Na Kab Ts Ta ≡ {(s, s').
     ― ‹previous guards:›
     runs s Ra = Some (Init, [A, B], []) ∧
     (Kab ∉ Domain (leak s) ⟶ (Kab, A) ∈ azC (runs s)) ∧   ― ‹authorization guard›
     Na = Ra$na ∧                                     ― ‹fix parameter›

     ― ‹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, aNum Ts]))) ∧

     ― ‹new guards:›
     Ta = clk s ∧                     ― ‹fresh timestamp›
     clk s < Ts + Ls ∧                ― ‹ensure session key recentness›

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

definition         ― ‹by @{term "B"}, refines @{term m1x_step4}›
  m1_step5 :: "[rid_t, agent, agent, key, time, time] ⇒ 'x m1_trans"
where
  "m1_step5 Rb A B Kab Ts Ta ≡ {(s, s'). 
     ― ‹previous guards:›
     runs s Rb = Some (Resp, [A, B], []) ∧ 
     (Kab ∉ Domain (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, aNum Ts]))) ∧

     ― ‹new guards:›
     ― ‹guard for showing agreement with initiator ‹A› on ‹(Kab, Ts, Ta)››
     (A ∉ bad ⟶ B ∉ bad ⟶ 
       (∃Ra nl. runs s Ra = Some (Init, [A, B], aKey Kab # aNum Ts # aNum Ta # nl))) ∧

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

     ― ‹check validity of authenticator and prevent its replay›
     ― ‹'replays' with fresh authenticator ok!›
     clk s < Ta + La ∧ 
     (B, Kab, Ta) ∉ cache s ∧ 

     ― ‹actions:›
     s' = s⦇
       runs := (runs s)(Rb ↦ (Resp, [A, B], [aKey Kab, aNum Ts, aNum Ta])),
       cache := insert (B, Kab, Ta) (cache s) 
     ⦈
  }"

definition         ― ‹by @{term "A"}, refines @{term skip}›
  m1_step6 :: "[rid_t, agent, agent, nonce, key, time, time] ⇒ 'x m1_trans"
where
  "m1_step6 Ra A B Na Kab Ts Ta ≡ {(s, s').
     runs s Ra = Some (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta]) ∧  ― ‹key recv'd before›
     Na = Ra$na ∧                                                     ― ‹fix parameter›

     ― ‹check key's freshness [NEW]›
     ― ‹‹clk s < Ts + Ls ∧››

     ― ‹guard for showing agreement with ‹B› on ‹Kab›, ‹Ts›, and ‹Ta››
     (A ∉ bad ⟶ B ∉ bad ⟶ 
       (∃Rb. runs s Rb = Some (Resp, [A, B], [aKey Kab, aNum Ts, aNum Ta]))) ∧ 

     ― ‹actions: (redundant) update local state marks successful termination›
     s' = s⦇
       runs := (runs s)(Ra ↦ (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta, END])) 
     ⦈
  }"

definition         ― ‹by attacker, refines @{term m1a_leak}›
  m1_leak :: "[rid_t, agent, agent, nonce, time] ⇒ 'x m1_trans"
where
  "m1_leak Rs A B Na Ts ≡ {(s, s1).
    ― ‹guards:›
    runs s Rs = Some (Serv, [A, B], [aNon Na, aNum Ts]) ∧ 
    (clk s ≥ Ts + Ls) ∧             ― ‹only compromise 'old' session keys›

    ― ‹actions:›
    ― ‹record session key as leaked;›
    s1 = s⦇ leak := insert (sesK (Rs$sk), A, B, Na, Ts) (leak s) ⦈ 
  }"


text ‹Clock tick event›

definition     ― ‹refines @{term skip}›
  m1_tick :: "time ⇒ 'x m1_trans"
where
  "m1_tick T ≡ {(s, s').
     s' = s⦇ clk := clk s + T ⦈ 
  }"


text ‹Purge event: purge cache of expired timestamps›

definition     ― ‹refines @{term skip}›
  m1_purge :: "agent ⇒ 'x m1_trans"
where
  "m1_purge A ≡ {(s, s').
     s' = s⦇ 
       cache := cache s - {(A, K, T) | A K T. 
         (A, K, T) ∈ cache s ∧ T + La ≤ clk s
       } 
     ⦈ 
  }"


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

definition
  m1_init :: "m1_state set"
where
  "m1_init ≡ { ⦇ runs = Map.empty, leak = corrKey × {undefined}, clk = 0, cache = {} ⦈ }" 

definition 
  m1_trans :: "'x m1_trans" where
  "m1_trans ≡ (⋃A B Ra Rb Rs Na Kab Ts Ta T.
        m1_step1 Ra A B Na ∪
        m1_step2 Rb A B ∪
        m1_step3 Rs A B Kab Na Ts ∪
        m1_step4 Ra A B Na Kab Ts Ta ∪
        m1_step5 Rb A B Kab Ts Ta ∪
        m1_step6 Ra A B Na Kab Ts Ta ∪ 
        m1_leak Rs A B Na Ts ∪
        m1_tick T ∪
        m1_purge A ∪ 
        Id
  )"

definition 
  m1 :: "(m1_state, m1_obs) spec" where
  "m1 ≡ ⦇
      init = m1_init,
      trans = m1_trans,
      obs = id
  ⦈" 

lemmas m1_loc_defs = 
  m1_def m1_init_def m1_trans_def
  m1_step1_def m1_step2_def m1_step3_def m1_step4_def m1_step5_def 
  m1_step6_def m1_leak_def m1_purge_def m1_tick_def

lemmas m1_defs = m1_loc_defs m1a_defs

lemma m1_obs_id [simp]: "obs m1 = id"
by (simp add: m1_def)


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

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

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

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

lemmas m1_inv0_finI = m1_inv0_fin_def [THEN setc_def_to_intro, rule_format]
lemmas m1_inv0_finE [elim] = m1_inv0_fin_def [THEN setc_def_to_elim, rule_format]
lemmas m1_inv0_finD = m1_inv0_fin_def [THEN setc_def_to_dest, rule_format]

text ‹Invariance proofs.›

lemma PO_m1_inv0_fin_init [iff]:
  "init m1 ⊆ m1_inv0_fin"
by (auto simp add: m1_defs intro!: m1_inv0_finI)

lemma PO_m1_inv0_fin_trans [iff]:
  "{m1_inv0_fin} trans m1 {> m1_inv0_fin}"
by (auto simp add: PO_hoare_defs m1_defs intro!: m1_inv0_finI)

lemma PO_m1_inv0_fin [iff]: "reach m1 ⊆ m1_inv0_fin"
by (rule inv_rule_incr, auto del: subsetI)


subsubsection ‹inv1: Caching invariant for responder›
(*inv**************************************************************************)

definition 
  m1_inv1r_cache :: "'x m1_pred"
where
  "m1_inv1r_cache ≡ {s. ∀Rb A B Kab Ts Ta nl.
     runs s Rb = Some (Resp, [A, B], aKey Kab # aNum Ts # aNum Ta # nl) ⟶ 
     clk s < Ta + La ⟶
       (B, Kab, Ta) ∈ cache s
  }"

lemmas m1_inv1r_cacheI = m1_inv1r_cache_def [THEN setc_def_to_intro, rule_format]
lemmas m1_inv1r_cacheE [elim] = m1_inv1r_cache_def [THEN setc_def_to_elim, rule_format]
lemmas m1_inv1r_cacheD = m1_inv1r_cache_def [THEN setc_def_to_dest, rule_format, rotated 1]


text ‹Invariance proof›

lemma PO_m1_inv1r_cache_init [iff]:
  "init m1 ⊆ m1_inv1r_cache"
by (auto simp add: m1_defs intro!: m1_inv1r_cacheI)

lemma PO_m1_inv1r_cache_trans [iff]:
  "{m1_inv1r_cache} trans m1 {> m1_inv1r_cache}"
apply (auto simp add: PO_hoare_defs m1_defs intro!: m1_inv1r_cacheI
            dest: m1_inv1r_cacheD)
apply (auto dest: m1_inv1r_cacheD)
done

lemma PO_m1_inv1r_cache [iff]: "reach m1 ⊆ m1_inv1r_cache"
by (rule inv_rule_basic) (auto del: subsetI)


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

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

text ‹The abstraction removes all but the first freshness
identifiers (corresponding to ‹Kab› and ‹Ts›) from the 
initiator and responder frames and leaves the server's freshness ids untouched.
›

overloading is_len' ≡ "is_len" rs_len' ≡ "rs_len" begin
definition is_len_def [simp]: "is_len' ≡ 1::nat"
definition rs_len_def [simp]: "rs_len' ≡ 1::nat"
end

fun 
  rm1a1 :: "role_t ⇒ atom list ⇒ atom list"
where
  "rm1a1 Init = take (Suc is_len)"       ― ‹take ‹Kab›, ‹Ts›; drop ‹Ta››
| "rm1a1 Resp = take (Suc rs_len)"       ― ‹take ‹Kab›, ‹Ts›; drop ‹Ta››
| "rm1a1 Serv = id"                      ― ‹take ‹Na›, ‹Ts››

abbreviation 
  runs1a1 :: "runs_t ⇒ runs_t" where
  "runs1a1 ≡ map_runs rm1a1" 

lemma knC_runs1a1 [simp]:
  "knC (runs1a1 runz) = knC runz"
apply (auto simp add: map_runs_def elim!: knC.cases)
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_tac knC_serv, auto simp add: map_runs_def)
done

text ‹med1a1: The mediator function maps a concrete observation (i.e., run) 
to an abstract one.›

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

definition
  med1a1 :: "m1_obs ⇒ m1a_obs" where
  "med1a1 s ≡ ⦇ runs = runs1a1 (runs s), m1x_state.leak = Domain (leak s) ⦈"
   
definition
  R1a1 :: "(m1a_state × m1_state) set" where
  "R1a1 ≡ {(s, t). s = med1a1 t}"

lemmas R1a1_defs = R1a1_def med1a1_def 


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

lemma PO_m1_step1_refines_m1a_step1:
  "{R1a1} 
     (m1a_step1 Ra A B Na), (m1_step1 Ra A B Na) 
   {> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)

lemma PO_m1_step2_refines_m1a_step2:
  "{R1a1} 
     (m1a_step2 Rb A B), (m1_step2 Rb A B) 
   {> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)

lemma PO_m1_step3_refines_m1a_step3:
  "{R1a1} 
     (m1a_step3 Rs A B Kab Na [aNum Ts]), (m1_step3 Rs A B Kab Na Ts)
   {> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)

lemma PO_m1_step4_refines_m1a_step4:
  "{R1a1} 
     (m1a_step4 Ra A B Na Kab [aNum Ts]), (m1_step4 Ra A B Na Kab Ts Ta) 
   {> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs map_runs_def)

lemma PO_m1_step5_refines_m1a_step5:
  "{R1a1} 
     (m1a_step5 Rb A B Kab [aNum Ts]), (m1_step5 Rb A B Kab Ts Ta) 
   {> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs map_runs_def)

lemma PO_m1_step6_refines_m1a_skip:
  "{R1a1} 
     Id, (m1_step6 Ra A B Na Kab Ts Ta)
   {> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs map_runs_def)

lemma PO_m1_leak_refines_m1a_leak:
  "{R1a1} 
     (m1a_leak Rs), (m1_leak Rs A B Na Ts)
   {> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs map_runs_def dest: dom_lemmas)

lemma PO_m1_tick_refines_m1a_skip:
  "{R1a1} 
     Id, (m1_tick T) 
   {> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs map_runs_def)

lemma PO_m1_purge_refines_m1a_skip:
  "{R1a1} 
     Id, (m1_purge A) 
   {> R1a1}"
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs map_runs_def)

text ‹All together now...›

lemmas PO_m1_trans_refines_m1a_trans = 
  PO_m1_step1_refines_m1a_step1 PO_m1_step2_refines_m1a_step2
  PO_m1_step3_refines_m1a_step3 PO_m1_step4_refines_m1a_step4
  PO_m1_step5_refines_m1a_step5 PO_m1_step6_refines_m1a_skip 
  PO_m1_leak_refines_m1a_leak PO_m1_tick_refines_m1a_skip 
  PO_m1_purge_refines_m1a_skip

lemma PO_m1_refines_init_m1a [iff]:
  "init m1 ⊆  R1a1``(init m1a)"
by (auto simp add: R1a1_defs m1_defs intro!: s0g_secrecyI)

lemma PO_m1_refines_trans_m1a [iff]:
  "{R1a1} 
     (trans m1a), (trans m1) 
   {> R1a1}"
apply (auto simp add: m1_def m1_trans_def m1a_def m1a_trans_def
         intro!: PO_m1_trans_refines_m1a_trans)
apply (force intro!: PO_m1_trans_refines_m1a_trans)+
done

text ‹Observation consistency.›

lemma obs_consistent_med1a1 [iff]: 
  "obs_consistent R1a1 med1a1 m1a m1"
by (auto simp add: obs_consistent_def R1a1_def m1a_def m1_def)


text ‹Refinement result.›

lemma PO_m1_refines_m1a [iff]: 
  "refines R1a1 med1a1 m1a m1"
by (rule Refinement_basic) (auto del: subsetI)

lemma  m1_implements_m1a [iff]: "implements med1a1 m1a m1"
by (rule refinement_soundness) (fast)


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

text ‹Secrecy, as external and internal invariant›

definition 
  m1_secrecy :: "'x m1_pred" where
  "m1_secrecy ≡ {s. knC (runs s) ⊆ azC (runs s) ∪ Domain (leak s) × UNIV}"

lemmas m1_secrecyI = m1_secrecy_def [THEN setc_def_to_intro, rule_format]
lemmas m1_secrecyE [elim] = m1_secrecy_def [THEN setc_def_to_elim, rule_format]

lemma PO_m1_obs_secrecy [iff]: "oreach m1 ⊆ m1_secrecy"
apply (rule_tac Q=m1x_secrecy in external_invariant_translation)
apply (auto del: subsetI)
apply (fastforce simp add: med1a1_def intro!: m1_secrecyI)
done

lemma PO_m1_secrecy [iff]: "reach m1 ⊆ m1_secrecy"
by (rule external_to_internal_invariant) (auto del: subsetI)


subsubsection ‹inv (inherited): Responder auth server.›
(*invh*************************************************************************)

definition 
  m1_inv2r_serv :: "'x m1r_pred"
where
  "m1_inv2r_serv ≡ {s. ∀A B Rb Kab Ts nlb.
     B ∉ bad ⟶ 
     runs s Rb = Some (Resp, [A, B], aKey Kab # aNum Ts # nlb) ⟶
       (∃Rs Na. Kab = sesK (Rs$sk) ∧ 
          runs s Rs = Some (Serv, [A, B], [aNon Na, aNum Ts]))
  }"

lemmas m1_inv2r_servI = m1_inv2r_serv_def [THEN setc_def_to_intro, rule_format]
lemmas m1_inv2r_servE [elim] = m1_inv2r_serv_def [THEN setc_def_to_elim, rule_format]
lemmas m1_inv2r_servD = m1_inv2r_serv_def [THEN setc_def_to_dest, rule_format, rotated -1]


text ‹Proof of invariance.›

lemma PO_m1_inv2r_serv [iff]: "reach m1 ⊆ m1_inv2r_serv"
apply (rule_tac Sa=m1a and Pa=m1a_inv2r_serv 
       and Qa=m1a_inv2r_serv and Q=m1_inv2r_serv 
       in internal_invariant_translation)
apply (auto del: subsetI)
― ‹1 subgoal›
apply (auto simp add: vimage_def intro!: m1_inv2r_servI)
apply (simp add: m1a_inv2r_serv_def med1a1_def)
apply (rename_tac x A B Rb Kab Ts nlb)
apply (drule_tac x=A in spec)
apply (drule_tac x=B in spec, clarsimp)
apply (drule_tac x=Rb in spec)
apply (drule_tac x=Kab in spec)
apply (drule_tac x="[aNum Ts]" in spec)
apply (auto simp add: map_runs_def) 
done


subsubsection ‹inv (inherited): Initiator auth server.›
(*invh*************************************************************************)

text ‹Simplified version of invariant ‹m1a_inv2i_serv›.›

definition 
  m1_inv2i_serv :: "'x m1r_pred"
where
  "m1_inv2i_serv ≡ {s. ∀A B Ra Kab Ts nla.
     A ∉ bad ⟶ 
     runs s Ra = Some (Init, [A, B], aKey Kab # aNum Ts # nla) ⟶
       (∃Rs. Kab = sesK (Rs$sk) ∧
         runs s Rs = Some (Serv, [A, B],  [aNon (Ra$na), aNum Ts]))
  }"

lemmas m1_inv2i_servI = m1_inv2i_serv_def [THEN setc_def_to_intro, rule_format]
lemmas m1_inv2i_servE [elim] = m1_inv2i_serv_def [THEN setc_def_to_elim, rule_format]
lemmas m1_inv2i_servD = m1_inv2i_serv_def [THEN setc_def_to_dest, rule_format, rotated -1]


text ‹Proof of invariance.›

lemma PO_m1_inv2i_serv [iff]: "reach m1 ⊆ m1_inv2i_serv"
apply (rule_tac Pa=m1a_inv2i_serv and Qa=m1a_inv2i_serv and Q=m1_inv2i_serv
       in internal_invariant_translation)
apply (auto del: subsetI)
― ‹1 subgoal›
apply (auto simp add: m1a_inv2i_serv_def med1a1_def vimage_def intro!: m1_inv2i_servI)
apply (rename_tac x A B Ra Kab Ts nla)
apply (drule_tac x=A in spec, clarsimp)
apply (drule_tac x=B in spec) 
apply (drule_tac x=Ra in spec) 
apply (drule_tac x=Kab in spec) 
apply (drule_tac x="[aNum Ts]" in spec)
apply (auto simp add: map_runs_def)
done

declare PO_m1_inv2i_serv [THEN subsetD, intro]


subsubsection ‹inv (inherited): Initiator key freshness›
(*invh*************************************************************************)

definition 
  m1_inv1_ifresh :: "'x m1_pred"
where
  "m1_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 ∉ Domain (leak s) ⟶
       Ra = Ra'
  }"

lemmas m1_inv1_ifreshI = m1_inv1_ifresh_def [THEN setc_def_to_intro, rule_format]
lemmas m1_inv1_ifreshE [elim] = m1_inv1_ifresh_def [THEN setc_def_to_elim, rule_format]
lemmas m1_inv1_ifreshD = m1_inv1_ifresh_def [THEN setc_def_to_dest, rule_format, rotated 1]

lemma PO_m1_ifresh [iff]: "reach m1 ⊆ m1_inv1_ifresh"
apply (rule_tac Pa=m1a_inv1_ifresh and Qa=m1a_inv1_ifresh and Q=m1_inv1_ifresh
       in internal_invariant_translation)
apply (auto del: subsetI)
apply (auto simp add: med1a1_def map_runs_def vimage_def m1_inv1_ifresh_def)
done


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

text ‹The responder injectively agrees with the initiator on @{term "Kab"},
@{term "Ts"}, and @{term "Ta"}.›


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

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

type_synonym
  risig = "key × time × time"

abbreviation
  ri_running :: "[runs_t, agent, agent, key, time, time] ⇒ rid_t set" 
where
  "ri_running runz A B Kab Ts Ta ≡ {Ra. ∃nl. 
     runz Ra = Some (Init, [A, B], aKey Kab # aNum Ts # aNum Ta # nl)
  }"

abbreviation
  ri_commit :: "[runs_t, agent, agent, key, time, time] ⇒ rid_t set" 
where
  "ri_commit runz A B Kab Ts Ta ≡ {Rb. ∃nl. 
     runz Rb = Some (Resp, [A, B], aKey Kab # aNum Ts # aNum Ta # nl)
  }"

fun
  ri_runs2sigs :: "runs_t ⇒ risig signal ⇒ nat"
where
  "ri_runs2sigs runz (Running [B, A] (Kab, Ts, Ta)) = 
     card (ri_running runz A B Kab Ts Ta)"

| "ri_runs2sigs runz (Commit [B, A] (Kab, Ts, Ta)) = 
     card (ri_commit runz A B Kab Ts Ta)"

| "ri_runs2sigs runz _ = 0"


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

definition 
  med_a0iim1_ri :: "m1_obs ⇒ risig a0i_obs" where
  "med_a0iim1_ri o1 ≡ ⦇ signals = ri_runs2sigs (runs o1), corrupted = {} ⦈"

definition
  R_a0iim1_ri :: "(risig a0i_state × m1_state) set" where
  "R_a0iim1_ri ≡ {(s, t). signals s = ri_runs2sigs (runs t) ∧ corrupted s = {} }"

lemmas R_a0iim1_ri_defs = R_a0iim1_ri_def med_a0iim1_ri_def 


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

text ‹Other lemmas›

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

lemma finite_ri_running [simp, intro]:
  "finite (dom runz) ⟹ finite (ri_running runz A B Kab Ts Ta)"
by (auto intro: finite_subset dest: dom_lemmas)

lemma finite_ri_commit [simp, intro]:
  "finite (dom runz) ⟹ finite (ri_commit runz A B Kab Ts Ta)"
by (auto intro: finite_subset dest: dom_lemmas)


text ‹Update lemmas›

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

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

lemma ri_runs2sigs_upd_serv [simp]:
  "⟦ Rs ∉ dom runz ⟧
  ⟹ ri_runs2sigs (runz(Rs ↦ (Serv, [A, B], [aNon Na, aNum Ts]))) 
      = ri_runs2sigs runz"
by (rule ext, erule rev_mp, rule ri_runs2sigs.induct)
   (auto dest: dom_lemmas)

lemma ri_runs2sigs_upd_init_some [simp]:
  "⟦ runz Ra = Some (Init, [A, B], []); finite (dom runz) ⟧
  ⟹ ri_runs2sigs (runz(Ra ↦ (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta]))) =
     (ri_runs2sigs runz)(
       Running [B, A] (Kab, Ts, Ta) := 
         Suc (card (ri_running runz A B Kab Ts Ta)))"
apply (rule ext, (erule rev_mp)+)
apply (rule ri_runs2sigs.induct, auto) 
― ‹1 subgoal›
apply (rename_tac runz)
apply (rule_tac s="card (insert Ra (ri_running runz A B Kab Ts Ta))"
       in trans, fast, auto)
done

lemma ri_runs2sigs_upd_resp_some [simp]:
  "⟦ runz Rb = Some (Resp, [A, B], []); finite (dom runz) ⟧
  ⟹ ri_runs2sigs (runz(Rb ↦ (Resp, [A, B], [aKey Kab, aNum Ts, aNum Ta]))) =
     (ri_runs2sigs runz)(
        Commit [B, A] (Kab, Ts, Ta) := 
          Suc (card (ri_commit runz A B Kab Ts Ta)))"
apply (rule ext, (erule rev_mp)+)
apply (rule ri_runs2sigs.induct, auto)
― ‹1 subgoal›
apply (rename_tac runz)
apply (rule_tac s="card (insert Rb (ri_commit runz A B Kab Ts Ta))"
       in trans, fast, auto)
done

lemma ri_runs2sigs_upd_init_some2 [simp]:
  "⟦ runz Ra = Some (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta]) ⟧
  ⟹ ri_runs2sigs (runz(Ra ↦ (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta, END]))) =
     ri_runs2sigs runz"
by (rule ext, erule rev_mp, rule ri_runs2sigs.induct)
   (auto dest: dom_lemmas)


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

lemma PO_m1_step1_refines_a0_ri_skip:
  "{R_a0iim1_ri} 
     Id, (m1_step1 Ra A B Na) 
   {> R_a0iim1_ri}"
by (auto simp add: PO_rhoare_defs R_a0iim1_ri_defs m1_defs)

lemma PO_m1_step2_refines_a0_ri_skip:
  "{R_a0iim1_ri} 
     Id, (m1_step2 Rb A B) 
   {> R_a0iim1_ri}"
by (auto simp add: PO_rhoare_defs R_a0iim1_ri_defs m1_defs)

lemma PO_m1_step3_refines_a0_ri_skip:
  "{R_a0iim1_ri} 
     Id, (m1_step3 Rs A B Kab Na Ts) 
   {> R_a0iim1_ri}"
by (auto simp add: PO_rhoare_defs R_a0iim1_ri_defs m1_defs)

lemma PO_m1_step4_refines_a0_ri_running:
  "{R_a0iim1_ri ∩ UNIV × m1_inv0_fin} 
     (a0i_running [B, A] (Kab, Ts, Ta)), (m1_step4 Ra A B Na Kab Ts Ta) 
   {> R_a0iim1_ri}"
by (auto simp add: PO_rhoare_defs R_a0iim1_ri_defs a0i_defs m1_defs)

lemma PO_m1_step5_refines_a0_ri_commit:
  "{R_a0iim1_ri ∩ UNIV × (m1_inv1r_cache ∩ m1_inv0_fin)} 
     (a0i_commit [B, A] (Kab, Ts, Ta)), (m1_step5 Rb A B Kab Ts Ta) 
   {> R_a0iim1_ri}"
apply (auto simp add: PO_rhoare_defs R_a0iim1_ri_defs a0i_defs m1_defs)
― ‹2 subgoals›
apply (rename_tac s t aa ab ac ba Rs Na Ra nl,
       subgoal_tac 
         "card (ri_commit (runs t) A B (sesK (Rs$sk)) Ts Ta) = 0 ∧
          card (ri_running (runs t) A B (sesK (Rs$sk)) Ts Ta) > 0", auto)
apply (rename_tac s t Rs Na Ra nl,
       subgoal_tac 
         "card (ri_commit (runs t) A B (sesK (Rs$sk)) Ts Ta) = 0 ∧
          card (ri_running (runs t) A B (sesK (Rs$sk)) Ts Ta) > 0", auto)
done

lemma PO_m1_step6_refines_a0_ri_skip:
  "{R_a0iim1_ri} 
     Id, (m1_step6 Ra A B Na Kab Ts Ta) 
   {> R_a0iim1_ri}"
by (auto simp add: PO_rhoare_defs R_a0iim1_ri_defs m1_defs)

lemma PO_m1_leak_refines_a0_ri_skip:
  "{R_a0iim1_ri} 
     Id, (m1_leak Rs A B Na Ts) 
   {> R_a0iim1_ri}"
by (auto simp add: PO_rhoare_defs R_a0iim1_ri_defs a0i_defs m1_defs)

lemma PO_m1_tick_refines_a0_ri_skip:
  "{R_a0iim1_ri}
     Id, (m1_tick T)
   {> R_a0iim1_ri}"
by (auto simp add: PO_rhoare_defs R_a0iim1_ri_defs m1_defs)

lemma PO_m1_purge_refines_a0_ri_skip:
  "{R_a0iim1_ri}
     Id, (m1_purge A)
   {> R_a0iim1_ri}"
by (auto simp add: PO_rhoare_defs R_a0iim1_ri_defs m1_defs)

text ‹All together now...›

lemmas PO_m1_trans_refines_a0_ri_trans = 
  PO_m1_step1_refines_a0_ri_skip  PO_m1_step2_refines_a0_ri_skip
  PO_m1_step3_refines_a0_ri_skip  PO_m1_step4_refines_a0_ri_running
  PO_m1_step5_refines_a0_ri_commit PO_m1_step6_refines_a0_ri_skip 
  PO_m1_leak_refines_a0_ri_skip PO_m1_tick_refines_a0_ri_skip 
  PO_m1_purge_refines_a0_ri_skip

lemma PO_m1_refines_init_a0_ri [iff]:
  "init m1 ⊆  R_a0iim1_ri``(init a0i)"
by (auto simp add: R_a0iim1_ri_defs a0i_defs m1_defs
         intro!: exI [where x="⦇signals = λs. 0, corrupted = {} ⦈"])

lemma PO_m1_refines_trans_a0_ri [iff]:
  "{R_a0iim1_ri ∩ a0i_inv1_iagree × (m1_inv1r_cache ∩ m1_inv0_fin)} 
     (trans a0i), (trans m1) 
   {> R_a0iim1_ri}"
by (force simp add: m1_def m1_trans_def a0i_def a0i_trans_def
          intro!: PO_m1_trans_refines_a0_ri_trans)


lemma obs_consistent_med_a0iim1_ri [iff]: 
  "obs_consistent 
     (R_a0iim1_ri ∩ a0i_inv1_iagree × (m1_inv1r_cache ∩ m1_inv0_fin))
     med_a0iim1_ri a0i m1"
by (auto simp add: obs_consistent_def R_a0iim1_ri_def med_a0iim1_ri_def 
                   a0i_def m1_def)


text ‹Refinement result.›

lemma PO_m1_refines_a0ii_ri [iff]: 
  "refines 
     (R_a0iim1_ri ∩ a0i_inv1_iagree × (m1_inv1r_cache ∩ m1_inv0_fin))
     med_a0iim1_ri a0i m1"
by (rule Refinement_using_invariants) (auto)

lemma  m1_implements_a0ii_ri: "implements med_a0iim1_ri a0i m1"
by (rule refinement_soundness) (fast)


subsubsection ‹inv3 (inherited): Responder and initiator›
(*invh*************************************************************************)

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

definition 
  m1_inv3r_init :: "'x m1_pred"
where
  "m1_inv3r_init ≡ {s. ∀A B Rb Kab Ts Ta nlb.
     B ∉ bad ⟶ A ∉ bad ⟶ Kab ∉ Domain (leak s) ⟶
     runs s Rb = Some (Resp, [A, B], aKey Kab # aNum Ts # aNum Ta # nlb) ⟶
       (∃Ra nla. 
        runs s Ra = Some (Init, [A, B], aKey Kab # aNum Ts # aNum Ta # nla))
  }"

lemmas m1_inv3r_initI = m1_inv3r_init_def [THEN setc_def_to_intro, rule_format]
lemmas m1_inv3r_initE [elim] = m1_inv3r_init_def [THEN setc_def_to_elim, rule_format]
lemmas m1_inv3r_initD = m1_inv3r_init_def [THEN setc_def_to_dest, rule_format, rotated -1]


text ‹Invariance proof.›

lemma PO_m1_inv3r_init [iff]: "reach m1 ⊆ m1_inv3r_init"
apply (rule INV_from_Refinement_basic [OF PO_m1_refines_a0ii_ri])
apply (auto simp add: R_a0iim1_ri_def a0i_inv1_iagree_def
            intro!:  m1_inv3r_initI)
― ‹1 subgoal›
apply (rename_tac s A B Rb Kab Ts Ta nlb a)
apply (drule_tac x="[B, A]" in spec, clarsimp)
apply (drule_tac x="Kab" in spec)
apply (drule_tac x="Ts" in spec)
apply (drule_tac x="Ta" in spec)
apply (subgoal_tac "card (ri_commit (runs s) A B Kab Ts Ta) > 0", auto) 
done


subsubsection ‹inv4: Key freshness for responder›
(*inv*************************************************************************)

definition 
  m1_inv4_rfresh :: "'x m1_pred"
where
  "m1_inv4_rfresh ≡ {s. ∀Rb1 Rb2 A1 A2 B1 B2 Kab Ts1 Ts2 Ta1 Ta2.
     runs s Rb1 = Some (Resp, [A1, B1], [aKey Kab, aNum Ts1, aNum Ta1]) ⟶ 
     runs s Rb2 = Some (Resp, [A2, B2], [aKey Kab, aNum Ts2, aNum Ta2]) ⟶ 
     B1 ∉ bad ⟶ A1 ∉ bad ⟶ Kab ∉ Domain (leak s) ⟶
       Rb1 = Rb2
  }"

lemmas m1_inv4_rfreshI = m1_inv4_rfresh_def [THEN setc_def_to_intro, rule_format]
lemmas m1_inv4_rfreshE [elim] = m1_inv4_rfresh_def [THEN setc_def_to_elim, rule_format]
lemmas m1_inv4_rfreshD = m1_inv4_rfresh_def [THEN setc_def_to_dest, rule_format, rotated 1]


text ‹Proof of key freshness for responder. All cases except step5 are straightforward.›

lemma PO_m1_inv4_rfresh_step5:
  "{m1_inv4_rfresh ∩ m1_inv3r_init ∩ m1_inv2r_serv ∩ m1_inv1r_cache ∩
    m1_secrecy ∩ m1_inv1_ifresh} 
     (m1_step5 Rb A B Kab Ts Ta)
   {> m1_inv4_rfresh}"
apply (auto simp add: PO_hoare_defs m1_defs intro!: m1_inv4_rfreshI)
apply (auto dest: m1_inv4_rfreshD)
apply (auto dest: m1_inv2r_servD) 

― ‹5 subgoals›
  apply (drule m1_inv2r_servD, auto) 
  apply (elim azC.cases, auto)

  apply (drule m1_inv2r_servD, auto)
  apply (elim azC.cases, auto)

  apply (drule m1_inv2r_servD, auto)
  apply (elim azC.cases, auto)

  apply (rename_tac Rb2 A2 B2 Ts2 Ta2 s Rs Na Ra nl)
  apply (case_tac "B2 ∈ bad")
    apply (thin_tac "(sesK (Rs$sk), B) ∈ azC (runs s)")
    apply (subgoal_tac "(sesK (Rs$sk), B2) ∈ azC (runs s)")
    apply (erule azC.cases, auto)
    apply (erule m1_secrecyE, auto) 

    apply (case_tac "A2 ∈ bad", auto dest: m1_inv2r_servD)
    apply (frule m1_inv3r_initD, auto)
    apply (rename_tac Raa nla, subgoal_tac "Raa = Ra", auto)    ― ‹uses cache invariant›

  apply (frule m1_inv3r_initD, auto)
  apply (rename_tac Raa nla, subgoal_tac "Raa = Ra", auto)      ― ‹uses cache invariant›
done

lemmas PO_m1_inv4_rfresh_step5_lemmas = 
  PO_m1_inv4_rfresh_step5

lemma PO_m1_inv4_rfresh_init [iff]:
  "init m1 ⊆ m1_inv4_rfresh"
by (auto simp add: m1_defs intro!: m1_inv4_rfreshI)

lemma PO_m1_inv4_rfresh_trans [iff]:
  "{m1_inv4_rfresh ∩ m1_inv3r_init ∩ m1_inv2r_serv ∩ m1_inv1r_cache ∩
    m1_secrecy ∩ m1_inv1_ifresh} 
      trans m1 
   {> m1_inv4_rfresh}"
by (auto simp add: m1_def m1_trans_def intro!: PO_m1_inv4_rfresh_step5_lemmas)
   (auto simp add: PO_hoare_defs m1_defs intro!: m1_inv4_rfreshI dest: m1_inv4_rfreshD)


lemma PO_m1_inv4_rfresh [iff]: "reach m1 ⊆ m1_inv4_rfresh"
apply (rule_tac 
         J="m1_inv3r_init ∩ m1_inv2r_serv ∩ m1_inv1r_cache ∩ m1_secrecy ∩ m1_inv1_ifresh" 
       in inv_rule_incr) 
apply (auto simp add: Int_assoc del: subsetI)
done

lemma PO_m1_obs_inv4_rfresh [iff]: "oreach m1 ⊆ m1_inv4_rfresh"
by (rule external_from_internal_invariant)
   (auto del: subsetI)


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

text ‹The initiator injectively agrees with the responder on ‹Kab›,
‹Ts›, and ‹Ta›.›


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

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

type_synonym
  irsig = "key × time × time"

abbreviation
  ir_running :: "[runs_t, agent, agent, key, time, time] ⇒ rid_t set" 
where
  "ir_running runz A B Kab Ts Ta ≡ {Rb. ∃nl. 
     runz Rb = Some (Resp, [A, B], aKey Kab # aNum Ts # aNum Ta # nl)
  }"

abbreviation
  ir_commit :: "[runs_t, agent, agent, key, time, time] ⇒ rid_t set" 
where
  "ir_commit runz A B Kab Ts Ta ≡ {Ra. ∃nl. 
     runz Ra = Some (Init, [A, B], aKey Kab # aNum Ts # aNum Ta # END # nl)
  }"

fun
  ir_runs2sigs :: "runs_t ⇒ risig signal ⇒ nat"
where
 "ir_runs2sigs runz (Running [A, B] (Kab, Ts, Ta)) = 
     card (ir_running runz A B Kab Ts Ta)"

| "ir_runs2sigs runz (Commit [A, B] (Kab, Ts, Ta)) = 
     card (ir_commit runz A B Kab Ts Ta)"

| "ir_runs2sigs runz _ = 0"


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

definition 
  med_a0iim1_ir :: "m1_obs ⇒ irsig a0i_obs" where
  "med_a0iim1_ir o1 ≡ ⦇ signals = ir_runs2sigs (runs o1), corrupted = {} ⦈"

definition
  R_a0iim1_ir :: "(irsig a0i_state × m1_state) set" where
  "R_a0iim1_ir ≡ {(s, t). signals s = ir_runs2sigs (runs t) ∧ corrupted s = {} }"

lemmas R_a0iim1_ir_defs = R_a0iim1_ir_def med_a0iim1_ir_def


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

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

(* already proven higher up:
lemma ir_running_finite [simp, intro]:
  "finite (dom runz) ⟹ finite (ir_running runz A B Kab Ts Ta)"
by (auto intro: finite_subset dest: dom_lemmas) 
*)

lemma ir_commit_finite [simp, intro]:
  "finite (dom runz) ⟹ finite (ir_commit runz A B Kab Ts Ta)"
by (auto intro: finite_subset dest: dom_lemmas)


text ‹Update lemmas›

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

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

lemma ir_runs2sigs_upd_serv [simp]:
  "⟦ Rs ∉ dom (runs y) ⟧
  ⟹ ir_runs2sigs ((runs y)(Rs ↦ (Serv, [A, B], [aNon Na, aNum Ts]))) 
      = ir_runs2sigs (runs y)"
by (rule ext, erule rev_mp) 
   (rule ir_runs2sigs.induct, auto dest: dom_lemmas)

lemma ir_runs2sigs_upd_init_some [simp]:
  "⟦ runz Ra = Some (Init, [A, B], []) ⟧
  ⟹ ir_runs2sigs (runz(Ra ↦ (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta]))) =
     ir_runs2sigs runz"
by (rule ext, erule rev_mp) 
   (rule ir_runs2sigs.induct, auto dest: dom_lemmas)

lemma ir_runs2sigs_upd_resp_some_raw:
  assumes
    "runz Rb = Some (Resp, [A, B], [])" 
    "finite (dom runz)"
  shows
    "ir_runs2sigs (runz(Rb ↦ (Resp, [A, B], [aKey Kab, aNum Ts, aNum Ta]))) s =
     ((ir_runs2sigs runz)(
       Running [A, B] (Kab, Ts, Ta) := 
         Suc (card (ir_running runz A B Kab Ts Ta)))) s"
  using assms
proof (induct rule: ir_runs2sigs.induct) 
  case (1 runz A B Kab Ts Ta) note H = this
    hence "Rb ∉ ir_running runz A B Kab Ts Ta" by auto
    moreover
    with H have
      "card (insert Rb (ir_running runz A B Kab Ts Ta)) 
       = Suc (card (ir_running runz A B Kab Ts Ta))" by auto
  ultimately show ?case by (auto elim: subst)
qed (auto)

lemma ir_runs2sigs_upd_resp_some [simp]:
  "⟦ runz Rb = Some (Resp, [A, B], []); finite (dom runz) ⟧
  ⟹ ir_runs2sigs (runz(Rb ↦ (Resp, [A, B], [aKey Kab, aNum Ts, aNum Ta]))) =
     (ir_runs2sigs runz)(
       Running [A, B] (Kab, Ts, Ta) := 
         Suc (card (ir_running runz A B Kab Ts Ta)))"
by (intro ext ir_runs2sigs_upd_resp_some_raw)

lemma ir_runs2sigs_upd_init_some2_raw:
  assumes 
    "runz Ra = Some (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta])" 
    "finite (dom runz)" 
  shows
    "ir_runs2sigs (runz(Ra ↦ (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta, END]))) s =
     ((ir_runs2sigs runz)(
        Commit [A, B] (Kab, Ts, Ta) := 
          Suc (card (ir_commit runz A B Kab Ts Ta)))) s"
  using assms
proof (induct runz s rule: ir_runs2sigs.induct)
  case (2 runz A B Kab Ts Ta) note H = this 
    from H have "Ra ∉ ir_commit runz A B Kab Ts Ta" by auto
    moreover
    with H have 
      "card (insert Ra (ir_commit runz A B Kab Ts Ta)) 
       = Suc (card (ir_commit runz A B Kab Ts Ta))" 
    by (auto)
    ultimately show ?case by (auto elim: subst)
qed (auto)

lemma ir_runs2sigs_upd_init_some2 [simp]:
  "⟦ runz Na = Some (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta]); finite (dom runz) ⟧
  ⟹ ir_runs2sigs (runz(Na ↦ (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta, END]))) =
     (ir_runs2sigs runz)(
        Commit [A, B] (Kab, Ts, Ta) := 
          Suc (card (ir_commit runz A B Kab Ts Ta)))"
by (intro ir_runs2sigs_upd_init_some2_raw ext)


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

lemma PO_m1_step1_refines_ir_a0ii_skip:
  "{R_a0iim1_ir} 
     Id, (m1_step1 Ra A B Na) 
   {> R_a0iim1_ir}"
by (simp add: PO_rhoare_defs R_a0iim1_ir_defs m1_defs, safe, auto)

lemma PO_m1_step2_refines_ir_a0ii_skip:
  "{R_a0iim1_ir} 
     Id, (m1_step2 Rb A B) 
   {> R_a0iim1_ir}"
by (simp add: PO_rhoare_defs R_a0iim1_ir_defs m1_defs, safe, auto)

lemma PO_m1_step3_refines_ir_a0ii_skip:
  "{R_a0iim1_ir} 
     Id, (m1_step3 Rs A B Kab Na Ts) 
   {> R_a0iim1_ir}"
by (simp add: PO_rhoare_defs R_a0iim1_ir_defs a0i_defs m1_defs, safe, auto)

lemma PO_m1_step4_refines_ir_a0ii_skip:
  "{R_a0iim1_ir} 
     Id, (m1_step4 Ra A B Na Kab Ts Ta) 
   {> R_a0iim1_ir}"
by (simp add: PO_rhoare_defs R_a0iim1_ir_defs m1_defs, safe, auto)

lemma PO_m1_step5_refines_ir_a0ii_running:
  "{R_a0iim1_ir ∩ UNIV × m1_inv0_fin} 
     (a0i_running [A, B] (Kab, Ts, Ta)), (m1_step5 Rb A B Kab Ts Ta) 
   {> R_a0iim1_ir}"
by (simp add: PO_rhoare_defs R_a0iim1_ir_defs a0i_defs m1_defs, safe, auto)

lemma PO_m1_step6_refines_ir_a0ii_commit:
  "{R_a0iim1_ir ∩ UNIV × m1_inv0_fin} 
     (a0n_commit [A, B] (Kab, Ts, Ta)), (m1_step6 Ra A B Na Kab Ts Ta) 
   {> R_a0iim1_ir}"
by (simp add: PO_rhoare_defs R_a0iim1_ir_defs a0n_defs m1_defs, safe, auto)

lemma PO_m1_leak_refines_ir_a0ii_skip:
  "{R_a0iim1_ir}
     Id, (m1_leak Rs A B Na Ts)
   {> R_a0iim1_ir}"
by (simp add: PO_rhoare_defs R_a0iim1_ir_defs a0n_defs m1_defs, safe, auto)

lemma PO_m1_tick_refines_ir_a0ii_skip:
  "{R_a0iim1_ir}
     Id, (m1_tick T)
   {> R_a0iim1_ir}"
by (simp add: PO_rhoare_defs R_a0iim1_ir_defs m1_defs, safe, auto)

lemma PO_m1_purge_refines_ir_a0ii_skip:
  "{R_a0iim1_ir}
     Id, (m1_purge A)
   {> R_a0iim1_ir}"
by (simp add: PO_rhoare_defs R_a0iim1_ir_defs m1_defs, safe, auto)

text ‹All together now...›

lemmas PO_m1_trans_refines_ir_a0ii_trans = 
  PO_m1_step1_refines_ir_a0ii_skip  PO_m1_step2_refines_ir_a0ii_skip
  PO_m1_step3_refines_ir_a0ii_skip  PO_m1_step4_refines_ir_a0ii_skip
  PO_m1_step5_refines_ir_a0ii_running PO_m1_step6_refines_ir_a0ii_commit
  PO_m1_leak_refines_ir_a0ii_skip PO_m1_tick_refines_ir_a0ii_skip 
  PO_m1_purge_refines_ir_a0ii_skip

lemma PO_m1_refines_init_ir_a0ii [iff]:
  "init m1 ⊆  R_a0iim1_ir``(init a0n)"
by (auto simp add: R_a0iim1_ir_defs a0n_defs m1_defs
         intro!: exI [where x="⦇signals = λs. 0, corrupted = {}⦈"])

lemma PO_m1_refines_trans_ir_a0ii [iff]:
  "{R_a0iim1_ir ∩ UNIV × m1_inv0_fin} 
     (trans a0n), (trans m1) 
   {> R_a0iim1_ir}"
by (auto simp add: m1_def m1_trans_def a0n_def a0n_trans_def
         intro!: PO_m1_trans_refines_ir_a0ii_trans)


text ‹Observation consistency.›

lemma obs_consistent_med_a0iim1_ir [iff]: 
  "obs_consistent 
     (R_a0iim1_ir ∩ UNIV × m1_inv0_fin) 
     med_a0iim1_ir a0n m1"
by (auto simp add: obs_consistent_def R_a0iim1_ir_def med_a0iim1_ir_def 
                   a0n_def m1_def)


text ‹Refinement result.›

lemma PO_m1_refines_a0ii_ir [iff]: 
  "refines (R_a0iim1_ir ∩ UNIV × m1_inv0_fin) 
     med_a0iim1_ir a0n m1"
by (rule Refinement_using_invariants) (auto) 

lemma  m1_implements_a0ii_ir: "implements med_a0iim1_ir a0n m1"
by (rule refinement_soundness) (fast)


end