Theory m3_nssk

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

  Project: Development of Security Protocols by Refinement

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

  Key distribution protocols
  Third refinement: Needham-Schroeder Shared Key protocol (NSSK)
  (Boyd/Mathuria, Protocol 3.19)

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

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

section ‹Needham-Schroeder Shared Key (L3)›

theory m3_nssk imports m2_nssk "../Refinement/Message"
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: & \{Kab, A\}_{Kbs} \\
  \mathrm{M4.} & B \rightarrow A: & \{Nb\}_{Kab} \\ 
  \mathrm{M5.} & A \rightarrow B: & \{Nb - 1 \}_{Kab} \\
\end{array}
\]
This refinement works with a single insecure channel and introduces the full
Dolev-Yao intruder.
›

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: agent's local state.›

type_synonym
  m3_obs = m2_obs

definition
  m3_obs :: "m3_state ⇒ m3_obs" where
  "m3_obs s ≡ ⦇ runs = runs s, leak = leak 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 ∧                             ― ‹generate nonce ‹Na››

    ― ‹actions:›
    s1 = s⦇
      runs := (runs s)(Ra ↦ (Init, [A, B], [])),
      IK := insert ⦃Agent A, Agent B, Nonce Na⦄ (IK s)    ― ‹send msg 1›
    ⦈
  }"

definition     ― ‹by @{term "B"}, refines @{term "m2_step2"}›
  m3_step2 :: "[rid_t, agent, agent] ⇒ m3_trans"
where
  "m3_step2 Rb A B ≡ {(s, s1).

    ― ‹guards:›
    Rb ∉ dom (runs s) ∧                       ― ‹‹Rb› is fresh›

    ― ‹actions:›
    ― ‹create responder thread›
    s1 = s⦇
      runs := (runs s)(Rb ↦ (Resp, [A, B], []))
    ⦈
  }"

definition     ― ‹by @{text "Server"}, refines @{term m2_step3}›
  m3_step3 :: "[rid_t, agent, agent, nonce, key] ⇒ m3_trans"
where
  "m3_step3 Rs A B Na Kab ≡ {(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 msg 1›

    ― ‹actions:›
    ― ‹record session 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])),
      IK := insert
              (Crypt (shrK A)
                ⦃Nonce Na, Agent B, Key Kab,
                   Crypt (shrK B) ⦃Key Kab, Agent A⦄⦄)
              (IK s)
    ⦈
  }"

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

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

    Crypt (shrK A) ⦃Nonce Na, Agent B, Key Kab, X⦄ ∈ IK s ∧  ― ‹recv msg 2›

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

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

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

    Crypt (shrK B) ⦃Key Kab, Agent A⦄ ∈ IK s ∧              ― ‹recv msg 3›

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

definition     ― ‹by @{term "A"}, refines @{term m2_step6}›
  m3_step6 :: "[rid_t, agent, agent, nonce, nonce, key] ⇒ m3_trans"
where
  "m3_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 ∧

    Crypt Kab (Nonce Nb) ∈ IK s ∧                      ― ‹receive ‹M4››

    ― ‹actions:›
    s' = s⦇
      runs := (runs s)(Ra ↦ (Init, [A, B], [aKey Kab, aNon Nb])),
      IK := insert (Crypt Kab ⦃Nonce Nb, Nonce Nb⦄) (IK s)
    ⦈
  }"

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

    Crypt Kab ⦃Nonce Nb, Nonce Nb⦄ ∈ IK s ∧         ― ‹receive ‹M5››

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


text ‹Session key compromise.›

definition     ― ‹refines @{term m2_leak}›
  m3_leak :: "[rid_t, rid_t, rid_t, agent, agent] ⇒ m3_trans"
where
  "m3_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:›
    ― ‹record session key as leaked and add it to intruder knowledge›
    s1 = s⦇ leak := insert (sesK (Rs$sk), Ra$na, Rb$nb) (leak s),
            IK := insert (Key (sesK (Rs$sk))) (IK s) ⦈
  }"

