Theory m2_nssk

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

  Project: Development of Security Protocols by Refinement

  Module:  Key_establish/m2_nssk.thy (Isabelle/HOL 2016-1)
  ID:      $Id: m2_nssk.thy 133854 2017-03-20 17:53:50Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Key distribution protocols
  Second refinement: channel-protocol, parallel version of Needham-Schroeder
  Shared Key protocol (NSSK, Boyd/Mathuria, Protocol 3.19)

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

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

section ‹Abstract Needham-Schroeder Shared Key (L2)›

theory m2_nssk imports m1_nssk "../Refinement/Channels"
begin

text ‹
We model an abstract version of the Needham-Schroeder Shared Key protocol:
\[
\begin{array}{lll}
  \mathrm{M1.} & A \rightarrow S: & A, B, Na \\ 
  \mathrm{M2.} & S \rightarrow A: & \{Na, B, Kab, \{Kab, A\}_{Kbs} \}_{Kas} \\
  \mathrm{M3.} & A \rightarrow B: & \{A, Kab\}_{Kbs} \\
  \mathrm{M4.} & B \rightarrow A: & \{Nb\}_{Kab} \\  
  \mathrm{M5.} & A \rightarrow B: & \{Nb - 1 \}_{Kab} \\
\end{array}
\]
The last two message are supposed to authenticate $A$ to $B$, but this fails
as shown by Dening and Sacco.  Therefore and since we are mainly interested
in secrecy at this point, we drop the last two message from this development.

This refinement introduces channels with security properties.  We model 
a parallel/"channel-pure" version of the first three messages of the NSSK 
protocol:
\[
\begin{array}{lll}
  \mathrm{M1.} & A \rightarrow S: & A, B, Na \\ 
  \mathrm{M2.} & S \rightarrow A: & \{Na, B, Kab\}_{Kas} \\
  \mathrm{M3.} & S \rightarrow B: & \{Kab, A\}_{Kbs} \\
\end{array}
\]
Message 1 is sent over an insecure channel, the other two message over
secure channels to/from the server.
›

declare domIff [simp, iff del]


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

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

type_synonym
  m2_obs = "m1_state"

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

type_synonym
  m2_pred = "m2_state set"

type_synonym
  m2_trans = "(m2_state × m2_state) set"


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

text ‹Protocol events.›

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

    ― ‹guards:›
    Ra ∉ dom (runs s) ∧                      ― ‹fresh run identifier›
    Na = Ra$na ∧                             ― ‹generate nonce ‹Na››

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

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

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

    Insec A B (Msg [aNon Na]) ∈ chan s ∧          ― ‹recv msg 1›

    ― ‹actions:›
    ― ‹record key and send messages 2 and 3›
    ― ‹note that last field in server record is for responder nonce›
    s1 = s⦇
      runs := (runs s)(Rs ↦ (Serv, [A, B], [aNon Na])), 
      chan := {Secure Sv A (Msg [aNon Na, aAgt B, aKey Kab]), 
               Secure Sv B (Msg [aKey Kab, aAgt A])} ∪ chan s
    ⦈
  }"

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

    ― ‹guards:›
    runs s Ra = Some (Init, [A, B], []) ∧ 
    Na = Ra$na ∧

    Secure Sv A (Msg [aNon Na, aAgt B, aKey Kab]) ∈ chan s ∧  ― ‹recv msg 2›

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

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

    ― ‹guards:›
    runs s Rb = Some (Resp, [A, B], []) ∧
    Nb = Rb$nb ∧

    Secure Sv B (Msg [aKey Kab, aAgt A]) ∈ chan s ∧     ― ‹recv msg 3›

    ― ‹actions:›
    ― ‹record session key›
    s1 = s⦇
      runs := (runs s)(Rb ↦ (Resp, [A, B], [aKey Kab])), 
      chan := insert (dAuth Kab (Msg [aNon Nb])) (chan s)
    ⦈
  }"

definition     ― ‹by @{term "A"}, refines @{term m1_step6}›
  m2_step6 :: "[rid_t, agent, agent, nonce, nonce, key] ⇒ m2_trans"
where
  "m2_step6 Ra A B Na Nb Kab ≡ {(s, s'). 
    runs s Ra = Some (Init, [A, B], [aKey Kab]) ∧    ― ‹key recv'd before›
    Na = Ra$na ∧

    dAuth Kab (Msg [aNon Nb]) ∈ chan s ∧             ― ‹receive ‹M4››

    ― ‹actions:›
    s' = s⦇
      runs := (runs s)(Ra ↦ (Init, [A, B], [aKey Kab, aNon Nb])),
      chan := insert (dAuth Kab (Msg [aNon Nb, aNon Nb])) (chan s)
    ⦈
  }"

definition     ― ‹by @{term "B"}, refines @{term m1_step6}›
  m2_step7 :: "[rid_t, agent, agent, nonce, key] ⇒ m2_trans"
where
  "m2_step7 Rb A B Nb Kab ≡ {(s, s').
    runs s Rb = Some (Resp, [A, B], [aKey Kab]) ∧     ― ‹key recv'd before›
    Nb = Rb$nb ∧

    dAuth Kab (Msg [aNon Nb, aNon Nb]) ∈ chan s ∧     ― ‹receive ‹M5››

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


