Theory m1_keydist

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

  Project: Development of Security Protocols by Refinement

  Module:  Key_establish/m1b_keydist.thy (Isabelle/HOL 2016-1)
  ID:      $Id: m1_keydist.thy 134925 2017-05-24 17:53:14Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Key distribution protocols
  First refinement: abstract server-based key transport protocol with 
  initiator and responder roles.

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

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

chapter ‹Key Establishment Protocols›

text ‹In this chapter, we develop several key establishment protocols:
\begin{itemize} 
\item Needham-Schroeder Shared Key (NSSK) 
\item core Kerberos IV and V, and
\item Denning-Sacco. 
\end{itemize}
›


section ‹Basic abstract key distribution (L1)›

theory m1_keydist imports "../Refinement/Runs" "../Refinement/s0g_secrecy"
begin

text ‹The first refinement introduces the protocol roles, local memory of the
agents and the communication structure of the protocol.  For actual 
communication, the "receiver" directly reads the memory of the "sender". 

It captures the core of essentials of server-based key distribution protocols:
The server generates a key that the clients read from his memory. At this
stage we are only interested in secrecy preservation, not in authentication.
›

declare option.split_asm [split]
declare domIff [simp, iff del] 

consts
  sk :: "nat"             ― ‹identifier used for session keys›


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

text ‹Runs record the protocol participants (initiator, responder) and the 
keys learned during the execution. In later refinements, we will also add
nonces and timestamps to the run record.

The variables ‹kn› and ‹az› from ‹s0g_secrecy_leak› 
are replaced by runs using a data refinement. Variable ‹lk› is 
concretized into variable ‹leak›. 

We define the state in two separate record definitions. The first one has 
just a runs field and the second extends this with a leak field.  Later 
refinements may define different state for leaks (e.g. to record more context).
›

record m1r_state = 
  runs :: runs_t

record m1x_state = m1r_state +  
  leak :: "key set"             ― ‹keys leaked to attacker›

type_synonym m1x_obs = "m1x_state"

text ‹Predicate types for invariants and transition relation types. Use the
r-version for invariants and transitions if there is no reference to the leak
variable. This improves reusability in later refinements.
›
type_synonym 'x m1r_pred = "'x m1r_state_scheme set"
type_synonym 'x m1x_pred = "'x m1x_state_scheme set"

type_synonym 'x m1r_trans = "('x m1r_state_scheme × 'x m1r_state_scheme) set"
type_synonym 'x m1x_trans = "('x m1x_state_scheme × 'x m1x_state_scheme) set"


subsubsection ‹Key knowledge and authorization (reconstruction)›
(******************************************************************************)

text ‹Key knowledge and authorization relations, reconstructed from the runs 
and an unspecified initial key setup. These auxiliary definitions are used in 
some event guards and in the simulation relation (see below).›

text ‹Knowledge relation (reconstructed)›

inductive_set
  knC :: "runs_t ⇒ (key × agent) set" for runz :: "runs_t" 
where
  knC_init:
    "runz Ra = Some (Init, [A, B], aKey K # al) ⟹ (K, A) ∈ knC runz"
| knC_resp:
    "runz Rb = Some (Resp, [A, B], aKey K # al) ⟹ (K, B) ∈ knC runz"
| knC_serv:
    "⟦ Rs ∈ dom runz; fst (the (runz Rs)) = Serv ⟧ ⟹ (sesK (Rs$sk), Sv) ∈ knC runz"
| knC_0:
    "(K, A) ∈ keySetup ⟹ (K, A) ∈ knC runz"


text ‹Authorization relation (reconstructed)›

inductive_set
  azC :: "runs_t ⇒ (key × agent) set" for runz :: "runs_t"
where
  azC_good:
    "⟦ runz Rs = Some (Serv, [A, B], al); C ∈ {A, B, Sv} ⟧ 
   ⟹ (sesK (Rs$sk), C) ∈ azC runz"
| azC_bad:
    "⟦ runz Rs = Some (Serv, [A, B], al); A ∈ bad ∨ B ∈ bad ⟧ 
   ⟹ (sesK (Rs$sk), C) ∈ azC runz"
