Theory pfslvl1

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

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  pfslvl1.thy (Isabelle/HOL 2016-1)
  ID:      $Id: pfslvl1.thy 133183 2017-01-31 13:55:43Z csprenge $
  Author:  Joseph Lallemand, INRIA Nancy <joseph.lallemand@loria.fr>
           Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  Level-1 protocol using ephemeral asymmetric keys to achieve forward secrecy.

  Copyright (c) 2015-2016 Joseph Lallemand and Christoph Sprenger
  Licence: LGPL

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

section ‹Key Transport Protocol with PFS (L1)›

theory pfslvl1
imports Runs Secrecy AuthenticationI Payloads
begin


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

(**************************************************************************************************)
subsection ‹State and Events›
(**************************************************************************************************)

consts
  sk :: "nat"
  kE :: "nat"  
  Nend :: "nat"

text ‹Proofs break if @{term "1"} is used, because @{method "simp"} replaces it with
@{term "Suc 0"}\dots›
abbreviation
  "xpkE ≡ Var 0"

abbreviation
  "xskE ≡ Var 2"

abbreviation
  "xsk ≡ Var 3"

abbreviation
  "xEnd ≡ Var 4"


abbreviation 
  "End ≡ Number Nend"


text ‹domain of each role (protocol dependent)›
fun domain :: "role_t ⇒ var set" where
  "domain Init = {xpkE, xskE, xsk}"
| "domain Resp = {xpkE, xsk}"



consts
  test :: rid_t
  
consts
  guessed_runs :: "rid_t ⇒ run_t"
  guessed_frame :: "rid_t ⇒ frame"

text ‹specification of the guessed frame›
text ‹\begin{enumerate}
\item Domain
\item Well-typedness.
  The messages in the frame of a run never contain implementation material
  even if the agents of the run are dishonest.
  Therefore we consider only well-typed frames.
  This is notably required for the session key compromise; it also helps proving
  the partitionning of ik,
  since we know that the messages added by the protocol do not contain ltkeys in their
  payload and are therefore valid implementations.
\item We also ensure that the values generated by the frame owner are correctly guessed.
\end{enumerate}›
specification (guessed_frame) 
  guessed_frame_dom_spec [simp]:
    "dom (guessed_frame R) = domain (role (guessed_runs R))"
  guessed_frame_payload_spec [simp, elim]:
    "guessed_frame R x = Some y ⟹ y ∈ payload"
  guessed_frame_Init_xpkE [simp]: 
    "role (guessed_runs R) = Init ⟹ guessed_frame R xpkE = Some (epubKF (R$kE))"
  guessed_frame_Init_xskE [simp]: 
    "role (guessed_runs R) = Init ⟹ guessed_frame R xskE = Some (epriKF (R$kE))"
  guessed_frame_Resp_xsk [simp]: 
    "role (guessed_runs R) = Resp ⟹ guessed_frame R xsk = Some (NonceF (R$sk))"
apply (rule exI [of _ 
    "λR.
      if role (guessed_runs R) = Init 
      then [xpkE ↦ epubKF (R$kE), xskE ↦ epriKF (R$kE), xsk ↦ End]
      else [xpkE ↦ End, xsk ↦ NonceF (R$sk)]"],
  auto simp add: domIff intro: role_t.exhaust)  
done


abbreviation
  "test_owner ≡ owner (guessed_runs test)"

abbreviation
  "test_partner ≡ partner (guessed_runs test)"


text ‹level 1 state›
record l1_state = 
  s0_state +
  progress :: progress_t
  signals :: "signal ⇒ nat"


type_synonym l1_obs = "l1_state"


abbreviation
  run_ended :: "var set option ⇒ bool"
where
  "run_ended r ≡ in_progress r xsk"

lemma run_ended_not_None [elim]:
  "run_ended R ⟹ R = None ⟹ False"
by (fast dest: in_progress_Some)

text ‹@{term "test_ended s"} $\longleftrightarrow$ the test run has ended in @{term "s"}›
abbreviation
  test_ended :: "'a l1_state_scheme ⇒ bool"
where
  "test_ended s ≡ run_ended (progress s test)"

text ‹a run can emit signals if it involves the same agents as the test run, and if the test run 
  has not ended yet›
definition
  can_signal :: "'a l1_state_scheme ⇒ agent ⇒ agent ⇒ bool"
where
  "can_signal s A B ≡
  ((A = test_owner ∧ B = test_partner) ∨ (B = test_owner ∧ A = test_partner)) ∧
  ¬ test_ended s"


text ‹events›
definition
  l1_learn :: "msg ⇒ ('a l1_state_scheme * 'a l1_state_scheme) set"
where
  "l1_learn m ≡ {(s,s').
    ― ‹guard›
    synth (analz (insert m (ik s))) ∩ (secret s) = {}  ∧
    ― ‹action›
    s' = s ⦇ik := ik s ∪ {m}⦈
  }"