text ‹Intruder fake event.›

definition     ― ‹refines @{term m1_leak}›
  m2_leak :: "[rid_t, rid_t, rid_t, agent, agent] ⇒ m2_trans" 
where
  "m2_leak Rs Ra Rb A B ≡ {(s, s1).
    ― ‹guards:›
    runs s Rs = Some (Serv, [A, B], [aNon (Ra$na)]) ∧
    runs s Ra = Some (Init, [A, B], [aKey (sesK (Rs$sk)), aNon (Rb$nb)]) ∧  
    runs s Rb = Some (Resp, [A, B], [aKey (sesK (Rs$sk)), END]) ∧  

    ― ‹actions:›
    s1 = s⦇ leak := insert (sesK (Rs$sk), Ra$na, Rb$nb) (leak s), 
            chan := insert (Insec undefined undefined (Msg [aKey (sesK (Rs$sk))])) (chan s) ⦈
  }"

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

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


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

definition 
  m2_init :: "m2_pred"
where
  "m2_init ≡ { ⦇ 
     runs = Map.empty, 
     leak = corrKey × {undefined} × {undefined}, 
     chan = {} ⦈ 
  }"

definition 
  m2_trans :: "m2_trans" where
  "m2_trans ≡ (⋃A B Ra Rb Rs Na Nb Kab.
     m2_step1 Ra A B Na ∪
     m2_step2 Rb A B ∪
     m2_step3 Rs A B Na Kab ∪
     m2_step4 Ra A B Na Kab ∪
     m2_step5 Rb A B Nb Kab ∪
     m2_step6 Ra A B Na Nb Kab ∪
     m2_step7 Rb A B Nb Kab ∪
     m2_leak Rs Ra Rb A B ∪
     m2_fake ∪
     Id
  )"

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

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

lemmas m2_defs = m2_loc_defs m1_defs


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

subsubsection ‹inv1: Key definedness›
(*inv**************************************************************************)

text ‹All session keys in channel messages stem from existing runs.›

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

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


text ‹Invariance proof.›

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

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

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


subsubsection ‹inv2: Definedness of used keys›
(*inv**************************************************************************)

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

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

text ‹Invariance proof.›

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

lemma PO_m2_inv2_keys_for_trans [iff]:
  "{m2_inv2_keys_for ∩ m2_inv1_keys} trans m2 {> m2_inv2_keys_for}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv2_keys_forI)
apply (auto dest!: m2_inv2_keys_forD dest: m2_inv1_keysD dest: dom_lemmas)
― ‹2 subgoals, from step 4 and fake›
apply (rename_tac R xa xb xc xe)
apply (subgoal_tac "aKey (sesK (R$sk)) ∈ atoms (chan xa)", 
       auto dest!: m2_inv1_keysD dest: dom_lemmas)
apply (auto simp add: keys_for_def, erule fake.cases, fastforce+) 
done

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


text ‹Useful application of invariant.›

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


subsubsection ‹inv2b: leaked keys include corrupted ones›
(*inv**************************************************************************)

definition 
  m2_inv2b_corrKey_leaked :: "m2_pred"
where 
  "m2_inv2b_corrKey_leaked ≡ {s. ∀K.
     K ∈ corrKey ⟶ K ∈ Domain (leak s)
  }"

lemmas m2_inv2b_corrKey_leakedI = m2_inv2b_corrKey_leaked_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv2b_corrKey_leakedE [elim] = m2_inv2b_corrKey_leaked_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv2b_corrKey_leakedD = m2_inv2b_corrKey_leaked_def [THEN setc_def_to_dest, rule_format, rotated 1]

text ‹Invariance proof.›

lemma PO_m2_inv2b_corrKey_leaked_init [iff]:
  "init m2 ⊆ m2_inv2b_corrKey_leaked"
by (auto simp add: m2_defs intro!: m2_inv2b_corrKey_leakedI)

lemma PO_m2_inv2b_corrKey_leaked_trans [iff]:
  "{m2_inv2b_corrKey_leaked ∩ m2_inv1_keys} trans m2 {> m2_inv2b_corrKey_leaked}"
by (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv2b_corrKey_leakedI)

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


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

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

definition 
  m2_inv3a_sesK_compr :: "m2_state set"
where 
  "m2_inv3a_sesK_compr ≡ {s. ∀K KK.
     ⌦‹KK ⊆ range sesK ⟶›
     aKey K ∈ extr (aKey`KK ∪ ik0) (chan s) ⟷ (K ∈ KK ∨ aKey K ∈ extr ik0 (chan s)) 
  }"

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

text ‹Additional lemma to get the keys in front›
lemmas insert_commute_aKey = insert_commute [where x="aKey K" for K] 

lemmas m2_inv3a_sesK_compr_simps = 
  m2_inv3a_sesK_comprD
  m2_inv3a_sesK_comprD [where KK="{Kab}" for Kab, simplified]
  m2_inv3a_sesK_comprD [where KK="insert Kab KK" for Kab KK, simplified]
  insert_commute_aKey 

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

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

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


subsubsection ‹inv3b: Session key compromise for nonces›
(*inv**************************************************************************)

text ‹A variant of the above for nonces. Roughly, it states that adding 
a set of keys @{term KK} to the parameter ‹T› of @{term extr} 
does not help the intruder to extract more nonces than those extractable 
without adding @{term KK}.

NOTE: This lemma is only needed at the next refinement level.
›

definition 
  m2_inv3b_sesK_compr_non :: "m2_state set"
where 
  "m2_inv3b_sesK_compr_non ≡ {s. ∀N KK.
     ⌦‹KK ⊆ range sesK ⟶›
     aNon N ∈ extr (aKey`KK ∪ ik0) (chan s) ⟷ aNon N ∈ extr ik0 (chan s)
  }"