| azC_0:
    "⟦ (K, C) ∈ keySetup ⟧ ⟹ (K, C) ∈ azC runz"


declare knC.intros [intro]
declare azC.intros [intro]


text ‹Misc lemmas: empty state, projections, ...›

lemma knC_empty [simp]: "knC Map.empty = keySetup"
by (auto elim: knC.cases)

lemma azC_empty [simp]: "azC Map.empty = keySetup"
by (auto elim: azC.cases)


text ‹‹azC› and run abstraction›

lemma azC_map_runs [simp]: "azC (map_runs h runz) = azC runz"
by (auto simp add: map_runs_def elim!: azC.cases)


text ‹Update lemmas for @{term "knC"}›

lemma knC_upd_Init_Resp_None:
  "⟦ R ∉ dom runz; rol ∈ {Init, Resp} ⟧
  ⟹ knC (runz(R ↦ (rol, [A, B], []))) = knC runz"
by (fastforce simp add: domIff elim!: knC.cases)

lemma knC_upd_Init_Some:
  "⟦ runz Ra = Some (Init, [A, B], []) ⟧ 
  ⟹ knC (runz(Ra ↦ (Init, [A, B], [aKey Kab]))) = insert (Kab, A) (knC runz)"
apply (auto elim!: knC.cases) 
― ‹3 subgoals›
apply (rename_tac Raa Aa Ba K al, rule_tac A=Aa and B=Ba and al=al in knC_init, auto)
apply (rename_tac Rb Aa Ba K al, rule_tac A=Aa and B=Ba and al=al in knC_resp, auto)
apply (rule_tac knC_serv, auto)
done

lemma knC_upd_Resp_Some:
  "⟦ runz Ra = Some (Resp, [A, B], []) ⟧ 
  ⟹ knC (runz(Ra ↦ (Resp, [A, B], [aKey Kab]))) = insert (Kab, B) (knC runz)"
apply (auto elim!: knC.cases)
― ‹3 subgoals›
apply (rename_tac Raa Aa Ba K al, rule_tac A=Aa and B=Ba and al=al in knC_init, auto)
apply (rename_tac Raa Aa Ba K al, rule_tac A=Aa and B=Ba and al=al in knC_resp, auto)
apply (rule_tac knC_serv, auto)
done

lemma knC_upd_Server:
  "⟦ Rs ∉ dom runz ⟧
  ⟹ knC (runz(Rs ↦ (Serv, [A, B], []))) = insert (sesK (Rs$sk), Sv) (knC runz)"
apply (auto elim!: knC.cases)
― ‹2 subgoals›
apply (rename_tac Raa Aa Ba K al, rule_tac A=Aa and B=Ba in knC_init, auto dest: dom_lemmas)
apply (rename_tac Raa Aa Ba K al, rule_tac A=Aa and B=Ba in knC_resp, auto dest: dom_lemmas)
done

lemmas knC_upd_lemmas [simp] = 
  knC_upd_Init_Resp_None knC_upd_Init_Some knC_upd_Resp_Some
  knC_upd_Server 


text ‹Update lemmas for @{term "azC"}›

lemma azC_upd_Init_None:
  "⟦ Ra ∉ dom runz ⟧
  ⟹ azC (runz(Ra ↦ (Init, [A, B], []))) = azC runz"
by (auto simp add: azC.simps elim!: azC.cases dest: dom_lemmas)

lemma azC_upd_Resp_None:
  "⟦ Rb ∉ dom runz ⟧
  ⟹ azC (runz(Rb ↦ (Resp, [A, B], []))) = azC runz"
by (auto simp add: azC.simps elim!: azC.cases dest: dom_lemmas)

lemma azC_upd_Init_Some:
  "⟦ runz Ra = Some (Init, [A, B], []) ⟧
  ⟹ azC (runz(Ra ↦ (Init, [A, B], al))) = azC runz"
apply (auto elim!: azC.cases)
― ‹5 subgoals›
apply (rule_tac azC_good, auto)
apply (rule_tac azC_good, auto)
apply (rule_tac azC_good, auto)
apply (rule_tac azC_bad, auto)+
done