text ‹protocol events›

text ‹
\begin{itemize}
\item step 1: create @{term "Ra"}, @{term "A"} generates @{term "pkE"}, @{term "skE"}
\item step 2: create @{term "Rb"}, @{term "B"} reads @{term "pkE"} authentically,
  generates @{term "K"}, emits a running signal for @{term "A"}, @{term "B"},
  (@{term "pkE"}, @{term "K"})
\item step 3: @{term "A"} reads @{term "K"} and @{term "pkE"} authentically,
  emits a commit signal for @{term "A"}, @{term "B"}, (@{term "pkE"}, @{term "K"})
\end{itemize}
›

definition
  l1_step1 :: "rid_t ⇒ agent ⇒ agent ⇒ ('a l1_state_scheme * 'a l1_state_scheme) set"
where
  "l1_step1 Ra A B ≡ {(s, s').
    ― ‹guards:›
    Ra ∉ dom (progress s) ∧
    guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
    ― ‹actions:›
    s' = s⦇
      progress := (progress s)(Ra ↦ {xpkE, xskE})
      ⦈
  }"


definition
  l1_step2 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ ('a l1_state_scheme * 'a l1_state_scheme) set"
where
  "l1_step2 Rb A B KE ≡ {(s, s').
    ― ‹guards:›
    guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
    Rb ∉ dom (progress s) ∧
    guessed_frame Rb xpkE = Some KE ∧
    (can_signal s A B ⟶ ― ‹authentication guard›
      (∃ Ra. guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
             in_progress (progress s Ra) xpkE ∧ guessed_frame Ra xpkE = Some KE)) ∧
    (Rb = test ⟶ NonceF (Rb$sk) ∉ synth (analz (ik s))) ∧
    ― ‹actions:›
    s' = s⦇ progress := (progress s)(Rb ↦ {xpkE, xsk}),
            secret := {x. x = NonceF (Rb$sk) ∧ Rb = test} ∪ secret s,
            signals := if can_signal s A B then
                          addSignal (signals s) (Running A B (⟨ KE, NonceF (Rb$sk) ⟩))
                       else
                          signals s
          ⦈
  }"

definition
  l1_step3 :: "rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ ('a l1_state_scheme * 'a l1_state_scheme) set"
where
  "l1_step3 Ra A B K ≡ {(s, s').
    ― ‹guards:›
    guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
    progress s Ra = Some {xpkE, xskE} ∧
    guessed_frame Ra xsk = Some K ∧
    (can_signal s A B ⟶ ― ‹authentication guard›
      (∃ Rb. guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
             progress s Rb = Some {xpkE, xsk} ∧
             guessed_frame Rb xpkE = Some (epubKF (Ra$kE)) ∧
             guessed_frame Rb xsk = Some K)) ∧
    (Ra = test ⟶ K ∉ synth (analz (ik s))) ∧

    ― ‹actions:›
    s' = s⦇ progress := (progress s)(Ra ↦ {xpkE, xskE, xsk}),
            secret := {x. x = K ∧ Ra = test} ∪ secret s,
            signals := if can_signal s A B then
                         addSignal (signals s) (Commit A B ⟨epubKF (Ra$kE), K⟩)
                       else
                         signals s
          ⦈
  }"




text ‹specification›

definition 
  l1_init :: "l1_state set"
where
  "l1_init ≡ { ⦇
    ik = {},
    secret = {},
    progress = Map.empty,
    signals = λx. 0
    ⦈ }"

definition 
  l1_trans :: "('a l1_state_scheme * 'a l1_state_scheme) set" where
  "l1_trans ≡ (⋃m Ra Rb A B K KE.
     l1_step1 Ra A B ∪
     l1_step2 Rb A B KE ∪
     l1_step3 Ra A B K ∪
     l1_learn m ∪
     Id
  )"

definition 
  l1 :: "(l1_state, l1_obs) spec" where
  "l1 ≡ ⦇
    init = l1_init,
    trans = l1_trans,
    obs = id
  ⦈"