text ‹Intruder fake event.›

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

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


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

definition
  m3_init :: "m3_state set"
where
  "m3_init ≡ { ⦇
     runs = Map.empty,
     leak = shrK`bad × {undefined} × {undefined},
     IK = Key`shrK`bad
  ⦈ }"

definition
  m3_trans :: "(m3_state × m3_state) set" where
  "m3_trans ≡ (⋃Ra Rb Rs A B Na Nb Kab X.
     m3_step1 Ra A B Na ∪
     m3_step2 Rb A B ∪
     m3_step3 Rs A B Na Kab ∪
     m3_step4 Ra A B Na Kab X ∪
     m3_step5 Rb A B Nb Kab ∪
     m3_step6 Ra A B Na Nb Kab ∪
     m3_step7 Rb A B Nb Kab ∪
     m3_leak Rs Ra Rb A B ∪
     m3_DY_fake ∪
     Id
  )"

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

lemmas m3_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_step7_def m3_leak_def m3_DY_fake_def


(******************************************************************************)
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›
(*inv**************************************************************************)

text ‹inv1: Secrecy of long-term keys›

definition
  m3_inv1_lkeysec :: "m3_state set"
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_lkeysecD = 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 m3_inv1_lkeysec_def)

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 dest: Body)

lemma PO_m3_inv1_lkeysec [iff]: "reach m3 ⊆ m3_inv1_lkeysec"
by (rule inv_rule_incr) (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 ‹inv2: Ticket shape for honestly encrypted M2›
(*inv**************************************************************************)

definition
  m3_inv2_ticket :: "m3_state set"
where
  "m3_inv2_ticket ≡ {s. ∀A B N K X.
     A ∉ bad ⟶
     Crypt (shrK A) ⦃Nonce N, Agent B, Key K, X⦄ ∈ parts (IK s) ⟶
       X = Crypt (shrK B) ⦃Key K, Agent A⦄ ∧ K ∈ range sesK
  }"

lemmas m3_inv2_ticketI =
  m3_inv2_ticket_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv2_ticketE [elim] =
  m3_inv2_ticket_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv2_ticketD =
  m3_inv2_ticket_def [THEN setc_def_to_dest, rule_format, rotated -1]


text ‹Invariance proof.›

lemma PO_m3_inv2_ticket_init [iff]:
  "init m3 ⊆ m3_inv2_ticket"
by (auto simp add: m3_defs intro!: m3_inv2_ticketI)

lemma PO_m3_inv2_ticket_trans [iff]:
  "{m3_inv2_ticket ∩ m3_inv1_lkeysec} trans m3 {> m3_inv2_ticket}"
apply (auto simp add: PO_hoare_defs m3_defs intro!: m3_inv2_ticketI)
apply (auto dest: m3_inv2_ticketD)
― ‹2 subgoals, from step4 [?]›
apply (drule Body [where H="IK s" for s], drule parts_cut,
       auto dest: m3_inv2_ticketD)+
done

lemma PO_m3_inv2_ticket [iff]: "reach m3 ⊆ m3_inv2_ticket"
by (rule inv_rule_incr) (auto del: subsetI)


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

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

NOTE: For NSSK, this invariant cannot be inherited from the corresponding
L2 invariant. The simulation relation is only an implication not an equivalence.
›

definition
  m3_inv3_sesK_compr :: "m3_state set"
where
  "m3_inv3_sesK_compr ≡ {s. ∀K KK.
     KK ⊆ range sesK ⟶
     (Key K ∈ analz (Key`KK ∪ (IK s))) = (K ∈ KK ∨ Key K ∈ analz (IK s))
  }"