lemmas m2_inv3b_sesK_compr_nonI = m2_inv3b_sesK_compr_non_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv3b_sesK_compr_nonE [elim] = m2_inv3b_sesK_compr_non_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv3b_sesK_compr_nonD = m2_inv3b_sesK_compr_non_def [THEN setc_def_to_dest, rule_format]

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

lemma PO_m2_inv3b_sesK_compr_non_init [iff]:
  "init m2 ⊆ m2_inv3b_sesK_compr_non"
by (auto simp add: m2_defs intro!: m2_inv3b_sesK_compr_nonI)

(* with dSecure instead of dAuth in step5:

lemma PO_m2_inv3b_sesK_compr_non_trans [iff]:
  "{m2_inv3b_sesK_compr_non ∩ m2_inv3a_sesK_compr} 
     m2_step5 Rb A B Nb Kab 
   {> m2_inv3b_sesK_compr_non}"
apply (auto simp add: PO_hoare_defs m2_defs m2_inv3b_sesK_compr_non_simps 
                      m2_inv3a_sesK_compr_simps
         intro!: m2_inv3b_sesK_compr_nonI)
(* 1 subgoal, unsolvable! *)
oops
*)

lemma PO_m2_inv3b_sesK_compr_non_trans [iff]:
  "{m2_inv3b_sesK_compr_non} trans m2 {> m2_inv3b_sesK_compr_non}"
by (auto simp add: PO_hoare_defs m2_defs m2_inv3b_sesK_compr_non_simps 
         intro!: m2_inv3b_sesK_compr_nonI)

lemma PO_m2_inv3b_sesK_compr_non [iff]: "reach m2 ⊆ m2_inv3b_sesK_compr_non"
by (rule inv_rule_basic) (auto) 


subsubsection ‹inv3: Lost session keys›
(*inv**************************************************************************)

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

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

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

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

lemma PO_m2_inv3_extrKey_trans [iff]:
  "{m2_inv3_extrKey ∩ m2_inv3a_sesK_compr} trans m2 {> m2_inv3_extrKey}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv3_extrKeyI)
apply (auto simp add: m2_inv3a_sesK_compr_simps dest: dom_lemmas)
― ‹11 subgoals, sledgehammer›
apply (metis m2_inv3_extrKeyD map_definedness_contra)
apply (metis m2_inv3_extrKeyD map_definedness_contra)
apply (metis m2_inv3_extrKeyD)
apply (metis m2_inv3_extrKeyD)
apply (metis m2_inv3_extrKeyD)
apply (metis m2_inv3_extrKeyD map_definedness_contra)
apply (metis m2_inv3_extrKeyD not_Cons_self2 prod.inject option.inject)
apply (metis m2_inv3_extrKeyD not_Cons_self2 prod.inject option.inject)
apply (metis m2_inv3_extrKeyD atom.distinct(7) list.inject option.inject prod.inject)
apply (metis m2_inv3_extrKeyD atom.distinct(7) list.inject option.inject prod.inject)
apply (metis m2_inv3_extrKeyD)
done
(*
apply (aut dest!: m2_inv3_extrKeyD dest: dom_lemmas)        -- {*SLOW*}
-- {* 18 subgoals; go agressive*}
apply (aut intro!: exI dest: dom_lemmas)
done
*)

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


subsubsection ‹inv4: Secure channel and message 2›
(*inv**************************************************************************)

text ‹inv4: Secure messages to honest agents and server state; one variant 
for each of M2 and M3. Note that the one for M2 is stronger than the 
one for M3.›

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

lemmas m2_inv4_M2I = m2_inv4_M2_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv4_M2E [elim] = m2_inv4_M2_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv4_M2D = m2_inv4_M2_def [THEN setc_def_to_dest, rule_format, rotated 1]

text ‹Invariance proof.›

lemma PO_m2_inv4_M2_init [iff]:
  "init m2 ⊆ m2_inv4_M2"
by (auto simp add: m2_defs intro!: m2_inv4_M2I)

lemma PO_m2_inv4_M2_trans [iff]:
  "{m2_inv4_M2} trans m2 {> m2_inv4_M2}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv4_M2I)
apply (auto dest!: m2_inv4_M2D dest: dom_lemmas)
― ‹5 subgoals›
apply (force dest!: spec)
apply (force dest!: spec)
apply (force dest!: spec)
apply (rule exI, auto)+
done

lemma PO_m2_inv4_M2 [iff]: "reach m2 ⊆ m2_inv4_M2"
by (rule inv_rule_basic) (auto)


subsubsection ‹inv4b: Secure channel and message 3›
(*inv**************************************************************************)

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

lemmas m2_inv4_M3I = m2_inv4_M3_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv4_M3E [elim] = m2_inv4_M3_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv4_M3D = m2_inv4_M3_def [THEN setc_def_to_dest, rule_format, rotated 1]

