Theory m3_kerberos_par

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

  Project: Development of Security Protocols by Refinement

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

  Key distribution protocols
  Third refinement: parallel version of core Kerberos protocol

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

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

section ‹Core Kerberos, "parallel" variant (L3)›

theory m3_kerberos_par imports m2_kerberos "../Refinement/Message"
begin

text ‹
We model a direct implementation of the channel-based core Kerberos protocol
at Level 2 without ticket forwarding:
\[
\begin{array}{lll}
  \mathrm{M1.} & A \rightarrow S: & A, B, Na \\ 
  \mathrm{M2a.} & S \rightarrow A: & \{Kab, B, Ts, Na\}_{Kas} \\
  \mathrm{M2b.} & S \rightarrow B: & \{Kab, A, Ts\}_{Kbs} \\
  \mathrm{M3.} & A \rightarrow B: & \{A, Ta\}_{Kab} \\
  \mathrm{M4.} & B \rightarrow A: & \{Ta\}_{Kab} \\
\end{array}
\]
›

text ‹Proof tool configuration. Avoid annoying automatic unfolding of
dom›.›

declare domIff [simp, iff del]


(******************************************************************************)
subsection ‹Setup›
(******************************************************************************)

text ‹Now we can define the initial key knowledge.›

overloading ltkeySetup'  ltkeySetup begin
definition ltkeySetup_def: "ltkeySetup'  {(sharK C, A) | C A. A = C  A = Sv}"
end

lemma corrKey_shrK_bad [simp]: "corrKey = shrK`bad"
by (auto simp add: keySetup_def ltkeySetup_def corrKey_def)


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

text ‹The secure channels are star-shaped to/from the server.  Therefore,
we have only one agent in the relation.›

record m3_state = "m1_state" +
  IK :: "msg set"                                ― ‹intruder knowledge›


text ‹Observable state:
@{term "runs"}, @{term "leak"}, @{term "clk"}, and @{term "cache"}.›

type_synonym
  m3_obs = "m2_obs"

definition
  m3_obs :: "m3_state  m3_obs" where
  "m3_obs s   runs = runs s, leak = leak s, clk = clk s, cache = cache s "

type_synonym
  m3_pred = "m3_state set"

type_synonym
  m3_trans = "(m3_state × m3_state) set"


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

text ‹Protocol events.›

definition     ― ‹by @{term "A"}, refines @{term "m2_step1"}
  m3_step1 :: "[rid_t, agent, agent, nonce]  m3_trans"
where
  "m3_step1 Ra A B Na  {(s, s1).
    ― ‹guards:›
    Ra  dom (runs s)                   ― ‹Ra› is fresh›
    Na = Ra$na                          ― ‹generated nonce›

    ― ‹actions:›
    s1 = s
      runs := (runs s)(Ra  (Init, [A, B], [])),
      IK := insert Agent A, Agent B, Nonce Na (IK s)   ― ‹send M1›
    
  }"

definition     ― ‹by @{term "B"}, refines @{term "m2_step2"}
  m3_step2 :: "[rid_t, agent, agent]  m3_trans"
where
  "m3_step2  m1_step2"

definition     ― ‹by @{text "Server"}, refines @{term m2_step3}
  m3_step3 :: "[rid_t, agent, agent, key, nonce, time]  m3_trans"
where
  "m3_step3 Rs A B Kab Na Ts  {(s, s1).
     ― ‹guards:›
     Rs  dom (runs s)                           ― ‹fresh server run›
     Kab = sesK (Rs$sk)                           ― ‹fresh session key›

     Agent A, Agent B, Nonce Na  IK s          ― ‹recv M1›
     Ts = clk s                                   ― ‹fresh timestamp›

     ― ‹actions:›
     ― ‹record session key and send M2›
     s1 = s
       runs := (runs s)(Rs  (Serv, [A, B], [aNon Na, aNum Ts])),
       IK := insert (Crypt (shrK A) Key Kab, Agent B, Number Ts, Nonce Na)
             (insert (Crypt (shrK B) Key Kab,  Agent A, Number Ts)  (IK s))
     
  }"