lemmas m3_inv3_sesK_comprI = m3_inv3_sesK_compr_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv3_sesK_comprE = m3_inv3_sesK_compr_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv3_sesK_comprD = m3_inv3_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_inv3_sesK_compr_simps =
  m3_inv3_sesK_comprD
  m3_inv3_sesK_comprD [where KK="{Kab}" for Kab, simplified]
  m3_inv3_sesK_comprD [where KK="insert Kab KK" for Kab KK, simplified]
  insert_commute_Key

text ‹Invariance proof.›

lemma PO_m3_inv3_sesK_compr_step4:
  "{m3_inv3_sesK_compr ∩ m3_inv2_ticket ∩ m3_inv1_lkeysec}
      m3_step4 Ra A B Na Kab X
   {> m3_inv3_sesK_compr}"
proof -
  { fix K KK s
    assume H:
      "s ∈ m3_inv1_lkeysec" "s ∈ m3_inv3_sesK_compr" "s ∈ m3_inv2_ticket"
      "runs s Ra = Some (Init, [A, B], [])"
      "Na = Ra$na"
      "KK ⊆ range sesK"
      "Crypt (shrK A) ⦃Nonce Na, Agent B, Key Kab, X⦄ ∈ analz (IK s)"
    have
      "(Key K ∈ analz (insert X (Key ` KK ∪ IK s))) =
          (K ∈ KK ∨ Key K ∈ analz (insert X (IK s)))"
    proof (cases "A ∈ bad")
      case True
        with H have "X ∈ analz (IK s)" by (auto dest!: Decrypt)
      moreover
        with H have "X ∈ analz (Key ` KK ∪ IK s)"
        by (auto intro: analz_monotonic)
      ultimately show ?thesis using H
        by (auto simp add: m3_inv3_sesK_compr_simps analz_insert_eq)
    next
      case False thus ?thesis using H
      by (fastforce simp add: m3_inv3_sesK_compr_simps
                    dest!: m3_inv2_ticketD [OF analz_into_parts])
    qed
  }
  thus ?thesis
  by (auto simp add: PO_hoare_defs m3_defs intro!: m3_inv3_sesK_comprI dest!: analz_Inj_IK)
qed

text ‹All together now.›

lemmas PO_m3_inv3_sesK_compr_trans_lemmas =
  PO_m3_inv3_sesK_compr_step4

lemma PO_m3_inv3_sesK_compr_init [iff]:
  "init m3 ⊆ m3_inv3_sesK_compr"
by (auto simp add: m3_defs intro!: m3_inv3_sesK_comprI)

lemma PO_m3_inv3_sesK_compr_trans [iff]:
  "{m3_inv3_sesK_compr ∩ m3_inv2_ticket ∩ m3_inv1_lkeysec}
     trans m3
   {> m3_inv3_sesK_compr}"
by (auto simp add: m3_def m3_trans_def intro!: PO_m3_inv3_sesK_compr_trans_lemmas)
   (auto simp add: PO_hoare_defs m3_defs m3_inv3_sesK_compr_simps intro!: m3_inv3_sesK_comprI)

lemma PO_m3_inv3_sesK_compr [iff]: "reach m3 ⊆ m3_inv3_sesK_compr"
by (rule_tac J="m3_inv2_ticket ∩ m3_inv1_lkeysec" in inv_rule_incr) (auto)


(******************************************************************************)
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 Na⦄ ∈ H
  ⟹ Insec A B (Msg [aNon Na]) ∈ abs_msg H"
| am_M2:
    "Crypt (shrK C) ⦃Nonce N, Agent B, Key K, X⦄ ∈ H
  ⟹ Secure Sv C (Msg [aNon N, aAgt B, aKey K]) ∈ abs_msg H"
| am_M3:
    "Crypt (shrK C) ⦃Key K, Agent A⦄ ∈ H
  ⟹ Secure Sv C (Msg [aKey K, aAgt A]) ∈ abs_msg H"
| am_M4:
    "Crypt K (Nonce N) ∈ H
  ⟹ dAuth K (Msg [aNon N]) ∈ abs_msg H"