text ‹Invariance proof.›

lemma PO_m2_inv4_M3_init [iff]:
  "init m2 ⊆ m2_inv4_M3"
by (auto simp add: m2_defs intro!: m2_inv4_M3I)

lemma PO_m2_inv4_M3_trans [iff]:
  "{m2_inv4_M3} trans m2 {> m2_inv4_M3}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv4_M3I) 
apply (auto dest!: m2_inv4_M3D dest: dom_lemmas)
― ‹5 subgoals›
apply (force)+
done

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


text ‹Consequence needed in proof of inv8/step5›

lemma m2_inv4_M2_M3_unique_names:
assumes 
  "Secure Sv A' (Msg [aNon Na, aAgt B', aKey Kab]) ∈ chan s" 
  "Secure Sv B  (Msg [aKey Kab, aAgt A]) ∈ chan s" "aKey Kab ∉ extr ik0 (chan s)" 
  "s ∈ m2_inv4_M2" "s ∈ m2_inv4_M3"
shows 
  "A = A' ∧ B = B'"
proof (cases "A' ∈ bad ∨ B ∈ bad")
  case True thus ?thesis using assms(1-3) by auto
next
  case False thus ?thesis using assms(1,2,4,5) by (auto dest!: m2_inv4_M2D m2_inv4_M3D)
qed


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

lemma m2_inv34_M2_authorized:
  assumes "Secure Sv A (Msg [aNon N, aAgt B, aKey K]) ∈ chan s" 
          "s ∈ m2_inv4_M2" "s ∈ m2_inv3_extrKey" "s ∈ m2_inv2b_corrKey_leaked" 
          "K ∉ Domain (leak s)" 
  shows   "(K, A) ∈ azC (runs s)"
proof (cases)
  assume "A ∈ bad" 
  hence "aKey K ∈ extr ik0 (chan s)" using assms(1) by auto
  thus ?thesis using assms(3-) by auto 
next
  assume "A ∉ bad" 
  thus ?thesis using assms(1-2) by (auto dest: m2_inv4_M2D) 
qed

lemma m2_inv34_M3_authorized:
  assumes "Secure Sv B (Msg [aKey K, aAgt A]) ∈ chan s" 
          "s ∈ m2_inv4_M3" "s ∈ m2_inv3_extrKey" "s ∈ m2_inv2b_corrKey_leaked" 
          "K ∉ Domain (leak s)" 
  shows  "(K, B) ∈ azC (runs s)"
proof (cases)
  assume "B ∈ bad" 
  hence "aKey K ∈ extr ik0 (chan s)" using assms(1) by auto
  thus ?thesis using assms(3-) by auto 
next
  assume "B ∉ bad"
  thus ?thesis using assms(1-2) by (auto dest: m2_inv4_M3D) 
qed


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

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

definition 
  m2_inv5_ikk_sv :: "m2_pred"
where
  "m2_inv5_ikk_sv ≡ {s. ∀Rs A B Na al.
     runs s Rs = Some (Serv, [A, B], aNon Na # al) ⟶ A ∈ good ⟶ B ∈ good ⟶
     aKey (sesK (Rs$sk)) ∈ extr ik0 (chan s) ⟶
       (∃Nb'. (sesK (Rs$sk), Na, Nb') ∈ leak s)
  }"

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


text ‹Invariance proof. This invariant follows from ‹m2_inv3_extrKey›.›

lemma m2_inv5_ikk_sv_derived: 
  "s ∈ m2_inv3_extrKey ⟹ s ∈ m2_inv5_ikk_sv"
by (auto simp add: m2_inv3_extrKey_def m2_inv5_ikk_sv_def) (force)

lemma PO_m2_inv5_ikk_sv [iff]: "reach m2 ⊆ m2_inv5_ikk_sv"
proof -
  have "reach m2 ⊆ m2_inv3_extrKey" by blast
  also have "... ⊆ m2_inv5_ikk_sv" by (blast intro: m2_inv5_ikk_sv_derived)
  finally show ?thesis .
qed

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

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

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


subsubsection ‹inv6 (derived): Key secrecy for initiator›
(*invd**************************************************************************)

text ‹This invariant is derivable (see below).›

definition 
  m2_inv6_ikk_init :: "m2_pred"
where
  "m2_inv6_ikk_init ≡ {s. ∀Ra K A B al.
     runs s Ra = Some (Init, [A, B], aKey K # al) ⟶ A ∈ good ⟶ B ∈ good ⟶
     aKey K ∈ extr ik0 (chan s) ⟶
       (∃Nb'. (K, Ra $ na, Nb') ∈ leak s)     
  }"

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


subsubsection ‹inv7 (derived): Key secrecy for responder›
(*invd**************************************************************************)

text ‹This invariant is derivable (see below).›

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

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


subsubsection ‹inv8: Relating M2 and M4 to the responder state›
(*inv**************************************************************************)

text ‹This invariant relates messages M2 and M4 to the responder's state. 
It is required in the refinement of step 6 to prove that the initiator 
agrees with the responder on (A, B, Nb, Kab).›

definition
  m2_inv8_M4 :: "m2_pred"