lemma azC_upd_Resp_Some:
  "⟦ runz Rb = Some (Resp, [A, B], []) ⟧
  ⟹ azC (runz(Rb ↦ (Resp, [A, B], al))) = azC runz"
apply (auto elim!: azC.cases)
― ‹5 subgoals›
apply (rule_tac azC_good, auto)
apply (rule_tac azC_good, auto)
apply (rule_tac azC_good, auto)
apply (rule_tac azC_bad, auto)+
done

lemma azC_upd_Serv_bad:
  "⟦ Rs ∉ dom runz; A ∈ bad ∨ B ∈ bad ⟧
  ⟹ azC (runz(Rs ↦ (Serv, [A, B], al))) = azC runz ∪ {sesK (Rs$sk)} × UNIV"
apply (auto elim!: azC.cases)
― ‹10 subgoals›
apply (
  rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
  rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
  rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
  rename_tac Rsa Aa Ba ala C, rule_tac A=Aa and B=Ba and al=ala in azC_bad, auto dest: dom_lemmas,
  rename_tac Rsa Aa Ba ala C, rule_tac A=Aa and B=Ba and al=ala in azC_bad, auto dest: dom_lemmas
)+
done

lemma azC_upd_Serv_good:
  "⟦ Rs ∉ dom runz; K = sesK (Rs$sk); A ∉ bad; B ∉ bad ⟧
  ⟹ azC (runz(Rs ↦ (Serv, [A, B], al))) 
      = azC runz ∪ {(K, A), (K, B), (K, Sv)}"
apply (auto elim!: azC.cases)
― ‹5 subgoals›
apply (
  rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
  rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
  rename_tac Rsa Aa Ba ala, rule_tac A=Aa and B=Ba and al=ala in azC_good, auto dest: dom_lemmas,
  rename_tac Rsa Aa Ba ala C, rule_tac A=Aa and B=Ba and al=ala in azC_bad, auto dest: dom_lemmas,
  rename_tac Rsa Aa Ba ala C, rule_tac A=Aa and B=Ba and al=ala in azC_bad, auto dest: dom_lemmas
)+
done

lemma azC_upd_Serv:
  "⟦ Rs ∉ dom runz; K = sesK (Rs$sk) ⟧
  ⟹ azC (runz(Rs ↦ (Serv, [A, B], al))) =
     azC runz ∪ {K} × (if A ∉ bad ∧ B ∉ bad then {A, B, Sv} else UNIV)" 
by (simp add: azC_upd_Serv_bad azC_upd_Serv_good) 

lemmas azC_upd_lemmas [simp] =
  azC_upd_Init_None azC_upd_Resp_None
  azC_upd_Init_Some azC_upd_Resp_Some azC_upd_Serv


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

definition     ― ‹by @{term "A"}, refines skip›
  m1x_step1 :: "[rid_t, agent, agent] ⇒ 'x m1r_trans"
where
  "m1x_step1 Ra A B ≡ {(s, s1).

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

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

definition     ― ‹by @{term "B"}, refines skip›
  m1x_step2 :: "[rid_t, agent, agent] ⇒ 'x m1r_trans"
where
  "m1x_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 @{term "Server"}, refines @{term s0g_gen}›
  m1x_step3 :: "[rid_t, agent, agent, key] ⇒ 'x m1r_trans"
where
  "m1x_step3 Rs A B Kab ≡ {(s, s1).

    ― ‹guards:›
    Rs ∉ dom (runs s) ∧                        ― ‹‹Rs› is fresh›
    Kab = sesK (Rs$sk) ∧                       ― ‹generate session key›

    ― ‹actions:›
    s1 = s⦇ runs := (runs s)(Rs ↦ (Serv, [A, B], [])) ⦈
  }"

definition     ― ‹by @{term "A"}, refines @{term s0g_learn}›
  m1x_step4 :: "[rid_t, agent, agent, key] ⇒ 'x m1x_trans"
where
  "m1x_step4 Ra A B Kab ≡ {(s, s1).
    ― ‹guards:›
    runs s Ra = Some (Init, [A, B], []) ∧
    (Kab ∉ leak s ⟶ (Kab, A) ∈ azC (runs s)) ∧   ― ‹authorization guard›

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