| am_M5:
    "Crypt K ⦃Nonce N, Nonce N'⦄ ∈ H
  ⟹ dAuth K (Msg [aNon N, aNon N']) ∈ 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     ― ‹only an implication!›
  "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      ― ‹only an implication!›
  "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}"

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_keysD = R23_keys_def [THEN rel_def_to_dest, simplified, rule_format, rotated 2]

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_nonD = R23_non_def [THEN rel_def_to_dest, simplified, rule_format, rotated 2]

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 ‹Further lemmas: general lemma for simplifier and different instantiations.›

lemmas R23_keys_dests =
  R23_keysD
  R23_keysD [where KK="{}", simplified]
  R23_keysD [where KK="{K}" for K, simplified]
  R23_keysD [where KK="insert K KK" for K KK, simplified, OF _ _ conjI]

lemmas R23_non_dests =
  R23_nonD
  R23_nonD [where KK="{}", simplified]
  R23_nonD [where KK="{K}" for K, simplified]
  R23_nonD [where KK="insert K KK" for K KK, simplified, OF _ _ conjI]

lemmas R23_dests = R23_keys_dests R23_non_dests

(* lemmas insert_commute_Key = insert_commute [where x="Key K" for K]  *)
(*
lemmas R23_keys_emptyD =
  R23_keysD [where KK="{}", simplified, THEN iffD1, rotated 1]
  R23_keysD [where KK="{}", simplified, THEN iffD2, rotated 1]
*)

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 dest: R23_dests)+
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 m2_defs 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 m2_defs m3_defs intro!: R23_intros)

lemma PO_m3_step3_refines_m2_step3:
  "{R23 ∩ (m2_inv3a_sesK_compr) × (m3_inv3_sesK_compr ∩ m3_inv1_lkeysec)}
     (m2_step3 Rs A B Na Kab), (m3_step3 Rs A B Na Kab)
   {> 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_inv3_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])),
          chan := insert (Secure Sv A (Msg [aNon Na, aAgt B, aKey Kab]))
                 (insert (Secure Sv B (Msg [aKey Kab, aAgt A])) (chan s)) ⦈"
    let ?t'=
      "t⦇ runs := (runs t)(Rs ↦ (Serv, [A, B], [aNon Na])),
          IK := insert
                  (Crypt (shrK A)
                    ⦃Nonce Na, Agent B, Key Kab,
                       Crypt (shrK B) ⦃Key Kab, Agent A⦄⦄)
                  (IK t) ⦈"
    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_inv3_sesK_compr_simps dest: R23_keys_dests)
  moreover
    have "(?s', ?t') ∈ R23_non" using H
    by (-) (rule R23_intros,
            auto simp add: m2_inv3a_sesK_compr_simps m3_inv3_sesK_compr_simps dest: R23_non_dests)
  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 m2_defs m3_defs)
qed

(*  with equality in R23_keys [OLD, before adding session key compromise]:

goal (1 subgoal):
 1. ⋀s t. ⟦t ∈ m3_inv3_keyuse; t ∈ m3_inv1_lkeysec; t ∈ m3_inv5_badkeys;
           Kab ∉ dom (runs t); Kab ∈ range sesK;
           ⦃Agent A, Agent B, Nonce Na⦄ ∈ parts (IK t);
           Kab ∉ keysFor (analz (IK t)); Key (shrK A) ∉ analz (IK t);
           (s, t) ∈ R23_msgs; (s, t) ∈ R23_keys; (s, t) ∈ R23_pres; Kab ≠ shrK A;
           Key (shrK B) ∈ analz (IK t); Kab ≠ shrK B; A ∉ bad; B ∈ bad⟧
          ⟹ Key Kab ∈ analz (IK t)

This does NOT hold, since Kab is revealed in abstract model when A ∉ bad; B ∈ bad,
but not in concrete one, since here it is protected by A's encryption.
*)