definition     ― ‹by @{term "A"}, refines @{term m2_step4}
  m3_step4 :: "[rid_t, agent, agent, nonce, key, time, time]  m3_trans"
where
  "m3_step4 Ra A B Na Kab Ts Ta  {(s, s1).
     ― ‹guards:›
     runs s Ra = Some (Init, [A, B], [])            ― ‹key not yet recv'd›
     Na = Ra$na                                      ― ‹generated nonce›

     Crypt (shrK A)                                  ― ‹recv M2a›
       Key Kab, Agent B, Number Ts, Nonce Na  IK s 

     ― ‹read current time›
     Ta = clk s 

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

     ― ‹actions:›
     ― ‹record session key and send M3›
     s1 = s
       runs := (runs s)(Ra  (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta])),
       IK := insert (Crypt Kab Agent A, Number Ta) (IK s)  ― ‹M3›
     
  }"

definition     ― ‹by @{term "B"}, refines @{term m2_step5}
  m3_step5 :: "[rid_t, agent, agent, key, time, time]  m3_trans"
where
  "m3_step5 Rb A B Kab Ts Ta  {(s, s1).
     ― ‹guards:›
     runs s Rb = Some (Resp, [A, B], [])              ― ‹key not yet recv'd›

     Crypt (shrK B) Key Kab, Agent A, Number Ts  IK s    ― ‹recv M2b›
     Crypt Kab Agent A, Number Ta  IK s                  ― ‹recv M3›

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

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

     ― ‹actions:›
     ― ‹record session key›
     s1 = s
       runs := (runs s)(Rb  (Resp, [A, B], [aKey Kab, aNum Ts, aNum Ta])),
       cache := insert (B, Kab, Ta) (cache s),
       IK := insert (Crypt Kab (Number Ta)) (IK s)              ― ‹send M4›
     
  }"

definition     ― ‹by @{term "A"}, refines @{term m2_step6}
  m3_step6 :: "[rid_t, agent, agent, nonce, key, time, time]  m3_trans"
where
  "m3_step6 Ra A B Na Kab Ts Ta  {(s, s').
     ― ‹guards:›
     runs s Ra = Some (Init, [A, B], [aKey Kab, aNum Ts, aNum Ta])   ― ‹knows key›
     Na = Ra$na                                     ― ‹generated nonce›
     clk s < Ts + Ls                                ― ‹check session key's recentness›

     Crypt Kab (Number Ta)  IK s                   ― ‹recv M4›

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

text ‹Clock tick event›

definition   ― ‹refines @{term "m2_tick"}
  m3_tick :: "time  m3_trans"
where
  "m3_tick  m1_tick"


text ‹Purge event: purge cache of expired timestamps›

definition     ― ‹refines @{term "m2_purge"}
  m3_purge :: "agent  m3_trans"
where
  "m3_purge  m1_purge"


text ‹Session key compromise.›

definition     ― ‹refines @{term m2_leak}
  m3_leak :: "[rid_t, agent, agent, nonce, time]  m3_trans"
where
  "m3_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 and add it to intruder knowledge›
    s1 = s leak := insert (sesK (Rs$sk), A, B, Na, Ts) (leak s),
            IK := insert (Key (sesK (Rs$sk))) (IK s) 
  }"

text ‹Intruder fake event. The following "Dolev-Yao" event generates all
intruder-derivable messages.›

definition     ― ‹refines @{term "m2_fake"}
  m3_DY_fake :: "m3_trans"
where
  "m3_DY_fake  {(s, s1).

     ― ‹actions:›
     s1 = s(| IK := synth (analz (IK s)) |)       ― ‹take DY closure›
  }"


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

definition
  m3_init :: "m3_pred"