where
  "m2_inv8_M4 ≡ {s. ∀Kab A B Na Nb.
     Secure Sv A (Msg [aNon Na, aAgt B, aKey Kab]) ∈ chan s ⟶
     dAuth Kab (Msg [aNon Nb]) ∈ chan s ⟶  
     aKey Kab ∉ extr ik0 (chan s) ⟶
       (∃Rb. Nb = Rb$nb ∧ (∃al. runs s Rb = Some (Resp, [A, B], aKey Kab # al)))
  }"

(* original open subgoal in refinement proof for step6:

1. ⋀s t. ⟦runs s = runs t; runs t Ra = Some (Init, [A, B], [aKey Kab]);
           dAuth Kab (Msg [aNon Nb]) ∈ chan t; A ∉ bad; B ∉ bad⟧
          ⟹ ∃Rb nl. Nb = Rb $ nb ∧ runs t Rb = Some (Resp, [A, B], aKey Kab # nl)
*)

lemmas m2_inv8_M4I = m2_inv8_M4_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv8_M4E [elim] = m2_inv8_M4_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv8_M4D = m2_inv8_M4_def [THEN setc_def_to_dest, rule_format, rotated 1]


text ‹Invariance proof.›

lemma PO_m2_inv8_M4_step1:
  "{m2_inv8_M4} m2_step1 Ra A B Na {> m2_inv8_M4}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv8_M4I)
apply (auto dest!: m2_inv8_M4D dest: dom_lemmas)
done

lemma PO_m2_inv8_M4_step2:
  "{m2_inv8_M4} m2_step2 Rb A B {> m2_inv8_M4}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv8_M4I)
apply (auto dest!: m2_inv8_M4D dest: dom_lemmas)
done

lemma PO_m2_inv8_M4_step3:
  "{m2_inv8_M4 ∩ m2_inv2_keys_for} m2_step3 Rs A B Na Kab {> m2_inv8_M4}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv8_M4I)
apply (auto simp add: m2_inv2_keys_for__extr_insert_key dest!: m2_inv8_M4D dest: dom_lemmas)
done

lemma PO_m2_inv8_M4_step4:
  "{m2_inv8_M4} m2_step4 Ra A B Na Kab {> m2_inv8_M4}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv8_M4I)
― ‹1 subgoal›
apply (drule m2_inv8_M4D, auto) 
apply (rule exI, auto)
done

lemma PO_m2_inv8_M4_step5:
  "{m2_inv8_M4 ∩ m2_inv4_M3 ∩ m2_inv4_M2} 
      m2_step5 Rb A B Nb Kab 
   {> m2_inv8_M4}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv8_M4I)
apply (auto dest: m2_inv4_M2_M3_unique_names)
apply (auto dest!: m2_inv8_M4D)
done

lemma PO_m2_inv8_M4_step6:
  "{m2_inv8_M4} m2_step6 Ra A B Na Nb Kab {> m2_inv8_M4}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv8_M4I)
apply (auto dest!: m2_inv8_M4D)
― ‹1 subgoal›
apply (rule exI, auto)
done

lemma PO_m2_inv8_M4_step7:
  "{m2_inv8_M4} m2_step7 Rb A B Nb Kab {> m2_inv8_M4}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv8_M4I)
apply (auto dest!: m2_inv8_M4D)
done

lemma PO_m2_inv8_M4_leak:
  "{m2_inv8_M4 ∩ m2_inv3a_sesK_compr} m2_leak Rs Ra Rb A B {> m2_inv8_M4}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv8_M4I)
apply (auto simp add: m2_inv3a_sesK_compr_simps dest!: m2_inv8_M4D)
done

lemma PO_m2_inv8_M4_fake:
  "{m2_inv8_M4} m2_fake {> m2_inv8_M4}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv8_M4I)
― ‹1 subgoal›
apply (erule fake.cases, auto dest!: m2_inv8_M4D)
done

text ‹All together now..›

lemmas PO_m2_inv8_M4_lemmas = 
  PO_m2_inv8_M4_step1 PO_m2_inv8_M4_step2 PO_m2_inv8_M4_step3
  PO_m2_inv8_M4_step4 PO_m2_inv8_M4_step5 PO_m2_inv8_M4_step6
  PO_m2_inv8_M4_step7 PO_m2_inv8_M4_leak PO_m2_inv8_M4_fake

lemma PO_m2_inv8_M4_init [iff]:
  "init m2 ⊆ m2_inv8_M4"
by (auto simp add: m2_defs intro!: m2_inv8_M4I)

lemma PO_m2_inv8_M4_trans [iff]:
  "{m2_inv8_M4 ∩ m2_inv4_M3 ∩ m2_inv4_M2 ∩ m2_inv3a_sesK_compr ∩ m2_inv2_keys_for} 
      trans m2 
   {> m2_inv8_M4}"
by (auto simp add: m2_def m2_trans_def intro!: PO_m2_inv8_M4_lemmas)

lemma PO_m2_inv8_M4 [iff]: "reach m2 ⊆ m2_inv8_M4"
by (rule_tac J="m2_inv4_M3 ∩ m2_inv4_M2 ∩  m2_inv3a_sesK_compr ∩ m2_inv2_keys_for" in inv_rule_incr) 
   (auto)


subsubsection ‹inv8a: Relating the initiator state to M2›
(*inv**************************************************************************)

definition
  m2_inv8a_init_M2 :: "m2_pred"
where
  "m2_inv8a_init_M2 ≡ {s. ∀Ra A B Kab al.
     runs s Ra = Some (Init, [A, B], aKey Kab # al) ⟶
       Secure Sv A (Msg [aNon (Ra$na), aAgt B, aKey Kab]) ∈ chan s
  }"

lemmas m2_inv8a_init_M2I = m2_inv8a_init_M2_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv8a_init_M2E [elim] = m2_inv8a_init_M2_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv8a_init_M2D = m2_inv8a_init_M2_def [THEN setc_def_to_dest, rule_format, rotated 1]


text ‹Invariance proof.›

lemma PO_m2_inv8a_init_M2_init [iff]:
  "init m2 ⊆ m2_inv8a_init_M2"
by (auto simp add: m2_defs intro!: m2_inv8a_init_M2I)

lemma PO_m2_inv8a_init_M2_trans [iff]:
  "{m2_inv8a_init_M2}  
      trans m2 
   {> m2_inv8a_init_M2}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv8a_init_M2I) 
apply (blast)
done 

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


subsubsection ‹inv9a: Relating the responder state to M3›
(*inv**************************************************************************)

definition
  m2_inv9a_resp_M3 :: "m2_pred"
where
  "m2_inv9a_resp_M3 ≡ {s. ∀Rb A B Kab al.
     runs s Rb = Some (Resp, [A, B], aKey Kab # al) ⟶
       Secure Sv B (Msg [aKey Kab, aAgt A]) ∈ chan s
  }"

lemmas m2_inv9a_resp_M3I = m2_inv9a_resp_M3_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv9a_resp_M3E [elim] = m2_inv9a_resp_M3_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv9a_resp_M3D = m2_inv9a_resp_M3_def [THEN setc_def_to_dest, rule_format, rotated 1]


text ‹Invariance proof.›

lemma PO_m2_inv9a_resp_M3_init [iff]:
  "init m2 ⊆ m2_inv9a_resp_M3"
by (auto simp add: m2_defs intro!: m2_inv9a_resp_M3I)

lemma PO_m2_inv9a_resp_M3_trans [iff]:
  "{m2_inv9a_resp_M3}  
      trans m2 
   {> m2_inv9a_resp_M3}"
by (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9a_resp_M3I dest: m2_inv9a_resp_M3D) 
   (blast)

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


subsubsection ‹inv9: Relating M3 and M5 to the initiator state›
(*inv**************************************************************************)

text ‹This invariant relates message M5 to the initiator's state. It is 
required in step 7 of the refinement to prove that the initiator agrees with 
the responder on (A, B, Nb, Kab).›

definition
  m2_inv9_M5 :: "m2_pred"
where
  "m2_inv9_M5 ≡ {s. ∀Kab A B Nb.
     Secure Sv B (Msg [aKey Kab, aAgt A]) ∈ chan s ⟶
     dAuth Kab (Msg [aNon Nb, aNon Nb]) ∈ chan s ⟶ 
     aKey Kab ∉ extr ik0 (chan s) ⟶
       (∃Ra. runs s Ra = Some (Init, [A, B], [aKey Kab, aNon Nb]))
  }"