lemma PO_m3_step4_refines_m2_step4:
  "{R23 ∩ (m2_inv3b_sesK_compr_non)
        × (m3_inv3_sesK_compr ∩ m3_inv2_ticket ∩ m3_inv1_lkeysec)}
     (m2_step4 Ra A B Na Kab), (m3_step4 Ra A B Na Kab X)
   {> 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_inv3b_sesK_compr_non"
      "t ∈ m3_inv3_sesK_compr" "t ∈ m3_inv2_ticket" "t ∈ m3_inv1_lkeysec"
      "runs t Ra = Some (Init, [A, B], [])"
      "Na = Ra$na"
      "Crypt (shrK A) ⦃Nonce Na, Agent B, Key Kab, X⦄ ∈ analz (IK t)"
    let ?s' = "s⦇ runs := (runs s)(Ra ↦ (Init, [A, B], [aKey Kab])) ⦈"
    and ?t' = "t⦇ runs := (runs t)(Ra ↦ (Init, [A, B], [aKey Kab])),
                  IK := insert X (IK t) ⦈"
    from H
    have "Secure Sv A (Msg [aNon Na, aAgt B, aKey Kab]) ∈ chan s" by auto
    moreover
    have "X ∈ parts (IK t)" using H by (auto dest!: Body MPair_parts)
    hence "(?s', ?t') ∈ R23_msgs" using H by (auto intro!: R23_intros)
    moreover
    have "(?s', ?t') ∈ R23_keys"
    proof (cases)
      assume "A ∈ bad"
      with H have "X ∈ analz (IK t)" by (-) (drule Decrypt, auto)
      with H show ?thesis
        by (-) (rule R23_intros, auto dest!: analz_cut  intro: analz_monotonic)
    next
      assume "A ∉ bad" show ?thesis
      proof -
        note H
        moreover
        with ‹A ∉ bad›
        have "X = Crypt (shrK B) ⦃Key Kab, Agent A⦄ ∧ Kab ∈ range sesK"
          by (auto dest!: m3_inv2_ticketD)
        moreover
        { assume H1: "Key (shrK B) ∈ analz (IK t)"
          have "aKey Kab ∈ extr ik0 (chan s)"
          proof -
            note calculation
            moreover
            hence "Secure Sv B (Msg [aKey Kab, aAgt A]) ∈ chan s"
              by (-) (drule analz_into_parts, drule Body, elim MPair_parts, auto)
            ultimately
            show ?thesis using H1 by auto
          qed
        }
        ultimately show ?thesis
          by (-) (rule R23_intros, auto simp add: m3_inv3_sesK_compr_simps)
      qed
    qed
    moreover
    have "(?s', ?t') ∈ R23_non"
    proof (cases)
      assume "A ∈ bad"
      hence "X ∈ analz (IK t)" using H by (-) (drule Decrypt, auto)
      thus ?thesis using H
        by (-) (rule R23_intros, auto dest!: analz_cut intro: analz_monotonic)
    next
      assume "A ∉ bad"
      hence "X = Crypt (shrK B) ⦃Key Kab, Agent A ⦄ ∧ Kab ∈ range sesK" using H
        by (auto dest!: m3_inv2_ticketD)
      thus ?thesis using H
        by (-) (rule R23_intros,
                auto simp add: m2_inv3b_sesK_compr_non_simps m3_inv3_sesK_compr_simps
                     dest: R23_non_dests)
    qed
    moreover
    have "(?s', ?t') ∈ R23_pres" using H by (auto intro!: R23_intros)
    moreover
    note calculation
  }
  thus ?thesis
    by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs dest!: analz_Inj_IK)
qed

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

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

lemma PO_m3_step7_refines_m2_step7:
  "{R23}
     (m2_step7 Rb A B Nb Kab), (m3_step7 Rb A B Nb Kab)
   {> R23}"
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)


text ‹Intruder events.›

lemma PO_m3_leak_refines_m2_leak:
 "{R23}
     m2_leak Rs Ra Rb A B, m3_leak Rs Ra Rb A B
   {> R23}"
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)
   (auto dest: R23_dests)

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 m2_defs 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 dest: R23_dests)
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_step7_refines_m2_step7 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 m2_defs m3_defs intro!: R23_intros)