lemmas l1_defs = 
  l1_def l1_init_def l1_trans_def
  l1_learn_def
  l1_step1_def l1_step2_def l1_step3_def

lemmas l1_nostep_defs =
  l1_def l1_init_def l1_trans_def

lemma l1_obs_id [simp]: "obs l1 = id"
by (simp add: l1_def)


declare domIff [iff]

lemma run_ended_trans:
  "run_ended (progress s R) ⟹
   (s, s') ∈ trans l1 ⟹
   run_ended (progress s' R)"
apply (auto simp add: l1_nostep_defs)
apply (simp add: l1_defs ik_dy_def, fast ?)+
done

declare domIff [iff del]

lemma can_signal_trans:
  "can_signal s' A B ⟹
  (s, s') ∈ trans l1 ⟹
  can_signal s A B"
by (auto simp add: can_signal_def run_ended_trans)


(**************************************************************************************************)
subsection ‹Refinement: secrecy›
(**************************************************************************************************)

text ‹mediator function›
definition 
  med01s :: "l1_obs ⇒ s0_obs"
where
  "med01s t ≡ ⦇ ik = ik t, secret = secret t ⦈"


text ‹relation between states›
definition
  R01s :: "(s0_state * l1_state) set"
where
  "R01s ≡ {(s,s').
    s = ⦇ik = ik s', secret = secret s'⦈
    }"


text ‹protocol independent events›

lemma l1_learn_refines_learn:
  "{R01s} s0_learn m, l1_learn m {>R01s}"
apply (simp add: PO_rhoare_defs R01s_def)
apply auto
apply (simp add: l1_defs s0_defs s0_secrecy_def)
done



text ‹protocol events›
lemma l1_step1_refines_skip:
  "{R01s} Id, l1_step1 Ra A B {>R01s}"
by (auto simp add: PO_rhoare_defs R01s_def l1_step1_def)

lemma l1_step2_refines_add_secret_skip:
  "{R01s} s0_add_secret (NonceF (Rb$sk)) ∪ Id, l1_step2 Rb A B KE {>R01s}"
apply (auto simp add: PO_rhoare_defs R01s_def s0_add_secret_def)
apply (auto simp add: l1_step2_def)
done

lemma l1_step3_refines_add_secret_skip:
  "{R01s} s0_add_secret K ∪ Id, l1_step3 Ra A B K {>R01s}"
apply (auto simp add: PO_rhoare_defs R01s_def s0_add_secret_def)
apply (auto simp add: l1_step3_def)
done


text ‹refinement proof›
lemmas l1_trans_refines_s0_trans = 
  l1_learn_refines_learn
  l1_step1_refines_skip l1_step2_refines_add_secret_skip l1_step3_refines_add_secret_skip 

lemma l1_refines_init_s0 [iff]:
  "init l1 ⊆ R01s `` (init s0)"
by (auto simp add: R01s_def s0_defs l1_defs s0_secrecy_def)


lemma l1_refines_trans_s0 [iff]:
  "{R01s} trans s0, trans l1 {> R01s}"
by (auto simp add: s0_def l1_def s0_trans_def l1_trans_def 
         intro: l1_trans_refines_s0_trans)


lemma obs_consistent_med01x [iff]: 
  "obs_consistent R01s med01s s0 l1"
by (auto simp add: obs_consistent_def R01s_def med01s_def)



text ‹refinement result›
lemma l1s_refines_s0 [iff]: 
  "refines 
     R01s
     med01s s0 l1"
by (auto simp add:refines_def PO_refines_def)

lemma  l1_implements_s0 [iff]: "implements med01s s0 l1"
by (rule refinement_soundness) (fast)


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

abbreviation "l1_secrecy ≡ s0_secrecy"


lemma l1_obs_secrecy [iff]: "oreach l1 ⊆ l1_secrecy"
apply (rule external_invariant_translation 
         [OF s0_obs_secrecy _ l1_implements_s0])
apply (auto simp add: med01s_def s0_secrecy_def)
done

lemma l1_secrecy [iff]: "reach l1 ⊆ l1_secrecy"
by (rule external_to_internal_invariant [OF l1_obs_secrecy], auto)


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

subsubsection ‹inv1›
(**************************************************************************************************)
text ‹if a commit signal for a nonce has been emitted,
 then there is a finished initiator run with this nonce.
›



definition
  l1_inv1 :: "l1_state set"
where
  "l1_inv1 ≡ {s. ∀ Ra A B K.
    signals s (Commit A B ⟨epubKF (Ra$kE), K⟩) > 0 ⟶
      guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
      progress s Ra = Some {xpkE, xskE, xsk} ∧
      guessed_frame Ra xsk = Some K
   }"
  
lemmas l1_inv1I = l1_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas l1_inv1E [elim] = l1_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas l1_inv1D = l1_inv1_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]