where
  "m3_init  { 
     runs = Map.empty,
     leak = shrK`bad × {undefined},
     clk = 0,
     cache = {},
     IK = Key`shrK`bad
   }"

definition
  m3_trans :: "m3_trans" where
  "m3_trans  (A B Ra Rb Rs Na Kab Ts Ta T.
     m3_step1 Ra A B Na 
     m3_step2 Rb A B 
     m3_step3 Rs A B Kab Na Ts 
     m3_step4 Ra A B Na Kab Ts Ta 
     m3_step5 Rb A B Kab Ts Ta 
     m3_step6 Ra A B Na Kab Ts Ta 
     m3_tick T 
     m3_purge A 
     m3_leak Rs A B Na Ts 
     m3_DY_fake 
     Id
  )"

definition
  m3 :: "(m3_state, m3_obs) spec" where
  "m3  
    init = m3_init,
    trans = m3_trans,
    obs = m3_obs
  "

lemmas m3_loc_defs =
  m3_def m3_init_def m3_trans_def m3_obs_def
  m3_step1_def m3_step2_def m3_step3_def m3_step4_def m3_step5_def
  m3_step6_def m3_tick_def m3_purge_def m3_leak_def m3_DY_fake_def

lemmas m3_defs = m3_loc_defs m2_defs


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

text ‹Specialized injection that we can apply more aggressively.›

lemmas analz_Inj_IK = analz.Inj [where H="IK s" for s]
lemmas parts_Inj_IK = parts.Inj [where H="IK s" for s]

declare parts_Inj_IK [dest!]

declare analz_into_parts [dest]


subsubsection ‹inv1: Secrecy of pre-distributed shared keys›
(******************************************************************************)

text ‹inv1: Secrecy of long-term keys›

definition
  m3_inv1_lkeysec :: "m3_pred"
where
  "m3_inv1_lkeysec  {s. C.
     (Key (shrK C)  parts (IK s)  C  bad) 
     (C  bad  Key (shrK C)  IK s)
  }"

lemmas m3_inv1_lkeysecI = m3_inv1_lkeysec_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv1_lkeysecE [elim] = m3_inv1_lkeysec_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv1_lkeysec_dest = m3_inv1_lkeysec_def [THEN setc_def_to_dest, rule_format]


text ‹Invariance proof.›

lemma PO_m3_inv1_lkeysec_init [iff]:
  "init m3  m3_inv1_lkeysec"
by (auto simp add: m3_defs intro!: m3_inv1_lkeysecI)

lemma PO_m3_inv1_lkeysec_trans [iff]:
  "{m3_inv1_lkeysec} trans m3 {> m3_inv1_lkeysec}"
by (fastforce simp add: PO_hoare_defs m3_defs intro!: m3_inv1_lkeysecI)

lemma PO_m3_inv1_lkeysec [iff]: "reach m3  m3_inv1_lkeysec"
by (rule inv_rule_basic) (fast+)


text ‹Useful simplifier lemmas›

lemma m3_inv1_lkeysec_for_parts [simp]:
  " s  m3_inv1_lkeysec   Key (shrK C)  parts (IK s)  C  bad"
by auto

lemma m3_inv1_lkeysec_for_analz [simp]:
  " s  m3_inv1_lkeysec   Key (shrK C)  analz (IK s)  C  bad"
by auto


subsubsection ‹inv7a: Session keys not used to encrypt other session keys›
(******************************************************************************)

text ‹Session keys are not used to encrypt other keys. Proof requires
generalization to sets of session keys.

NOTE: This invariant will be derived from the corresponding L2 invariant
using the simulation relation.
›

definition
  m3_inv7a_sesK_compr :: "m3_pred"
where
  "m3_inv7a_sesK_compr  {s. K KK.
     KK  range sesK 
     (Key K  analz (Key`KK  (IK s))) = (K  KK  Key K  analz (IK s))
  }"

lemmas m3_inv7a_sesK_comprI = m3_inv7a_sesK_compr_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv7a_sesK_comprE = m3_inv7a_sesK_compr_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv7a_sesK_comprD = m3_inv7a_sesK_compr_def [THEN setc_def_to_dest, rule_format]