definition     ― ‹by @{text "B"}, refines @{term s0g_learn}›
  m1x_step5 :: "[rid_t, agent, agent, key] ⇒ 'x m1x_trans"
where
  "m1x_step5 Rb A B Kab ≡ {(s, s1).
    ― ‹guards:›
    runs s Rb = Some (Resp, [A, B], []) ∧ 
    (Kab ∉ leak s ⟶ (Kab, B) ∈ azC (runs s)) ∧    ― ‹authorization guard›

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

definition     ― ‹by attacker, refines @{term s0g_leak}›
  m1x_leak :: "rid_t ⇒ 'x m1x_trans"
where
  "m1x_leak Rs ≡ {(s, s1).           
    ― ‹guards:›
    Rs ∈ dom (runs s) ∧
    fst (the (runs s Rs)) = Serv ∧         ― ‹compromise server run ‹Rs››

    ― ‹actions:›
    s1 = s⦇ leak := insert (sesK (Rs$sk)) (leak s) ⦈
  }"


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

definition 
  m1x_init :: "m1x_state set"
where
  "m1x_init ≡ { ⦇
     runs = Map.empty,
     leak = corrKey         ― ‹statically corrupted keys initially leaked›
  ⦈ }"

definition 
  m1x_trans :: "'x m1x_trans" where
  "m1x_trans ≡ (⋃A B Ra Rb Rs Kab.
     m1x_step1 Ra A B ∪
     m1x_step2 Rb A B ∪
     m1x_step3 Rs A B Kab ∪
     m1x_step4 Ra A B Kab ∪
     m1x_step5 Rb A B Kab ∪
     m1x_leak Rs ∪
     Id
  )"

definition 
  m1x :: "(m1x_state, m1x_obs) spec" where
  "m1x ≡ ⦇
    init = m1x_init,
    trans = m1x_trans,
    obs = id
  ⦈"

lemmas m1x_defs = 
  m1x_def m1x_init_def m1x_trans_def
  m1x_step1_def m1x_step2_def m1x_step3_def m1x_step4_def m1x_step5_def 
  m1x_leak_def 

lemma m1x_obs_id [simp]: "obs m1x = id"
by (simp add: m1x_def)


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

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

text ‹Only run identifiers or static keys can be (concretely) known or 
authorized keys. (This reading corresponds to the contraposition of the 
property expressed below.)›

definition 
  m1x_inv1_key :: "m1x_state set" 
where
  "m1x_inv1_key ≡ {s. ∀Rs A.
     Rs ∉ dom (runs s) ⟶ 
       (sesK (Rs$sk), A) ∉ knC (runs s) ∧ 
       (sesK (Rs$sk), A) ∉ azC (runs s) ∧
       sesK (Rs$sk) ∉ leak s
  }"

lemmas m1x_inv1_keyI = m1x_inv1_key_def [THEN setc_def_to_intro, rule_format]
lemmas m1x_inv1_keyE [elim] = 
  m1x_inv1_key_def [THEN setc_def_to_elim, rule_format]
lemmas m1x_inv1_keyD [dest] = 
  m1x_inv1_key_def [THEN setc_def_to_dest, rule_format, rotated 1]


text ‹Invariance proof.›

lemma PO_m1x_inv1_key_init [iff]:
  "init m1x ⊆ m1x_inv1_key"
by (auto simp add: m1x_defs m1x_inv1_key_def) 

lemma PO_m1x_inv1_key_trans [iff]:
  "{m1x_inv1_key} trans m1x {> m1x_inv1_key}"
by (auto simp add: PO_hoare_defs m1x_defs intro!: m1x_inv1_keyI)

lemma PO_m1x_inv1_key [iff]: "reach m1x ⊆ m1x_inv1_key"
by (rule inv_rule_basic) (auto)


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

text ‹med10: The mediator function maps a concrete observation to an 
abstract one.›

definition 
  med01x :: "m1x_obs ⇒ key s0g_obs"
where
  "med01x t ≡ ⦇ kn = knC (runs t), az = azC (runs t), lk = leak t ⦈"


text ‹R01: The simulation relation expreses key knowledge and authorization
in terms of the client and server run information.›