lemma PO_m3_refines_trans_m2 [iff]:
  "{R23 ∩ (m2_inv3a_sesK_compr ∩ m2_inv3b_sesK_compr_non)
        × (m3_inv3_sesK_compr ∩ m3_inv2_ticket ∩ 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 m2_defs m3_defs)


text ‹Refinement result.›

lemma m3_refines_m2 [iff]:
  "refines
     (R23 ∩ (m2_inv3a_sesK_compr ∩ m2_inv3b_sesK_compr_non)
          × (m3_inv3_sesK_compr ∩ m3_inv2_ticket ∩ m3_inv1_lkeysec))
     med32 m2 m3"
by (rule Refinement_using_invariants) (auto)

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


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

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

definition
  m3_inv4_ikk_init :: "m3_state set"
where
  "m3_inv4_ikk_init ≡ {s. ∀Ra K A B al.
     runs s Ra = Some (Init, [A, B], aKey K # al) ⟶ A ∈ good ⟶ B ∈ good ⟶
     Key K ∈ analz (IK s) ⟶
       (∃Nb'. (K, Ra $ na, Nb') ∈ leak s)
  }"

lemmas m3_inv4_ikk_initI = m3_inv4_ikk_init_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv4_ikk_initE [elim] = m3_inv4_ikk_init_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv4_ikk_initD = m3_inv4_ikk_init_def [THEN setc_def_to_dest, rule_format, rotated 1]

lemma PO_m3_inv4_ikk_init: "reach m3 ⊆ m3_inv4_ikk_init"
proof (rule INV_from_Refinement_using_invariants [OF m3_refines_m2])
  show "Range (R23 ∩ (m2_inv3a_sesK_compr ∩ m2_inv3b_sesK_compr_non)
                   × (m3_inv3_sesK_compr ∩ m3_inv2_ticket ∩ m3_inv1_lkeysec)
                   ∩ m2_inv6_ikk_init × UNIV)
      ⊆ m3_inv4_ikk_init"
    by (auto simp add: R23_def R23_pres_def intro!: m3_inv4_ikk_initI)
       (elim m2_inv6_ikk_initE, auto dest: R23_keys_dests)
qed auto


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

definition
  m3_inv5_ikk_resp :: "m3_state set"
where
  "m3_inv5_ikk_resp ≡ {s. ∀Rb K A B al.
     runs s Rb = Some (Resp, [A, B], aKey K # al) ⟶ A ∈ good ⟶ B ∈ good ⟶
     Key K ∈ analz (IK s) ⟶
       K ∈ Domain (leak s)
  }"

lemmas m3_inv5_ikk_respI = m3_inv5_ikk_resp_def [THEN setc_def_to_intro, rule_format]
lemmas m3_inv5_ikk_respE [elim] = m3_inv5_ikk_resp_def [THEN setc_def_to_elim, rule_format]
lemmas m3_inv5_ikk_respD = m3_inv5_ikk_resp_def [THEN setc_def_to_dest, rule_format, rotated 1]

lemma PO_m3_inv4_ikk_resp: "reach m3 ⊆ m3_inv5_ikk_resp"
proof (rule INV_from_Refinement_using_invariants [OF m3_refines_m2])
  show "Range (R23 ∩ (m2_inv3a_sesK_compr ∩ m2_inv3b_sesK_compr_non)
                   × (m3_inv3_sesK_compr ∩ m3_inv2_ticket ∩ m3_inv1_lkeysec)
                   ∩ m2_inv7_ikk_resp × UNIV)
      ⊆ m3_inv5_ikk_resp"
    by (auto simp add: R23_def R23_pres_def intro!: m3_inv5_ikk_respI)
       (elim m2_inv7_ikk_respE, auto dest: R23_keys_dests)
qed auto


end