(* 
 original subgoal in refinement of step 7:

 1. ⋀s t. ⟦runs s = runs t; runs t Rb = Some (Resp, [A, B], [aKey Kab]);
           dAuth Kab (Msg [Rb$nb, Rb$nb]) ∈ chan t; A ∉ bad; B ∉ bad⟧
          ⟹ ∃Ra. runs t Ra = Some (Init, [A, B], [aKey Kab, aNon Nb])
*)

lemmas m2_inv9_M5I = m2_inv9_M5_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv9_M5E [elim] = m2_inv9_M5_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv9_M5D = m2_inv9_M5_def [THEN setc_def_to_dest, rule_format, rotated 1]


text ‹Invariance proof.›

lemma PO_m2_inv9_M5_step1:
  "{m2_inv9_M5} m2_step1 Ra A B Na {> m2_inv9_M5}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9_M5I)
apply (auto dest!: m2_inv9_M5D dest: dom_lemmas)
done

lemma PO_m2_inv9_M5_step2:
  "{m2_inv9_M5} m2_step2 Rb A B {> m2_inv9_M5}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9_M5I)
apply (auto dest!: m2_inv9_M5D dest: dom_lemmas)
done

lemma PO_m2_inv9_M5_step3:
  "{m2_inv9_M5 ∩ m2_inv2_keys_for} m2_step3 Rs A B Na Kab {> m2_inv9_M5}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9_M5I)
apply (auto simp add: m2_inv2_keys_for__extr_insert_key dest!: m2_inv9_M5D dest: dom_lemmas)
done

lemma PO_m2_inv9_M5_step4:
  "{m2_inv9_M5} m2_step4 Ra A B Na Kab {> m2_inv9_M5}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9_M5I)
apply (auto dest!: m2_inv9_M5D dest: dom_lemmas)
― ‹1 subgoal›
apply (rule exI, auto)
done

lemma PO_m2_inv9_M5_step5:
  "{m2_inv9_M5} m2_step5 Rb A B Nb Kab {> m2_inv9_M5}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9_M5I)
