Theory m2_confid_chan

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

  Project: Development of Security Protocols by Refinement

  Module:  Auth_simple/m2_confid_chan.thy (Isabelle/HOL 2016-1)
  ID:      $Id: m2_confid_chan.thy 133854 2017-03-20 17:53:50Z csprenge $
  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
  
  One-Way authentication protocols
  Refinement 2: protocol using confidential channels

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

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

section ‹Refinement 2b: Confidential Channel Protocol›

theory m2_confid_chan imports m1_auth "../Refinement/Channels"
begin

text ‹We refine the abstract authentication protocol to the first two
steps of the Needham-Schroeder-Lowe protocol, which we call NSL/2.
In standard protocol notation, the original protocol is specified as follows.
\[
\begin{array}{llll}
  \mathrm{M1.} & A \rightarrow B & : & \{N_A, A\}_{K(B)} \\
  \mathrm{M2.} & B \rightarrow A & : & \{N_A, N_B, B\}_{K(A)} 
\end{array}
\]
At this refinement level, we abstract the encrypted messages to 
non-cryptographic messages transmitted on confidential channels.›

declare domIff [simp, iff del]


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

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

type_synonym 
  m2_obs = m1_state 

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


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

definition 
  m2_init :: "m2_state set"
where
  "m2_init ≡ { ⦇ 
     runs = Map.empty, 
     chan = {}
  ⦈ }"


definition
  m2_step1 :: "[rid_t, agent, agent, nonce] ⇒ (m2_state × m2_state) set"
where
  "m2_step1 Ra A B Na ≡ {(s, s1).

     ― ‹guards:›
     Ra ∉ dom (runs s) ∧
     Na = Ra$0 ∧

     ― ‹actions:›
     s1 = s⦇
       runs := (runs s)(Ra ↦ (Init, [A, B], [])), 
       ― ‹send ‹Na› on confidential channel 1›
       chan := insert (Confid A B (Msg [aNon Na])) (chan s)
     ⦈
  }"


definition
  m2_step2 :: "[rid_t, agent, agent, nonce, nonce] ⇒ (m2_state × m2_state) set"
where
  "m2_step2 Rb A B Na Nb ≡ {(s, s1).

     ― ‹guards›
     Rb ∉ dom (runs s) ∧
     Nb = Rb$0 ∧

     Confid A B (Msg [aNon Na]) ∈ chan s ∧           ― ‹receive M1›

     ― ‹actions›
     s1 = s⦇ 
       runs := (runs s)(Rb ↦ (Resp, [A, B], [aNon Na])), 
       chan := insert (Confid B A (Msg [aNon Na, aNon Nb])) (chan s)
     ⦈  
  }"


definition
  m2_step3 :: "[rid_t, agent, agent, nonce, nonce] ⇒ (m2_state × m2_state) set"
where
  "m2_step3 Ra A B Na Nb ≡ {(s, s1).

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

     Confid B A (Msg [aNon Na, aNon Nb]) ∈ chan s ∧  ― ‹receive M2›

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


text ‹Intruder fake event.›

definition     ― ‹refines @{term Id}› 
  m2_fake :: "(m2_state × m2_state) set"
where
  "m2_fake ≡ {(s, s1). 
    ― ‹actions:›
    s1 = s⦇ chan := fake ik0 (dom (runs s)) (chan s) ⦈
  }"


text ‹Transition system.›

definition 
  m2_trans :: "(m2_state × m2_state) set" where
  "m2_trans ≡ (⋃ A B Ra Rb Na Nb.
     m2_step1 Ra A B Na    ∪
     m2_step2 Rb A B Na Nb ∪
     m2_step3 Ra A B Na Nb ∪
     m2_fake ∪
     Id
  )"

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

lemmas m2_defs = 
  m2_def m2_init_def m2_trans_def m2_obs_def
  m2_step1_def m2_step2_def m2_step3_def m2_fake_def 


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

subsubsection ‹Invariant 1: Messages only contains generated nonces.›
(******************************************************************************)

definition 
  m2_inv1_nonces :: "m2_state set" where
  "m2_inv1_nonces ≡ {s. ∀R. 
     aNon (R$0) ∈ atoms (chan s) ⟶ R ∈ dom (runs s) 
  }"

lemmas m2_inv1_noncesI = 
  m2_inv1_nonces_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv1_noncesE [elim] = 
  m2_inv1_nonces_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv1_noncesD = 
  m2_inv1_nonces_def [THEN setc_def_to_dest, rule_format, rotated 1]


lemma PO_m2_inv1_init [iff]: "init m2 ⊆ m2_inv1_nonces"
by (auto simp add: PO_hoare_def m2_defs intro!: m2_inv1_noncesI) 

lemma PO_m2_inv1_trans [iff]:
  "{m2_inv1_nonces} trans m2 {> m2_inv1_nonces}"
apply (auto simp add: PO_hoare_def m2_defs intro!: m2_inv1_noncesI) 
apply (auto dest: m2_inv1_noncesD)
― ‹1 subgoal›
apply (subgoal_tac "aNon (R$0) ∈ atoms (chan xa)", auto)
done

lemma PO_m2_inv012 [iff]: 
  "reach m2 ⊆ m2_inv1_nonces"
by (rule inv_rule_basic) (auto)