text ‹Additional lemma›
lemmas insert_commute_Key = insert_commute [where x="Key K" for K]

lemmas m3_inv7a_sesK_compr_simps =
  m3_inv7a_sesK_comprD
  m3_inv7a_sesK_comprD [where KK="{Kab}" for Kab, simplified]
  m3_inv7a_sesK_comprD [where KK="insert Kab KK" for Kab KK, simplified]
  insert_commute_Key


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

subsubsection ‹Message abstraction and simulation relation›
(******************************************************************************)

text ‹Abstraction function on sets of messages.›

inductive_set
  abs_msg :: "msg set  chmsg set"
  for H :: "msg set"
where
  am_M1:
    "Agent A, Agent B, Nonce N  H
   Insec A B (Msg [aNon N])  abs_msg H"
| am_M2a:
    "Crypt (shrK C) Key K, Agent B, Number T, Nonce N  H
   Secure Sv C (Msg [aKey K, aAgt B, aNum T, aNon N])  abs_msg H"
| am_M2b:
    "Crypt (shrK C) Key K,  Agent A, Number T  H
   Secure Sv C (Msg [aKey K, aAgt A, aNum T])  abs_msg H"
| am_M3:
    "Crypt K Agent A, Number T  H
   dAuth K (Msg [aAgt A, aNum T])  abs_msg H"
| am_M4:
    "Crypt K (Number T)  H
   dAuth K (Msg [aNum T])  abs_msg H"


text ‹R23: The simulation relation. This is a data refinement of
the insecure and secure channels of refinement 2.›

definition
  R23_msgs :: "(m2_state × m3_state) set" where
  "R23_msgs  {(s, t). abs_msg (parts (IK t))  chan s }"

definition
  R23_keys :: "(m2_state × m3_state) set" where
  "R23_keys  {(s, t). KK K. KK  range sesK 
     Key K  analz (Key`KK  (IK t))  aKey K  extr (aKey`KK  ik0) (chan s)
  }"

definition
  R23_non :: "(m2_state × m3_state) set" where
  "R23_non  {(s, t). KK N. KK  range sesK 
     Nonce N  analz (Key`KK  (IK t))  aNon N  extr (aKey`KK  ik0) (chan s)
  }"

definition
  R23_pres :: "(m2_state × m3_state) set" where
  "R23_pres  {(s, t). runs s = runs t  leak s = leak t  clk s = clk t  cache s = cache t}"

definition
  R23 :: "(m2_state × m3_state) set" where
  "R23  R23_msgs  R23_keys  R23_non  R23_pres"

lemmas R23_defs =
  R23_def R23_msgs_def R23_keys_def R23_non_def R23_pres_def


text ‹The mediator function is the identity here.›

definition
  med32 :: "m3_obs  m2_obs" where
  "med32  id"


lemmas R23_msgsI = R23_msgs_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_msgsE [elim] = R23_msgs_def [THEN rel_def_to_elim, simplified, rule_format]
lemmas R23_msgsE' [elim] = R23_msgs_def [THEN rel_def_to_dest, simplified, rule_format, THEN subsetD]

lemmas R23_keysI = R23_keys_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_keysE [elim] = R23_keys_def [THEN rel_def_to_elim, simplified, rule_format]

lemmas R23_nonI = R23_non_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_nonE [elim] = R23_non_def [THEN rel_def_to_elim, simplified, rule_format]

lemmas R23_presI = R23_pres_def [THEN rel_def_to_intro, simplified, rule_format]
lemmas R23_presE [elim] = R23_pres_def [THEN rel_def_to_elim, simplified, rule_format]

lemmas R23_intros = R23_msgsI R23_keysI R23_nonI R23_presI


text ‹Simplifier lemmas for various instantiations (keys and nonces).›