definition
  R01x :: "(key s0g_state × m1x_state) set" where
  "R01x ≡ {(s, t). s = med01x t}"

lemmas R01x_defs = R01x_def med01x_def


text ‹Refinement proof.›

lemma PO_m1x_step1_refines_skip:
  "{R01x} 
     Id, (m1x_step1 Ra A B) 
   {> R01x}"
by (auto simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs)

lemma PO_m1x_step2_refines_skip:
  "{R01x} 
     Id, (m1x_step2 Rb A B) 
   {> R01x}"
by (auto simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs)

lemma PO_m1x_step3_refines_s0g_gen:
  "{R01x ∩ UNIV × m1x_inv1_key} 
     (s0g_gen Kab Sv {Sv, A, B}), (m1x_step3 Rs A B Kab) 
   {> R01x}"
by (auto simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs)

lemma PO_m1x_step4_refines_s0g_learn:
  "{R01x} 
     (s0g_learn Kab A), (m1x_step4 Ra A B Kab) 
   {> R01x}"
by (auto simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs)

lemma PO_m1x_step5_refines_s0g_learn:
  "{R01x} 
     (s0g_learn Kab B), (m1x_step5 Rb A B Kab) 
   {> R01x}"
by (auto simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs) 

lemma PO_m1x_leak_refines_s0g_leak:
  "{R01x} 
     (s0g_leak (sesK (Rs$sk))), (m1x_leak Rs) 
   {> R01x}"
by (fastforce simp add: PO_rhoare_defs R01x_defs s0g_defs m1x_defs)


text ‹All together now...›

lemmas PO_m1x_trans_refines_s0g_trans = 
  PO_m1x_step1_refines_skip PO_m1x_step2_refines_skip
  PO_m1x_step3_refines_s0g_gen PO_m1x_step4_refines_s0g_learn 
  PO_m1x_step5_refines_s0g_learn PO_m1x_leak_refines_s0g_leak

lemma PO_m1x_refines_init_s0g [iff]:
  "init m1x ⊆ R01x``(init s0g)"
by (auto simp add: R01x_defs s0g_defs m1x_defs intro!: s0g_secrecyI s0g_domI)

lemma PO_m1x_refines_trans_s0g [iff]:
  "{R01x ∩ UNIV × m1x_inv1_key} 
     (trans s0g), (trans m1x) 
   {> R01x}"
by (auto simp add: m1x_def m1x_trans_def s0g_def s0g_trans_def
         intro!: PO_m1x_trans_refines_s0g_trans)


text ‹Observation consistency.›

lemma obs_consistent_med01x [iff]: 
  "obs_consistent R01x med01x s0g m1x"
by (auto simp add: obs_consistent_def R01x_defs s0g_def m1x_def)


text ‹Refinement result.›

lemma PO_m1x_refines_s0g [iff]: 
  "refines 
     (R01x ∩ UNIV × m1x_inv1_key)
     med01x s0g m1x"
by (rule Refinement_using_invariants) (auto del: subsetI)

lemma  m1x_implements_s0g [iff]: "implements med01x s0g m1x"
by (rule refinement_soundness) (fast)


subsection ‹Derived invariants›
(******************************************************************************)

subsubsection ‹inv2: Secrecy›
(*invh*************************************************************************)

text ‹Secrecy, expressed in terms of runs.›

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

lemmas m1x_secrecyI = m1x_secrecy_def [THEN setc_def_to_intro, rule_format]
lemmas m1x_secrecyE [elim] = m1x_secrecy_def [THEN setc_def_to_elim, rule_format]


text ‹Invariance proof.›

lemma PO_m1x_obs_secrecy [iff]: "oreach m1x ⊆ m1x_secrecy"
apply (rule external_invariant_translation [OF PO_s0g_obs_secrecy _ m1x_implements_s0g])
apply (auto simp add: med01x_def m1x_secrecy_def s0g_secrecy_def)
done

lemma PO_m1x_secrecy [iff]: "reach m1x ⊆ m1x_secrecy"
by (rule external_to_internal_invariant [OF PO_m1x_obs_secrecy], auto)


end