lemma l1_inv1_init [iff]:
  "init l1 ⊆ l1_inv1"
by (auto simp add: l1_def l1_init_def l1_inv1_def)

declare domIff [iff]

lemma l1_inv1_trans [iff]:
  "{l1_inv1} trans l1 {> l1_inv1}"
apply (auto simp add: PO_hoare_defs l1_nostep_defs intro!: l1_inv1I)
apply (auto simp add: l1_defs ik_dy_def l1_inv1_def)
done

lemma PO_l1_inv1 [iff]: "reach l1 ⊆ l1_inv1"
by (rule inv_rule_basic) (auto)


subsubsection ‹inv2›
(**************************************************************************************************)
text ‹if a responder run knows a nonce, then a running signal for this nonce has been emitted›

definition
  l1_inv2 :: "l1_state set"
where
  "l1_inv2 ≡ {s. ∀ KE A B Rb.
    guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ⟶
    progress s Rb = Some {xpkE, xsk} ⟶
    guessed_frame Rb xpkE = Some KE ⟶
    can_signal s A B ⟶
      signals s (Running A B ⟨KE, NonceF (Rb$sk)⟩) > 0
  }"

lemmas l1_inv2I = l1_inv2_def [THEN setc_def_to_intro, rule_format]
lemmas l1_inv2E [elim] = l1_inv2_def [THEN setc_def_to_elim, rule_format]
lemmas l1_inv2D = l1_inv2_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]


lemma l1_inv2_init [iff]:
  "init l1 ⊆ l1_inv2"
by (auto simp add: l1_def l1_init_def l1_inv2_def)

lemma l1_inv2_trans [iff]:
  "{l1_inv2} trans l1 {> l1_inv2}"
apply (auto simp add: PO_hoare_defs intro!: l1_inv2I)
apply (drule can_signal_trans, assumption)
apply (auto simp add: l1_nostep_defs)
apply (auto simp add: l1_defs ik_dy_def l1_inv2_def)
done

lemma PO_l1_inv2 [iff]: "reach l1 ⊆ l1_inv2"
by (rule inv_rule_basic) (auto)


subsubsection ‹inv3 (derived)›
(**************************************************************************************************)
text ‹if an unfinished initiator run and a finished responder run both know the same nonce,
 then the number of running signals for this nonce is strictly greater than the number of commit
 signals.
 (actually, there are 0 commit and 1 running)
›

definition
  l1_inv3 :: "l1_state set"
where
  "l1_inv3 ≡ {s. ∀ A B Rb Ra.
    guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ⟶
    progress s Rb = Some {xpkE, xsk} ⟶
    guessed_frame Rb xpkE = Some (epubKF (Ra$kE)) ⟶
    guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ⟶
    progress s Ra = Some {xpkE, xskE} ⟶
    can_signal s A B ⟶
      signals s (Commit A B (⟨epubKF (Ra$kE), NonceF (Rb$sk)⟩)) 
    < signals s (Running A B (⟨epubKF (Ra$kE), NonceF (Rb$sk)⟩)) 
  }"

lemmas l1_inv3I = l1_inv3_def [THEN setc_def_to_intro, rule_format]
lemmas l1_inv3E [elim] = l1_inv3_def [THEN setc_def_to_elim, rule_format]
lemmas l1_inv3D = l1_inv3_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]

lemma l1_inv3_derived: "l1_inv1 ∩ l1_inv2 ⊆ l1_inv3"
apply (auto intro!: l1_inv3I)
apply (auto dest!: l1_inv2D)
apply (rename_tac x A B Rb Ra)
apply (case_tac "signals x (Commit A B ⟨epubKF (Ra $ kE), NonceF (Rb $ sk)⟩) > 0", auto)
apply (fastforce dest: l1_inv1D elim: equalityE)
done


(**************************************************************************************************)
subsection ‹Refinement: injective agreement›
(**************************************************************************************************)

text ‹mediator function›
definition 
  med01ia :: "l1_obs ⇒ a0i_obs"
where
  "med01ia t ≡ ⦇a0n_state.signals = signals t⦈"


text ‹relation between states›
definition
  R01ia :: "(a0i_state * l1_state) set"