lemmas R23_keys_simp = R23_keys_def [THEN rel_def_to_dest, simplified, rule_format]
lemmas R23_keys_simps =
  R23_keys_simp
  R23_keys_simp [where KK="{}", simplified]
  R23_keys_simp [where KK="{K'}" for K', simplified]
  R23_keys_simp [where KK="insert K' KK" for K' KK, simplified, OF _ conjI]

lemmas R23_non_simp = R23_non_def [THEN rel_def_to_dest, simplified, rule_format]
lemmas R23_non_simps =
  R23_non_simp
  R23_non_simp [where KK="{}", simplified]
  R23_non_simp [where KK="{K}" for K, simplified]
  R23_non_simp [where KK="insert K KK" for K KK, simplified, OF _ conjI]

lemmas R23_simps = R23_keys_simps R23_non_simps

(*
lemmas R23_keys_emptyD =
  R23_keys_simp [where KK="{}", simplified, THEN iffD1, rotated 1]
  R23_keys_simp [where KK="{}", simplified, THEN iffD2, rotated 1]

lemmas R23_non_emptyD =
  R23_non_simp [where KK="{}", simplified, THEN iffD1, rotated 1]
  R23_non_simp [where KK="{}", simplified, THEN iffD2, rotated 1]

lemmas R23_emptyD = R23_keys_emptyD R23_non_emptyD
*)

subsubsection ‹General lemmas›
(******************************************************************************)

text ‹General facts about @{term "abs_msg"}

declare abs_msg.intros [intro!]
declare abs_msg.cases [elim!]

lemma abs_msg_empty: "abs_msg {} = {}"
by (auto)

lemma abs_msg_Un [simp]:
  "abs_msg (G  H) = abs_msg G  abs_msg H"
by (auto)

lemma abs_msg_mono [elim]:
  " m  abs_msg G; G  H   m  abs_msg H"
by (auto)

lemma abs_msg_insert_mono [intro]:
  " m  abs_msg H   m  abs_msg (insert m' H)"
by (auto)


text ‹Facts about @{term "abs_msg"} concerning abstraction of fakeable
messages. This is crucial for proving the refinement of the intruder event.›

lemma abs_msg_DY_subset_fakeable:
  " (s, t)  R23_msgs; (s, t)  R23_keys; (s, t)  R23_non; t  m3_inv1_lkeysec 
   abs_msg (synth (analz (IK t)))  fake ik0 (dom (runs s)) (chan s)"
apply (auto)
― ‹9 subgoals, deal with replays first›
prefer 2 apply (blast)
prefer 3 apply (blast)
prefer 4 apply (blast)
prefer 5 apply (blast)
― ‹remaining 5 subgoals are real fakes›
apply (intro fake_StatCh fake_DynCh, auto simp add: R23_simps)+
done


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

text ‹Pair decomposition. These were set to \texttt{elim!}, which is too
agressive here.›

declare MPair_analz [rule del, elim]
declare MPair_parts [rule del, elim]


text ‹Protocol events.›

lemma PO_m3_step1_refines_m2_step1:
  "{R23}
     (m2_step1 Ra A B Na), (m3_step1 Ra A B Na)
   {> R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros) (auto)

lemma PO_m3_step2_refines_m2_step2:
  "{R23}
     (m2_step2 Rb A B), (m3_step2 Rb A B)
   {> R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)

lemma PO_m3_step3_refines_m2_step3:
  "{R23  (m2_inv3a_sesK_compr) × (m3_inv7a_sesK_compr  m3_inv1_lkeysec)}
     (m2_step3 Rs A B Kab Na Ts), (m3_step3 Rs A B Kab Na Ts)
   {> R23}"
proof -
  { fix s t
    assume H:
      "(s, t)  R23_msgs" "(s, t)  R23_keys" "(s, t)  R23_non" "(s, t)  R23_pres"
      "s  m2_inv3a_sesK_compr"
      "t  m3_inv7a_sesK_compr" "t  m3_inv1_lkeysec"
      "Kab = sesK (Rs$sk)" "Rs  dom (runs t)"
      " Agent A, Agent B, Nonce Na   parts (IK t)"
    let ?s'=
      "s runs := (runs s)(Rs  (Serv, [A, B], [aNon Na, aNum (clk t)])),
          chan := insert (Secure Sv A (Msg [aKey Kab, aAgt B, aNum (clk t), aNon Na]))
                 (insert (Secure Sv B (Msg [aKey Kab, aAgt A, aNum (clk t)])) (chan s)) "
    let ?t'=
      "t runs := (runs t)(Rs  (Serv, [A, B], [aNon Na, aNum (clk t)])),
          IK := insert (Crypt (shrK A)  Key Kab, Agent B, Number (clk t), Nonce Na )
                (insert (Crypt (shrK B)  Key Kab, Agent A, Number (clk t) ) (IK t)) "
  ― ‹here we go›
    have "(?s', ?t')  R23_msgs" using H
    by (-) (rule R23_intros, auto)
  moreover
    have "(?s', ?t')  R23_keys" using H
    by (-)
       (rule R23_intros,
        auto simp add: m2_inv3a_sesK_compr_simps m3_inv7a_sesK_compr_simps,
        auto simp add: R23_keys_simps)
  moreover
    have "(?s', ?t')  R23_non" using H
    by (-)
       (rule R23_intros,
        auto simp add: m2_inv3a_sesK_compr_simps m3_inv7a_sesK_compr_simps R23_non_simps)
  moreover
    have "(?s', ?t')  R23_pres" using H
    by (-) (rule R23_intros, auto)
  moreover
    note calculation
  }
  thus ?thesis
  by (auto simp add: PO_rhoare_defs R23_def m3_defs)
qed

lemma PO_m3_step4_refines_m2_step4:
  "{R23  UNIV × (m3_inv1_lkeysec) }
     (m2_step4 Ra A B Na Kab Ts Ta), (m3_step4 Ra A B Na Kab Ts Ta)
   {> R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
   (auto)

lemma PO_m3_step5_refines_m2_step5:
  "{R23}
     (m2_step5 Rb A B Kab Ts Ta), (m3_step5 Rb A B Kab Ts Ta)
   {> R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)
   (auto)

lemma PO_m3_step6_refines_m2_step6:
  "{R23}
     (m2_step6 Ra A B Na Kab Ts Ta), (m3_step6 Ra A B Na Kab Ts Ta)
   {> R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)

lemma PO_m3_tick_refines_m2_tick:
  "{R23}
     (m2_tick T), (m3_tick T)
   {>R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)

lemma PO_m3_purge_refines_m2_purge:
  "{R23}
     (m2_purge A), (m3_purge A)
   {>R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros)


text ‹Intruder events.›

lemma PO_m3_leak_refines_m2_leak:
  "{R23}
     (m2_leak Rs A B Na Ts), (m3_leak Rs A B Na Ts)
   {>R23}"
by (auto simp add: PO_rhoare_defs R23_def m3_defs R23_simps intro!: R23_intros)

(* also works, but requires invariants:
apply (auto simp add: m2_inv3a_sesK_compr_simps m2_inv3b_sesK_compr_non_simps
                      m3_inv7a_sesK_compr_simps m3_inv7b_sesK_compr_non_simps
            dest: R23_emptyD)
*)

lemma PO_m3_DY_fake_refines_m2_fake:
  "{R23  UNIV × m3_inv1_lkeysec}
     m2_fake, m3_DY_fake
   {> R23}"
apply (auto simp add: PO_rhoare_defs R23_def m3_defs intro!: R23_intros
            del: abs_msg.cases)
apply (auto intro: abs_msg_DY_subset_fakeable [THEN subsetD]
            del: abs_msg.cases)
apply (auto simp add: R23_simps)
done


text ‹All together now...›

lemmas PO_m3_trans_refines_m2_trans =
  PO_m3_step1_refines_m2_step1 PO_m3_step2_refines_m2_step2
  PO_m3_step3_refines_m2_step3 PO_m3_step4_refines_m2_step4
  PO_m3_step5_refines_m2_step5 PO_m3_step6_refines_m2_step6
  PO_m3_tick_refines_m2_tick PO_m3_purge_refines_m2_purge
  PO_m3_leak_refines_m2_leak PO_m3_DY_fake_refines_m2_fake


lemma PO_m3_refines_init_m2 [iff]:
  "init m3  R23``(init m2)"
by (auto simp add: R23_def m3_defs intro!: R23_intros)

lemma PO_m3_refines_trans_m2 [iff]:
  "{R23  (m2_inv3a_sesK_compr) × (m3_inv7a_sesK_compr  m3_inv1_lkeysec)}
     (trans m2), (trans m3)
   {> R23}"
apply (auto simp add: m3_def m3_trans_def m2_def m2_trans_def)
apply (blast intro!: PO_m3_trans_refines_m2_trans)+
done

lemma PO_m3_observation_consistent [iff]:
  "obs_consistent R23 med32 m2 m3"
by (auto simp add: obs_consistent_def R23_def med32_def m3_defs)


text ‹Refinement result.›

lemma m3_refines_m2 [iff]:
  "refines
     (R23  (m2_inv3a_sesK_compr) × (m3_inv1_lkeysec))
     med32 m2 m3"
proof -
  have "R23  m2_inv3a_sesK_compr × UNIV  UNIV × m3_inv7a_sesK_compr"
    by (auto simp add: R23_def R23_keys_simps intro!: m3_inv7a_sesK_comprI)
  thus ?thesis
    by (-) (rule Refinement_using_invariants, auto)
qed

lemma m3_implements_m2 [iff]:
  "implements med32 m2 m3"
by (rule refinement_soundness) (auto)


subsection ‹Inherited invariants›
(******************************************************************************)

subsubsection ‹inv3 (derived): Key secrecy for initiator›
(*invh*************************************************************************)

definition
  m3_inv3_ikk_init :: "m3_state set"
where
  "m3_inv3_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 
     Key K  analz (IK s) 
       (K, A, B, Ra$na, Ts)  leak s
  }"

lemmas m3_inv3_ikk_initI = m3_inv3_ikk_init_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv3_ikk_initE [elim] = m3_inv3_ikk_init_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv3_ikk_initD = m3_inv3_ikk_init_def [THEN setc_def_to_dest, rule_format, rotated 1]

lemma PO_m3_inv3_ikk_init: "reach m3  m3_inv3_ikk_init"
proof (rule INV_from_Refinement_using_invariants [OF m3_refines_m2])
  show "Range (R23  m2_inv3a_sesK_compr × m3_inv1_lkeysec  m2_inv6_ikk_init × UNIV)
       m3_inv3_ikk_init"
    by (fastforce simp add: R23_def R23_keys_simps intro!: m3_inv3_ikk_initI)
qed auto


subsubsection ‹inv4 (derived): Key secrecy for responder›
(*invh*************************************************************************)

definition
  m3_inv4_ikk_resp :: "m3_state set"
where
  "m3_inv4_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 
     Key K  analz (IK s) 
       (Na. (K, A, B, Na, Ts)  leak s)
  }"

lemmas m3_inv4_ikk_respI = m3_inv4_ikk_resp_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv4_ikk_respE [elim] = m3_inv4_ikk_resp_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv4_ikk_respD = m3_inv4_ikk_resp_def [THEN setc_def_to_dest, rule_format, rotated 1]

lemma PO_m3_inv4_ikk_resp: "reach m3  m3_inv4_ikk_resp"
proof (rule INV_from_Refinement_using_invariants [OF m3_refines_m2])
  show "Range (R23  m2_inv3a_sesK_compr × m3_inv1_lkeysec  m2_inv7_ikk_resp × UNIV)
       m3_inv4_ikk_resp"
    by (auto simp add: R23_def R23_keys_simps intro!: m3_inv4_ikk_respI)
       (elim m2_inv7_ikk_respE, auto)
qed auto


end