― ‹1 subgoal›
apply (drule m2_inv9_M5D, fast, fast, fast, clarsimp)
apply (rule exI, auto)
done

lemma PO_m2_inv9_M5_step6:
  "{m2_inv9_M5 ∩ m2_inv8a_init_M2 ∩ m2_inv9a_resp_M3 ∩ m2_inv4_M2 ∩ m2_inv4_M3}
     m2_step6 Ra A B Na Nb Kab 
   {> m2_inv9_M5}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9_M5I)
― ‹2 subgoals›
defer 1
  apply (drule m2_inv9_M5D, fast, fast, fast, clarsimp)
  apply (rename_tac Raa, rule_tac x=Raa in exI, auto)

  apply (auto dest!: m2_inv8a_init_M2D m2_inv9a_resp_M3D m2_inv4_M2_M3_unique_names)
done

lemma PO_m2_inv9_M5_step7:
  "{m2_inv9_M5} m2_step7 Rb A B Nb Kab {> m2_inv9_M5}"
apply (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9_M5I)
― ‹1 subgoal›
apply (drule m2_inv9_M5D, fast, fast, fast, clarsimp)
apply (rule exI, auto)
done

lemma PO_m2_inv9_M5_leak:
  "{m2_inv9_M5 ∩ m2_inv3a_sesK_compr} m2_leak Rs Ra Rb A B {> m2_inv9_M5}"
by (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9_M5I)
   (auto simp add: m2_inv3a_sesK_compr_simps dest!: m2_inv9_M5D)

lemma PO_m2_inv9_M5_fake:
  "{m2_inv9_M5} m2_fake {> m2_inv9_M5}"
by (auto simp add: PO_hoare_defs m2_defs intro!: m2_inv9_M5I)
   (auto dest!: m2_inv9_M5D)


text ‹All together now.›

lemmas PO_m2_inv9_M5_lemmas = 
  PO_m2_inv9_M5_step1 PO_m2_inv9_M5_step2 PO_m2_inv9_M5_step3
  PO_m2_inv9_M5_step4 PO_m2_inv9_M5_step5 PO_m2_inv9_M5_step6
  PO_m2_inv9_M5_step7 PO_m2_inv9_M5_leak PO_m2_inv9_M5_fake

lemma PO_m2_inv9_M5_init [iff]:
  "init m2 ⊆ m2_inv9_M5"
by (auto simp add: m2_defs intro!: m2_inv9_M5I)

lemma PO_m2_inv9_M5_trans [iff]:
  "{m2_inv9_M5 ∩ m2_inv8a_init_M2 ∩ m2_inv9a_resp_M3 ∩ 
    m2_inv4_M2 ∩ m2_inv4_M3 ∩ m2_inv3a_sesK_compr ∩ m2_inv2_keys_for} 
      trans m2 
   {> m2_inv9_M5}"
by (auto simp add: m2_def m2_trans_def intro!: PO_m2_inv9_M5_lemmas)

lemma PO_m2_inv9_M5 [iff]: "reach m2 ⊆ m2_inv9_M5"
by (rule_tac J="m2_inv8a_init_M2 ∩ m2_inv9a_resp_M3 ∩ 
                m2_inv4_M2 ∩ m2_inv4_M3 ∩ m2_inv3a_sesK_compr ∩ m2_inv2_keys_for" 
    in inv_rule_incr) 
   (auto simp add: Int_assoc del: subsetI)


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

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

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

text ‹The mediator function projects on the local states.›

definition 
  med21 :: "m2_obs ⇒ m1_obs" where
  "med21 o2 = ⦇ runs = runs o2, leak = leak o2 ⦈"


text ‹Refinement proof.›

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

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

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

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

lemma PO_m2_step5_refines_m1_step5:
  "{R12 ∩ UNIV × (m2_inv4_M3 ∩ m2_inv3_extrKey ∩ m2_inv2b_corrKey_leaked)} 
     (m1_step5 Rb A B Nb Kab), (m2_step5 Rb A B Nb Kab) 
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, simp_all)
   (auto dest: m2_inv34_M3_authorized)

lemma PO_m2_step6_refines_m1_step6:
  "{R12 ∩ UNIV × (m2_inv8a_init_M2 ∩ m2_inv8_M4 ∩ m2_inv6_ikk_init)} 
     (m1_step6 Ra A B Na Nb Kab), (m2_step6 Ra A B Na Nb Kab) 
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, auto)
   (auto intro!: m2_inv8_M4D [OF m2_inv8a_init_M2D] dest: m2_inv6_ikk_initD) 

lemma PO_m2_step7_refines_m1_step7:
  "{R12 ∩ UNIV × (m2_inv9_M5 ∩ m2_inv9a_resp_M3 ∩ m2_inv7_ikk_resp)} 
     (m1_step7 Rb A B Nb Kab), (m2_step7 Rb A B Nb Kab) 
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, auto)
   (auto intro!: m2_inv9_M5D [OF m2_inv9a_resp_M3D] dest: m2_inv7_ikk_respD) 

lemma PO_m2_leak_refines_leak:
  "{R12} 
     m1_leak Rs Ra Rb A B, m2_leak Rs Ra Rb A B
   {> R12}"
by (simp add: PO_rhoare_defs R12_def m2_defs, safe, auto)

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


text ‹Consequences of simulation relation and invariants.›