where
  "R01ia ≡ {(s,s').
    a0n_state.signals s = signals s'
    }"


text ‹protocol independent events›

lemma l1_learn_refines_a0_ia_skip:
  "{R01ia} Id, l1_learn m {>R01ia}"
apply (auto simp add: PO_rhoare_defs R01ia_def)
apply (simp add: l1_learn_def)
done



text ‹protocol events›
lemma l1_step1_refines_a0i_skip:
  "{R01ia} Id, l1_step1 Ra A B {>R01ia}"
by (auto simp add: PO_rhoare_defs R01ia_def l1_step1_def)


lemma l1_step2_refines_a0i_running_skip:
  "{R01ia} a0i_running A B ⟨KE, NonceF (Rb$sk)⟩ ∪ Id, l1_step2 Rb A B KE {>R01ia}"
by (auto simp add: PO_rhoare_defs R01ia_def, simp_all add: l1_step2_def a0i_running_def, auto)

lemma l1_step3_refines_a0i_commit_skip:
  "{R01ia ∩ (UNIV × l1_inv3)} a0i_commit A B ⟨epubKF (Ra$kE), K⟩ ∪ Id, l1_step3 Ra A B K {>R01ia}"
apply (auto simp add: PO_rhoare_defs R01ia_def)
apply (auto simp add: l1_step3_def a0i_commit_def)
apply (force elim!: l1_inv3E)+
done

text ‹refinement proof›
lemmas l1_trans_refines_a0i_trans = 
  l1_learn_refines_a0_ia_skip
  l1_step1_refines_a0i_skip l1_step2_refines_a0i_running_skip l1_step3_refines_a0i_commit_skip 

lemma l1_refines_init_a0i [iff]:
  "init l1 ⊆ R01ia `` (init a0i)"
by (auto simp add: R01ia_def a0i_defs l1_defs)


lemma l1_refines_trans_a0i [iff]:
  "{R01ia ∩ (UNIV × (l1_inv1 ∩ l1_inv2))} trans a0i, trans l1 {> R01ia}"
proof -
  let ?pre' = "R01ia ∩ (UNIV × l1_inv3)"
  show ?thesis (is "{?pre} ?t1, ?t2 {>?post}")
  proof (rule relhoare_conseq_left)
    show "?pre ⊆ ?pre'"
      using l1_inv3_derived by blast
  next 
    show "{?pre'} ?t1, ?t2 {> ?post}"
      apply (auto simp add: a0i_def l1_def a0i_trans_def l1_trans_def)
      prefer 2 using l1_step2_refines_a0i_running_skip apply (simp add: PO_rhoare_defs, blast)
      prefer 2 using l1_step3_refines_a0i_commit_skip apply (simp add: PO_rhoare_defs, blast)
      apply (blast intro!:l1_trans_refines_a0i_trans)+
      done
  qed
qed


lemma obs_consistent_med01ia [iff]: 
  "obs_consistent R01ia med01ia a0i l1"
by (auto simp add: obs_consistent_def R01ia_def med01ia_def)



text ‹refinement result›
lemma l1_refines_a0i [iff]: 
  "refines 
     (R01ia ∩ (reach a0i × (l1_inv1 ∩ l1_inv2)))
     med01ia a0i l1"
by (rule Refinement_using_invariants, auto)

lemma  l1_implements_a0i [iff]: "implements med01ia a0i l1"
by (rule refinement_soundness) (fast)


(**************************************************************************************************)
subsection ‹Derived invariants: injective agreement›
(**************************************************************************************************)

definition 
  l1_iagreement :: "('a l1_state_scheme) set"
where
  "l1_iagreement ≡ {s. ∀ A B N. signals s (Commit A B N) ≤ signals s (Running A B N)}"

lemmas l1_iagreementI = l1_iagreement_def [THEN setc_def_to_intro, rule_format]
lemmas l1_iagreementE [elim] = l1_iagreement_def [THEN setc_def_to_elim, rule_format]


lemma l1_obs_iagreement [iff]: "oreach l1 ⊆ l1_iagreement"
apply (rule external_invariant_translation 
         [OF PO_a0i_obs_agreement _ l1_implements_a0i])
apply (auto simp add: med01ia_def l1_iagreement_def a0i_agreement_def)
done

lemma l1_iagreement [iff]: "reach l1 ⊆ l1_iagreement"
by (rule external_to_internal_invariant [OF l1_obs_iagreement], auto)



end