subsubsection ‹Invariant 3: relates message 2 with the responder run›
(******************************************************************************)
(*
 1. ⋀a y. ⟦runs a = runs y; runs y Ra = Some (Init, [A, B], []);
           Confid A B (Msg [aNon (Ra$0), aNon Nb]) ∈ chan y; A ∉ bad; B ∉ bad⟧
          ⟹ ∃Rb. Nb = Rb $ 0 ∧ runs y Rb = Some (Resp, [A, B], [aNon (Ra $ 0)])
*)
text ‹It is needed, together with initiator nonce secrecy, in proof 
obligation REF/@{term m2_step2}.›

definition 
  m2_inv3_msg2 :: "m2_state set" where
  "m2_inv3_msg2 ≡ {s. ∀A B Na Nb. 
     Confid B A (Msg [aNon Na, aNon Nb]) ∈ chan s ⟶ 
     aNon Na ∉ extr ik0 (chan s) ⟶
       (∃Rb. Nb = Rb$0 ∧ runs s Rb = Some (Resp, [A, B], [aNon Na]))
  }"

lemmas m2_inv3_msg2I = m2_inv3_msg2_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv3_msg2E [elim] = m2_inv3_msg2_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv3_msg2D = m2_inv3_msg2_def [THEN setc_def_to_dest, rule_format, rotated 1]


lemma PO_m2_inv4_init [iff]:
  "init m2 ⊆ m2_inv3_msg2"
by (auto simp add: PO_hoare_def m2_defs intro!: m2_inv3_msg2I) 

lemma PO_m2_inv4_trans [iff]:
  "{m2_inv3_msg2} trans m2 {> m2_inv3_msg2}"
apply (auto simp add: PO_hoare_def m2_defs intro!: m2_inv3_msg2I)
apply (auto dest: m2_inv3_msg2D dom_lemmas)
― ‹2 subgoals›
  apply (drule m2_inv3_msg2D, auto dest: dom_lemmas)
  apply (drule m2_inv3_msg2D, auto, force)
done

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


subsubsection ‹Invariant 4: Initiator nonce secrecy.›
(******************************************************************************)

text ‹It is needed in the proof 
obligation REF/@{term m2_step2}. It would be sufficient to prove the invariant 
for the case @{term "x=None"}, but we have generalized it here.›

definition 
  m2_inv4_inon_secret :: "m2_state set" where
  "m2_inv4_inon_secret ≡ {s. ∀A B Ra al.
     runs s Ra = Some (Init, [A, B], al) ⟶
     A ∉ bad ⟶ B ∉ bad ⟶ 
       aNon (Ra$0) ∉ extr ik0 (chan s)
  }"

lemmas m2_inv4_inon_secretI = 
  m2_inv4_inon_secret_def [THEN setc_def_to_intro, rule_format]
lemmas m2_inv4_inon_secretE [elim] = 
  m2_inv4_inon_secret_def [THEN setc_def_to_elim, rule_format]
lemmas m2_inv4_inon_secretD = 
  m2_inv4_inon_secret_def [THEN setc_def_to_dest, rule_format, rotated 1]


lemma PO_m2_inv3_init [iff]:
  "init m2 ⊆ m2_inv4_inon_secret"
by (auto simp add: PO_hoare_def m2_defs intro!: m2_inv4_inon_secretI)
 
lemma PO_m2_inv3_trans [iff]:
  "{m2_inv4_inon_secret ∩ m2_inv1_nonces} 
     trans m2 
   {> m2_inv4_inon_secret}"
apply (auto simp add: PO_hoare_def m2_defs intro!: m2_inv4_inon_secretI)  
apply (auto dest: m2_inv4_inon_secretD) 
― ‹3 subgoals›
  apply (fastforce)                ― ‹requires @{text "m2_inv1_nonces"}›
  apply (fastforce)                ― ‹requires ind hyp›
  apply (fastforce)                ― ‹requires ind hyp›
done 

lemma PO_m2_inv3 [iff]: "reach m2 ⊆ m2_inv4_inon_secret"
by (rule inv_rule_incr [where J="m2_inv1_nonces"]) (auto)


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

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

abbreviation
  med21 :: "m2_obs ⇒ m1_obs" where
  "med21 ≡ id"


text ‹Proof obligations.›

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

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

lemma PO_m2_step3_refines_m1_step3:
  "{R12 ∩ UNIV × (m2_inv4_inon_secret ∩ m2_inv3_msg2)} 
     (m1_step3 Ra A B Na Nb), (m2_step3 Ra A B Na Nb) 
   {> R12}"
by (auto simp add: PO_rhoare_defs R12_def m1_defs m2_defs)
   (blast)

text ‹New fake events refine skip.›

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

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_fake_refines_skip 


text ‹All together now...›

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

lemma PO_m2_refines_trans_m1 [iff]:
  "{R12 ∩ 
    UNIV × (m2_inv4_inon_secret ∩ m2_inv3_msg2)} 
     (trans m1), (trans m2) 
   {> R12}"
apply (auto simp add: m2_def m2_trans_def m1_def m1_trans_def)
apply (blast intro!: PO_m2_trans_refines_m1_trans)+
done

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

lemma PO_m3_refines_m2:
  "refines 
     (R12 ∩ 
      UNIV × (m2_inv4_inon_secret ∩ m2_inv3_msg2 ∩ m2_inv1_nonces))
     med21 m1 m2"
by (rule Refinement_using_invariants) (auto)


end