lemma m2_inv6_ikk_init_derived:
assumes "(s, t) ∈ R12" "s ∈ m1_inv2i_serv" "t ∈ m2_inv5_ikk_sv" 
shows "t ∈ m2_inv6_ikk_init"
proof -
  have "t ∈ m1_inv2i_serv" using assms(1,2) by (simp add: R12_def m1_inv2i_serv_def)
  thus ?thesis using assms(3) 
    by (auto simp add: m2_inv6_ikk_init_def dest: m1_inv2i_servD m2_inv5_ikk_svD)
qed

lemma m2_inv7_ikk_resp_derived:
assumes "(s, t) ∈ R12" "s ∈ m1_inv2r_serv" "t ∈ m2_inv5_ikk_sv" 
shows "t ∈ m2_inv7_ikk_resp"
proof -
  have "t ∈ m1_inv2r_serv" using assms(1,2) by (simp add: R12_def m1_inv2r_serv_def)
  thus ?thesis using assms(3) 
    by (auto simp add: m2_inv7_ikk_resp_def dest!: m1_inv2r_servD m2_inv5_ikk_svD)
qed


text ‹All together now...›

lemmas PO_m2_trans_refines_m1_trans = 
  PO_m2_step1_refines_m1_step1 PO_m2_step2_refines_m1_step2
  PO_m2_step3_refines_m1_step3 PO_m2_step4_refines_m1_step4
  PO_m2_step5_refines_m1_step5 PO_m2_step6_refines_m1_step6 
  PO_m2_step7_refines_m1_step7 PO_m2_leak_refines_leak 
  PO_m2_fake_refines_skip 

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

lemma PO_m2_refines_trans_m1 [iff]:
  "{R12 ∩ 
    (reach m1 × 
     (m2_inv9_M5 ∩ m2_inv8a_init_M2 ∩ m2_inv9a_resp_M3 ∩ m2_inv8_M4 ∩ 
      m2_inv4_M3 ∩ m2_inv4_M2 ∩ m2_inv3a_sesK_compr ∩ m2_inv3_extrKey ∩ m2_inv2b_corrKey_leaked))} 
     (trans m1), (trans m2) 
   {> R12}"
proof -
  ― ‹derive the key secrecy invariants from simulation relation and the other invariants›
  let ?pre' = "R12 ∩ (UNIV × (m2_inv9_M5 ∩ m2_inv8a_init_M2 ∩ m2_inv9a_resp_M3 ∩ 
               m2_inv8_M4 ∩ m2_inv7_ikk_resp ∩ m2_inv6_ikk_init ∩ m2_inv5_ikk_sv ∩ 
               m2_inv4_M3 ∩ m2_inv4_M2 ∩ m2_inv3a_sesK_compr ∩ m2_inv3_extrKey ∩ 
               m2_inv2b_corrKey_leaked))"
  show ?thesis (is "{?pre} ?t1, ?t2 {>?post}")
  proof (rule relhoare_conseq_left)
    show "?pre ⊆ ?pre'"
      by (auto intro: m2_inv6_ikk_init_derived m2_inv7_ikk_resp_derived m2_inv5_ikk_sv_derived)
  next 
    show "{?pre'} ?t1, ?t2 {> ?post}"
      by (auto simp add: m2_def m2_trans_def m1_def m1_trans_def)
         (blast intro!: PO_m2_trans_refines_m1_trans)+
  qed
qed    

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


text ‹Refinement result.›

lemma m2_refines_m1 [iff]:
  "refines 
     (R12 ∩ 
      (reach m1 × 
       (m2_inv9_M5 ∩ m2_inv8a_init_M2 ∩ m2_inv9a_resp_M3 ∩ m2_inv8_M4 ∩ 
        m2_inv4_M3 ∩ m2_inv4_M2 ∩ m2_inv3a_sesK_compr ∩ m2_inv3_extrKey ∩ 
        m2_inv2b_corrKey_leaked ∩ m2_inv2_keys_for ∩ m2_inv1_keys)))
     med21 m1 m2"
by (rule Refinement_using_invariants) (auto)

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


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

text ‹Show preservation of invariants @{term "m1_inv2i_serv"} and
@{term "m1_inv2r_serv"} from ‹m1›.›

(*invh*************************************************************************)

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

(*invh*************************************************************************)

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

text ‹Now we derive the additional invariants for the initiator and the responder 
(see above for the definitions).›

lemma PO_m2_inv6_init_ikk [iff]: "reach m2 ⊆ m2_inv6_ikk_init"
proof -
  have "reach m2 ⊆ m1_inv2i_serv ∩ m2_inv5_ikk_sv" by simp
  also have "... ⊆ m2_inv6_ikk_init" by (blast intro!: m2_inv6_ikk_initI dest: m2_inv5_ikk_svD)
  finally show ?thesis .
qed

lemma PO_m2_inv6_resp_ikk [iff]: "reach m2 ⊆ m2_inv7_ikk_resp"
proof -
  have "reach m2 ⊆ m1_inv2r_serv ∩ m2_inv5_ikk_sv" by simp
  also have "... ⊆ m2_inv7_ikk_resp" by (blast intro!: m2_inv7_ikk_respI dest: m2_inv5_ikk_svD)
  finally show ?thesis .
qed


end