Theory sklvl3

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

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  sklvl3.thy (Isabelle/HOL 2016-1)
  ID:      $Id: sklvl3.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-3 SKEME/IKEv1 protocol using generic channel implementation. 
  Refines model sklvl2 based on channel assumptions.

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

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

section ‹SKEME Protocol (L3 locale)›

theory sklvl3
imports sklvl2 Implem_lemmas
begin

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

text ‹Level 3 state.›
text ‹(The types have to be defined outside the locale.)›

record l3_state = skl1_state +  
  bad :: "agent set"

type_synonym l3_obs = "l3_state"

type_synonym
  l3_pred = "l3_state set"

type_synonym
  l3_trans = "(l3_state × l3_state) set"


text ‹attacker event›
definition
  l3_dy :: "msg  l3_trans"
where
  "l3_dy  ik_dy"


text ‹Compromise events.›

definition
  l3_lkr_others :: "agent  l3_trans"
where
  "l3_lkr_others A  {(s,s').
    ― ‹guards›
    A  test_owner 
    A  test_partner 
    ― ‹actions›
    s' = sbad := {A}  bad s,
           ik := keys_of A  ik s
  }"

definition
  l3_lkr_actor :: "agent  l3_trans"
where
  "l3_lkr_actor A  {(s,s').
    ― ‹guards›
    A = test_owner 
    A  test_partner 
    ― ‹actions›
    s' = sbad := {A}  bad s,
           ik := keys_of A  ik s
  }"

definition
  l3_lkr_after :: "agent  l3_trans"
where
  "l3_lkr_after A  {(s,s').
    ― ‹guards›
    test_ended s 
    ― ‹actions›
    s' = sbad := {A}  bad s,
           ik := keys_of A  ik s
  }"

definition
  l3_skr :: "rid_t  msg  l3_trans"
where
  "l3_skr R K  {(s,s').
    ― ‹guards›
    R  test  R  partners 
    in_progress (progress s R) xsk 
    guessed_frame R xsk = Some K 
    ― ‹actions›
    s' = sik := {K}  ik s
  }"


text ‹New locale for the level 3 protocol. This locale does not add new assumptions, it is 
only used to separate the level 3 protocol from the implementation locale.›

locale sklvl3 = valid_implem
begin

text ‹Protocol events (with $K=H(ni, nr))$:
\begin{itemize}
\item step 1: create @{term "Ra"}, @{term "A"} generates @{term "nx"} and @{term "ni"},
  confidentially sends @{term "ni"},
  computes and insecurely sends $@{term "g"}^@{term "nx"}$
\item step 2: create @{term "Rb"}, @{term "B"} receives @{term "ni"} (confidentially)
  and $@{term "g"}^@{term "nx"}$ (insecurely),
  generates @{term "ny"} and @{term "nr"},
  confidentially sends @{term "nr"}, insecurely sends $@{term "g"}^@{term "ny"}$ and
  $MAC_K(@{term "g"}^@{term "nx"}, @{term "g"}^@{term "ny"}, @{term "B"}, @{term "A"})$
  computes $@{term "g"}^@{term "nx*ny"}$,
  emits a running signal for @{term "Init"}, @{term "ni"}, @{term "nr"}, 
  $@{term "g"}^@{term "nx*ny"}$
\item step 3: @{term "A"} receives @{term "nr"} confidentially,
  and $@{term "g"}^@{term "ny"}$ and the MAC insecurely,
  sends $MAC_K(@{term "g"}^@{term "ny"}, @{term "g"}^@{term "nx"}, @{term "A"}, @{term "B"})$
  insecurely, computes $@{term "g"}^@{term "ny*nx"}$, emits a commit signal for @{term "Init"},
  @{term "ni"}, @{term "nr"}, $@{term "g"}^@{term "ny*nx"}$,
  a running signal for @{term "Resp"}, @{term "ni"}, @{term "nr"}, $@{term "g"}^@{term "ny*nx"}$,
  declares the secret $@{term "g"}^@{term "ny*nx"}$
\item step 4: @{term "B"} receives the MAC insecurely,
  emits a commit signal for @{term "Resp"}, @{term "ni"}, @{term "nr"},
  $@{term "g"}^@{term "nx*ny"}$,
  declares the secret $@{term "g"}^@{term "nx*ny"}$
\end{itemize}
›
definition
  l3_step1 :: "rid_t  agent  agent  l3_trans"
where
  "l3_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  {xnx, xni, xgnx}),
      ik := {implConfid A B (NonceF (Ra$ni))}  
             ({implInsec A B (Exp Gen (NonceF (Ra$nx)))} 
              (ik s))
      
  }"


definition
  l3_step2 :: "rid_t  agent  agent  msg  msg  l3_trans"
where
  "l3_step2 Rb A B Ni gnx  {(s, s').
    ― ‹guards:›
    guessed_runs Rb = role=Resp, owner=B, partner=A 
    Rb  dom (progress s) 
    guessed_frame Rb xgnx = Some gnx 
    guessed_frame Rb xni = Some Ni 
    guessed_frame Rb xsk = Some (Exp gnx (NonceF (Rb$ny))) 
    implConfid A B Ni  ik s 
    implInsec A B gnx  ik s 
    ― ‹actions:›
    s' = s progress := (progress s)(Rb  {xny, xni, xnr, xgny, xgnx, xsk}),
            ik := {implConfid B A (NonceF (Rb$nr))} 
                   ({implInsec B A Exp Gen (NonceF (Rb$ny)),
                                hmac Number 0, gnx, Exp Gen (NonceF (Rb$ny)), Agent B, Agent A
                                     (Hash Ni, NonceF (Rb$nr)) }  
                    (ik s)),
            signalsInit := 
              if can_signal s A B then
                addSignal (signalsInit s) 
                          (Running A B Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny)))
              else
                signalsInit s,
            signalsInit2 := 
              if can_signal s A B then
                addSignal (signalsInit2 s) (Running A B (Exp gnx (NonceF (Rb$ny))))
              else
                signalsInit2 s
         
  }"  


definition
  l3_step3 :: "rid_t  agent  agent  msg  msg  l3_trans"
where
  "l3_step3 Ra A B Nr gny  {(s, s').
    ― ‹guards:›
    guessed_runs Ra = role=Init, owner=A, partner=B 
    progress s Ra = Some {xnx, xni, xgnx} 
    guessed_frame Ra xgny = Some gny 
    guessed_frame Ra xnr = Some Nr 
    guessed_frame Ra xsk = Some (Exp gny (NonceF (Ra$nx))) 
    implConfid B A Nr  ik s 
    implInsec B A gny, hmac Number 0, Exp Gen (NonceF (Ra$nx)), gny, Agent B, Agent A
                         (Hash NonceF (Ra$ni), Nr)  ik s 
    ― ‹actions:›
    s' = s progress := (progress s)(Ra  {xnx, xni, xnr, xgnx, xgny, xsk, xEnd}),
            ik := {implInsec A B (hmac Number 1, gny, Exp Gen (NonceF (Ra$nx)), Agent A, Agent B
                                     (Hash NonceF (Ra$ni), Nr))}  ik s,
            secret := {x. x = Exp gny (NonceF (Ra$nx))  Ra = test}  secret s,
            signalsInit := 
              if can_signal s A B then
                addSignal (signalsInit s) 
                          (Commit A B NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx)))
              else
                signalsInit s,
            signalsInit2 := 
              if can_signal s A B then
                addSignal (signalsInit2 s) (Commit A B (Exp gny (NonceF (Ra$nx))))
              else
                signalsInit2 s,
            signalsResp := 
              if can_signal s A B then
                addSignal (signalsResp s) 
                          (Running A B NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx)))
              else
                signalsResp s,
            signalsResp2 := 
              if can_signal s A B then
                addSignal (signalsResp2 s) (Running A B (Exp gny (NonceF (Ra$nx))))
              else
                signalsResp2 s
          
  }"


definition
  l3_step4 :: "rid_t  agent  agent  msg  msg  l3_trans"
where
  "l3_step4 Rb A B Ni gnx  {(s, s').
    ― ‹guards:›
    guessed_runs Rb = role=Resp, owner=B, partner=A 
    progress s Rb = Some {xny, xni, xnr, xgnx, xgny, xsk} 
    guessed_frame Rb xgnx = Some gnx 
    guessed_frame Rb xni = Some Ni 
    implInsec A B (hmac Number 1, Exp Gen (NonceF (Rb$ny)), gnx, Agent A, Agent B
                    (Hash Ni, NonceF (Rb$nr)))  ik s 

    ― ‹actions:›
    s' = s progress := (progress s)(Rb  {xny, xni, xnr, xgnx, xgny, xsk, xEnd}),
            secret := {x. x = Exp gnx (NonceF (Rb$ny))  Rb = test}  secret s,
            signalsResp := 
              if can_signal s A B then
                addSignal (signalsResp s) 
                          (Commit A B Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny)))
              else
                signalsResp s,
            signalsResp2 := 
              if can_signal s A B then
                addSignal (signalsResp2 s) (Commit A B (Exp gnx (NonceF (Rb$ny))))
              else
                signalsResp2 s
          
  }"


text ‹Specification.›

text ‹Initial compromise.›

definition
  ik_init :: "msg set"
where
  "ik_init  {priK C |C. C  bad_init}  {pubK A | A. True}  
             {shrK A B |A B. A  bad_init  B  bad_init}  Tags"

text ‹lemmas about @{term "ik_init"}
lemma parts_ik_init [simp]: "parts ik_init = ik_init"
by (auto elim!: parts.induct, auto simp add: ik_init_def)

lemma analz_ik_init [simp]: "analz ik_init = ik_init"
by (auto dest: analz_into_parts)

lemma abs_ik_init [iff]: "abs ik_init = {}"
apply (auto elim!: absE)
apply (auto simp add: ik_init_def)
done

lemma payloadSet_ik_init [iff]: "ik_init  payload = {}"
by (auto simp add: ik_init_def)

lemma validSet_ik_init [iff]: "ik_init  valid= {}"
by (auto simp add: ik_init_def)


definition 
  l3_init :: "l3_state set"
where
  "l3_init  { 
    ik = ik_init,
    secret = {},
    progress = Map.empty,
    signalsInit = λx. 0,
    signalsResp = λx. 0,
    signalsInit2 = λx. 0,
    signalsResp2 = λx. 0,
    bad = bad_init
    }"

lemmas l3_init_defs = l3_init_def ik_init_def

definition 
l3_trans :: "l3_trans"
where
  "l3_trans  ( M N X Rb Ra A B K.
     l3_step1 Ra A B 
     l3_step2 Rb A B N X 
     l3_step3 Ra A B N X 
     l3_step4 Rb A B N X 
     l3_dy M 
     l3_lkr_others A 
     l3_lkr_after A 
     l3_skr Ra K 
     Id
  )"


definition 
  l3 :: "(l3_state, l3_obs) spec" where
  "l3  
    init = l3_init,
    trans = l3_trans,
    obs = id
  "

lemmas l3_loc_defs = 
  l3_step1_def l3_step2_def l3_step3_def l3_step4_def
  l3_def l3_init_defs l3_trans_def
  l3_dy_def
  l3_lkr_others_def l3_lkr_after_def l3_skr_def

lemmas l3_defs = l3_loc_defs ik_dy_def
lemmas l3_nostep_defs = l3_def l3_init_def l3_trans_def


lemma l3_obs_id [simp]: "obs l3 = id"
by (simp add: l3_def)


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

subsubsection ‹inv1: No long-term keys as message parts›
(**************************************************************************************************)

definition
  l3_inv1 :: "l3_state set"
where
  "l3_inv1  {s.
     parts (ik s)  range LtK  ik s
  }"

lemmas l3_inv1I = l3_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv1E [elim] = l3_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv1D = l3_inv1_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv1D' [dest]: " LtK K  parts (ik s); s  l3_inv1  LtK K  ik s"
by (auto simp add: l3_inv1_def)

lemma l3_inv1_init [iff]:
  "init l3  l3_inv1"
by (auto simp add: l3_def l3_init_def intro!:l3_inv1I)

lemma l3_inv1_trans [iff]:
  "{l3_inv1} trans l3 {> l3_inv1}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs intro!: l3_inv1I)
apply (auto simp add: l3_defs dy_fake_msg_def dy_fake_chan_def
        parts_insert [where H="ik _"] parts_insert [where H="insert _ (ik _)"]
        dest!: Fake_parts_insert)
apply (auto dest:analz_into_parts)
done

lemma PO_l3_inv1 [iff]:
  "reach l3  l3_inv1"
by (rule inv_rule_basic) (auto)



subsubsection ‹inv2: @{term "bad s"} indeed contains "bad" keys›
(**************************************************************************************************)

definition
  l3_inv2 :: "l3_state set"
where
  "l3_inv2  {s.
    Keys_bad (ik s) (bad s)
  }"

lemmas l3_inv2I = l3_inv2_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv2E [elim] = l3_inv2_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv2D = l3_inv2_def [THEN setc_def_to_dest, rule_format]


lemma l3_inv2_init [simp,intro!]:
  "init l3  l3_inv2"
by (auto simp add: l3_def l3_init_defs intro!:l3_inv2I Keys_badI)

lemma l3_inv2_trans [simp,intro!]:
  "{l3_inv2  l3_inv1} trans l3 {> l3_inv2}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs intro!: l3_inv2I)
apply (auto simp add: l3_defs dy_fake_msg_def dy_fake_chan_def)
text ‹4 subgoals: dy, lkr*, skr.›
apply (auto intro: Keys_bad_insert_Fake Keys_bad_insert_keys_of)
apply (auto intro!: Keys_bad_insert_payload)
done

lemma PO_l3_inv2 [iff]: "reach l3  l3_inv2"
by (rule_tac J="l3_inv1" in inv_rule_incr) (auto)



subsubsection ‹inv3›
(**************************************************************************************************)

text ‹If a message can be analyzed from the intruder knowledge then it can
be derived (using @{term "synth"}/@{term "analz"}) from the sets of implementation, 
non-implementation, and long-term key messages and the tags. That is, intermediate messages 
are not needed.
›

definition
  l3_inv3 :: "l3_state set"      
where
  "l3_inv3  {s.
    analz (ik s)  
    synth (analz ((ik s  payload)  ((ik s)  valid)  (ik s  range LtK)  Tags))
  }"

lemmas l3_inv3I = l3_inv3_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv3E = l3_inv3_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv3D = l3_inv3_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv3_init [iff]:
  "init l3  l3_inv3"
apply (auto simp add: l3_def l3_init_def intro!: l3_inv3I)
apply (auto simp add: ik_init_def intro!: synth_increasing [THEN [2] rev_subsetD])
done

declare domIff [iff del]

text ‹Most of the cases in this proof are simple and very similar.
The proof could probably be shortened.›

lemma l3_inv3_trans [simp,intro!]:
  "{l3_inv3} trans l3 {> l3_inv3}"
proof (simp add: l3_nostep_defs, safe)
  fix Ra A B
  show "{l3_inv3} l3_step1 Ra A B {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (auto intro!: validI dest!: analz_insert_partition [THEN [2] rev_subsetD])
    done
next
  fix Rb A B Ni gnx
  show "{l3_inv3} l3_step2 Rb A B Ni gnx {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (auto intro!: validI dest!: analz_insert_partition [THEN [2] rev_subsetD])
    done
next
  fix Ra A B Nr gny
  show "{l3_inv3} l3_step3 Ra A B Nr gny {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (auto intro!: validI dest!: analz_insert_partition [THEN [2] rev_subsetD])
    done
next
  fix Rb A B Ni gnx
  show "{l3_inv3} l3_step4 Rb A B Ni gnx {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    done
next
  fix m 
  show "{l3_inv3} l3_dy m {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs dy_fake_chan_def dy_fake_msg_def
                intro!: l3_inv3I dest!: l3_inv3D)
    apply (drule synth_analz_insert)
    apply (blast intro: synth_analz_monotone dest: synth_monotone)
    done
next
  fix A
  show "{l3_inv3} l3_lkr_others A {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (drule analz_Un_partition [of _ "keys_of A"], auto)
    done
next
  fix A
  show "{l3_inv3} l3_lkr_after A {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (drule analz_Un_partition [of _ "keys_of A"], auto)
    done
next
  fix R K
  show "{l3_inv3} l3_skr R K {> l3_inv3}"
    apply (auto simp add: PO_hoare_def l3_defs intro!: l3_inv3I dest!: l3_inv3D)
    apply (auto dest!: analz_insert_partition [THEN [2] rev_subsetD])
    done
qed

lemma PO_l3_inv3 [iff]: "reach l3  l3_inv3"
by (rule inv_rule_basic) (auto)



subsubsection ‹inv4: the intruder knows the tags›
(**************************************************************************************************)

definition
  l3_inv4 :: "l3_state set"
where
  "l3_inv4  {s.
    Tags  ik s
  }"

lemmas l3_inv4I = l3_inv4_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv4E [elim] = l3_inv4_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv4D = l3_inv4_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv4_init [simp,intro!]:
  "init l3  l3_inv4"
by (auto simp add: l3_def l3_init_def ik_init_def intro!:l3_inv4I)

lemma l3_inv4_trans [simp,intro!]:
  "{l3_inv4} trans l3 {> l3_inv4}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs intro!: l3_inv4I)
apply (auto simp add: l3_defs dy_fake_chan_def dy_fake_msg_def)
done

lemma PO_l3_inv4 [simp,intro!]: "reach l3  l3_inv4"
by (rule inv_rule_basic) (auto)


text ‹The remaining invariants are derived from the others.
They are not protocol dependent provided the previous invariants hold.›
  
subsubsection ‹inv5›
(**************************************************************************************************)

text ‹The messages that the L3 DY intruder can derive from the intruder knowledge 
(using @{term "synth"}/@{term "analz"}), are either implementations or intermediate messages or
can also be derived by the L2 intruder from the set 
@{term "extr (bad s) ((ik s)  payload) (abs (ik s))"}, that is, given the 
non-implementation messages and the abstractions of (implementation) messages
in the intruder knowledge. 
›

definition
  l3_inv5 :: "l3_state set"
where
  "l3_inv5  {s.
    synth (analz (ik s))  
    dy_fake_msg (bad s) (ik s  payload) (abs (ik s))  -payload
  }"

lemmas l3_inv5I = l3_inv5_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv5E = l3_inv5_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv5D = l3_inv5_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv5_derived: "l3_inv2  l3_inv3  l3_inv5"
by (auto simp add: abs_validSet dy_fake_msg_def intro!: l3_inv5I
            dest!: l3_inv3D [THEN synth_mono, THEN [2] rev_subsetD]
            dest!: synth_analz_NI_I_K_synth_analz_NI_E [THEN [2] rev_subsetD])

lemma PO_l3_inv5 [simp,intro!]: "reach l3  l3_inv5"
using l3_inv5_derived PO_l3_inv2 PO_l3_inv3 
by blast


subsubsection ‹inv6›
(**************************************************************************************************)

text ‹If the level 3 intruder can deduce a message implementing an insecure channel message, 
then either:
\begin{itemize}
  \item the message is already in the intruder knowledge, or
  \item the message is constructed, and the payload can also be deduced by the intruder.
\end{itemize}
›

definition
  l3_inv6 :: "l3_state set"
where
  "l3_inv6  {s.  A B M. 
     (implInsec A B M  synth (analz (ik s))  M  payload)  
     (implInsec A B M  ik s  M  synth (analz (ik s)))
  }"

lemmas l3_inv6I = l3_inv6_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv6E = l3_inv6_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv6D = l3_inv6_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv6_derived [simp,intro!]:
  "l3_inv3  l3_inv4  l3_inv6"
apply (auto intro!: l3_inv6I dest!: l3_inv3D)
text ‹1 subgoal›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implInsec_synth_analz [rotated 1, where H="_  _"])
apply (auto dest!: synth_analz_monotone [of _ "_  _" "ik _"])
done

lemma PO_l3_inv6 [simp,intro!]: "reach l3  l3_inv6"
using l3_inv6_derived PO_l3_inv3 PO_l3_inv4
by (blast)

subsubsection ‹inv7›
(**************************************************************************************************)

text ‹If the level 3 intruder can deduce a message implementing a confidential channel message,
then either:
\begin{itemize}
 \item the message is already in the intruder knowledge, or
 \item the message is constructed, and the payload can also be deduced by the intruder.
\end{itemize}
›

definition
  l3_inv7 :: "l3_state set"
where
  "l3_inv7  {s.  A B M. 
     (implConfid A B M  synth (analz (ik s))  M  payload)  
     (implConfid A B M  ik s  M  synth (analz (ik s)))
  }"

lemmas l3_inv7I = l3_inv7_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv7E = l3_inv7_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv7D = l3_inv7_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv7_derived [simp,intro!]:
  "l3_inv3  l3_inv4  l3_inv7"
apply (auto intro!: l3_inv7I dest!: l3_inv3D)
text ‹1 subgoal›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implConfid_synth_analz [rotated 1, where H="_  _"])
apply (auto dest!: synth_analz_monotone [of _ "_  _" "ik _"])
done

lemma PO_l3_inv7 [simp,intro!]: "reach l3  l3_inv7"
using l3_inv7_derived PO_l3_inv3 PO_l3_inv4
by (blast)


subsubsection ‹inv8›
(**************************************************************************************************)

text ‹If the level 3 intruder can deduce a message implementing an authentic channel message 
then either:
\begin{itemize}
  \item the message is already in the intruder knowledge, or
  \item the message is constructed, and in this case the payload can also be deduced
     by the intruder, and one of the agents is bad.
\end{itemize}
›


definition
  l3_inv8 :: "l3_state set"
where
  "l3_inv8  {s.  A B M. 
     (implAuth A B M  synth (analz (ik s))  M  payload)  
     (implAuth A B M  ik s  (M  synth (analz (ik s))  (A  bad s  B  bad s)))
  }"

lemmas l3_inv8I = l3_inv8_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv8E = l3_inv8_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv8D = l3_inv8_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv8_derived [iff]:
  "l3_inv2  l3_inv3  l3_inv4  l3_inv8"
apply (auto intro!: l3_inv8I dest!: l3_inv3D l3_inv2D)
text ‹2 subgoals: M is deducible and the agents are bad›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implAuth_synth_analz [rotated 1, where H="_  _"] elim!: synth_analz_monotone)

apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implAuth_synth_analz [rotated 1, where H="_  _"] elim!: synth_analz_monotone)
done

lemma PO_l3_inv8 [iff]: "reach l3  l3_inv8"
using l3_inv8_derived
  PO_l3_inv3 PO_l3_inv2 PO_l3_inv4
by blast


subsubsection ‹inv9›
(**************************************************************************************************)

text ‹If the level 3 intruder can deduce a message implementing a secure channel message 
then either:
\begin{itemize}
  \item the message is already in the intruder knowledge, or
  \item the message is constructed, and in this case the payload can also be deduced 
 by the intruder, and one of the agents is bad.
\end{itemize}
›

definition
  l3_inv9 :: "l3_state set"
where
  "l3_inv9  {s.  A B M. 
     (implSecure A B M  synth (analz (ik s))  M  payload)  
     (implSecure A B M  ik s  (M  synth (analz (ik s))  (A  bad s  B  bad s)))
  }"

lemmas l3_inv9I = l3_inv9_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv9E = l3_inv9_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv9D = l3_inv9_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv9_derived [iff]:
  "l3_inv2  l3_inv3  l3_inv4  l3_inv9"
apply (auto intro!: l3_inv9I dest!:l3_inv3D l3_inv2D)
text ‹2 subgoals: M is deducible and the agents are bad.›
apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implSecure_synth_analz [rotated 1, where H="_  _"] 
            elim!: synth_analz_monotone)

apply (drule synth_mono, simp, drule subsetD, assumption)
apply (auto dest!: implSecure_synth_analz [rotated 1, where H="_  _"])
done

lemma PO_l3_inv9 [iff]: "reach l3  l3_inv9"
using l3_inv9_derived
  PO_l3_inv3 PO_l3_inv2 PO_l3_inv4
by blast


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

text ‹Mediator function.›
definition 
  med23s :: "l3_obs  l2_obs"
where
  "med23s t  
    ik = ik t  payload,
    secret = secret t,
    progress = progress t,
    signalsInit = signalsInit t,
    signalsResp = signalsResp t,
    signalsInit2 = signalsInit2 t,
    signalsResp2 = signalsResp2 t,
    chan = abs (ik t),
    bad = bad t
    "

text ‹Relation between states.›

definition
  R23s :: "(l2_state * l3_state) set"
where
  "R23s  {(s, s').
    s = med23s s'
    }"

lemmas R23s_defs = R23s_def med23s_def


lemma R23sI: 
  " ik s = ik t  payload; secret s = secret t; progress s = progress t;
     signalsInit s = signalsInit t; signalsResp s = signalsResp t;
     signalsInit2 s = signalsInit2 t; signalsResp2 s = signalsResp2 t;
     chan s = abs (ik t); l2_state.bad s = bad t  
  (s, t)  R23s"
by (auto simp add: R23s_def med23s_def)

lemma R23sD: 
  "(s, t)  R23s 
    ik s = ik t  payload  secret s = secret t  progress s = progress t 
    signalsInit s = signalsInit t  signalsResp s = signalsResp t 
    signalsInit2 s = signalsInit2 t  signalsResp2 s = signalsResp2 t 
    chan s = abs (ik t)  l2_state.bad s = bad t"
by (auto simp add: R23s_def med23s_def)

lemma R23sE [elim]: 
  " (s, t)  R23s;
      ik s = ik t  payload; secret s = secret t; progress s = progress t;
      signalsInit s = signalsInit t; signalsResp s = signalsResp t;
      signalsInit2 s = signalsInit2 t; signalsResp2 s = signalsResp2 t;
      chan s = abs (ik t); l2_state.bad s = bad t   P  
  P"
by (auto simp add: R23s_def med23s_def)

lemma can_signal_R23 [simp]:
  "(s2, s3)  R23s 
   can_signal s2 A B  can_signal s3 A B"
by (auto simp add: can_signal_def)


subsubsection ‹Protocol events›
(**************************************************************************************************)

lemma l3_step1_refines_step1:
  "{R23s} l2_step1 Ra A B, l3_step1 Ra A B {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_step1_def)
done

lemma l3_step2_refines_step2:
  "{R23s} l2_step2 Rb A B Ni gnx, l3_step2 Rb A B Ni gnx{>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs l2_step2_def)
apply (auto simp add: l3_step2_def)
done

lemma l3_step3_refines_step3:
  "{R23s} l2_step3 Ra A B Nr gny, l3_step3 Ra A B Nr gny {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs l2_step3_def)
apply (auto simp add: l3_step3_def)
done

lemma l3_step4_refines_step4:
  "{R23s} l2_step4 Rb A B Ni gnx, l3_step4 Rb A B Ni gnx {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs l2_step4_def)
apply (auto simp add: l3_step4_def)
done

subsubsection ‹Intruder events›
(**************************************************************************************************)

lemma l3_dy_payload_refines_dy_fake_msg:
  "M  payload 
   {R23s  UNIV × l3_inv5} l2_dy_fake_msg M, l3_dy M {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_dy_fake_msg_def dest: l3_inv5D)
done

lemma l3_dy_valid_refines_dy_fake_chan:
  " M  valid; M'  abs {M}  
   {R23s  UNIV × (l3_inv5  l3_inv6  l3_inv7  l3_inv8  l3_inv9)} 
      l2_dy_fake_chan M', l3_dy M 
   {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs, simp add: l2_dy_fake_chan_def)
apply (auto simp add: l3_defs)
text ‹1 subgoal›
apply (erule valid_cases, simp_all add: dy_fake_chan_def)
  text ‹Insec›
  apply (blast dest: l3_inv6D l3_inv5D)
  text ‹Confid›
  apply (blast dest: l3_inv7D l3_inv5D)
  text ‹Auth›
  apply (blast dest: l3_inv8D l3_inv5D)
  text ‹Secure›
  apply (blast dest: l3_inv9D l3_inv5D)
done


lemma l3_dy_valid_refines_dy_fake_chan_Un:
  "M  valid 
   {R23s  UNIV × (l3_inv5  l3_inv6  l3_inv7  l3_inv8  l3_inv9)} 
      M'. l2_dy_fake_chan M', l3_dy M 
   {>R23s}"
by (auto dest: valid_abs intro: l3_dy_valid_refines_dy_fake_chan)


lemma l3_dy_isLtKey_refines_skip:
  "{R23s} Id, l3_dy (LtK ltk) {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs l3_defs)
apply (auto elim!: absE)
done

lemma l3_dy_others_refines_skip:
  " M  range LtK; M  valid; M  payload   
   {R23s} Id, l3_dy M {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs)
apply (auto elim!: absE intro: validI)
done


lemma l3_dy_refines_dy_fake_msg_dy_fake_chan_skip:
   "{R23s  UNIV × (l3_inv5  l3_inv6  l3_inv7  l3_inv8  l3_inv9)} 
      l2_dy_fake_msg M  (M'. l2_dy_fake_chan M')  Id, l3_dy M 
    {>R23s}"
by (cases "M  payload  valid  range LtK")
   (auto dest: l3_dy_payload_refines_dy_fake_msg l3_dy_valid_refines_dy_fake_chan_Un 
         intro: l3_dy_isLtKey_refines_skip dest!: l3_dy_others_refines_skip)


subsubsection ‹Compromise events›
(**************************************************************************************************)

lemma l3_lkr_others_refines_lkr_others:
  "{R23s} l2_lkr_others A, l3_lkr_others A {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_lkr_others_def)
done

lemma l3_lkr_after_refines_lkr_after:
  "{R23s} l2_lkr_after A, l3_lkr_after A {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_lkr_after_def)
done

lemma l3_skr_refines_skr:
  "{R23s} l2_skr R K, l3_skr R K {>R23s}"
apply (auto simp add: PO_rhoare_defs R23s_defs)
apply (auto simp add: l3_defs l2_skr_def)
done



lemmas l3_trans_refines_l2_trans = 
  l3_step1_refines_step1 l3_step2_refines_step2 l3_step3_refines_step3 l3_step4_refines_step4
  l3_dy_refines_dy_fake_msg_dy_fake_chan_skip
  l3_lkr_others_refines_lkr_others l3_lkr_after_refines_lkr_after l3_skr_refines_skr



lemma l3_refines_init_l2 [iff]:
  "init l3  R23s `` (init l2)"
by (auto simp add: R23s_defs l2_defs l3_def l3_init_def)

lemma l3_refines_trans_l2 [iff]:
  "{R23s  (UNIV × (l3_inv1  l3_inv2  l3_inv3  l3_inv4))} trans l2, trans l3 {> R23s}"
proof -
  let ?pre' = "R23s  (UNIV × (l3_inv5  l3_inv6  l3_inv7  l3_inv8  l3_inv9))"
  show ?thesis (is "{?pre} ?t1, ?t2 {>?post}")
  proof (rule relhoare_conseq_left)
    show "?pre  ?pre'"
      using l3_inv5_derived l3_inv6_derived l3_inv7_derived l3_inv8_derived l3_inv9_derived 
      by blast
  next 
    show "{?pre'} ?t1, ?t2 {> ?post}" 
      by (auto simp add: l2_def l3_def l2_trans_def l3_trans_def
               intro!: l3_trans_refines_l2_trans)
  qed
qed    

lemma PO_obs_consistent_R23s [iff]: 
  "obs_consistent R23s med23s l2 l3"
by (auto simp add: obs_consistent_def R23s_def med23s_def l2_defs)


lemma l3_refines_l2 [iff]:
  "refines 
     (R23s  
      (reach l2 × (l3_inv1  l3_inv2  l3_inv3  l3_inv4)))
     med23s l2 l3"
by (rule Refinement_using_invariants, auto)

lemma l3_implements_l2 [iff]:
  "implements med23s l2 l3"
by (rule refinement_soundness) (auto)


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

subsubsection ‹inv10: secrets contain no implementation material›
(**************************************************************************************************)

definition
  l3_inv10 :: "l3_state set"
where
  "l3_inv10  {s.
    secret s  payload
  }"

lemmas l3_inv10I = l3_inv10_def [THEN setc_def_to_intro, rule_format]
lemmas l3_inv10E = l3_inv10_def [THEN setc_def_to_elim, rule_format]
lemmas l3_inv10D = l3_inv10_def [THEN setc_def_to_dest, rule_format]

lemma l3_inv10_init [iff]: 
  "init l3  l3_inv10"
by (auto simp add: l3_def l3_init_def ik_init_def intro!:l3_inv10I)

lemma l3_inv10_trans [iff]:
  "{l3_inv10} trans l3 {> l3_inv10}"
apply (auto simp add: PO_hoare_defs l3_nostep_defs)
apply (auto simp add: l3_defs l3_inv10_def)
done

lemma PO_l3_inv10 [iff]: "reach l3  l3_inv10"
by (rule inv_rule_basic) (auto)

lemma l3_obs_inv10 [iff]: "oreach l3  l3_inv10"
by (auto simp add: oreach_def)



subsubsection ‹Partial secrecy›
(**************************************************************************************************)

text ‹We want to prove @{term "l3_secrecy"}, ie
  @{term "synth (analz (ik s))  secret s = {}"},
  but by refinement we only get @{term "l3_partial_secrecy"}: 
    @{term "dy_fake_msg (bad s) (payloadSet (ik s)) (abs (ik s))  secret s = {}"}.
  This is fine if secrets contain no implementation material.
  Then, by @{term "inv5"}, a message in @{term "synth (analz (ik s))"} is in
    @{term "dy_fake_msg (bad s) (payloadSet (ik s)) (abs (ik s))  -payload"},
  and @{term "l3_partial_secrecy"} proves it is not a secret.
›

definition
  l3_partial_secrecy :: "('a l3_state_scheme) set"
where
  "l3_partial_secrecy  {s. 
    dy_fake_msg (bad s) (ik s  payload) (abs (ik s))  secret s = {}
  }"


lemma l3_obs_partial_secrecy [iff]: "oreach l3  l3_partial_secrecy"
apply (rule external_invariant_translation [OF l2_obs_secrecy _ l3_implements_l2])
apply (auto simp add: med23s_def l2_secrecy_def l3_partial_secrecy_def)
done


subsubsection ‹Secrecy›
(**************************************************************************************************)

definition 
  l3_secrecy :: "('a l3_state_scheme) set"
where
  "l3_secrecy  l1_secrecy"

lemma l3_obs_inv5: "oreach l3  l3_inv5"
by (auto simp add: oreach_def)

lemma l3_obs_secrecy [iff]: "oreach l3  l3_secrecy"
apply (rule, frule l3_obs_inv5 [THEN [2] rev_subsetD], frule l3_obs_inv10 [THEN [2] rev_subsetD])
apply (auto simp add: med23s_def l2_secrecy_def l3_secrecy_def s0_secrecy_def l3_inv10_def)
using l3_partial_secrecy_def apply (blast dest!: l3_inv5D subsetD [OF l3_obs_partial_secrecy])
done

lemma l3_secrecy [iff]: "reach l3  l3_secrecy"
by (rule external_to_internal_invariant [OF l3_obs_secrecy], auto)


subsubsection ‹Injective agreement›
(**************************************************************************************************)

abbreviation "l3_iagreement_Init  l1_iagreement_Init"

lemma l3_obs_iagreement_Init [iff]: "oreach l3  l3_iagreement_Init"
apply (rule external_invariant_translation 
         [OF l2_obs_iagreement_Init _ l3_implements_l2])
apply (auto simp add: med23s_def l1_iagreement_Init_def)
done

lemma l3_iagreement_Init [iff]: "reach l3  l3_iagreement_Init"
by (rule external_to_internal_invariant [OF l3_obs_iagreement_Init], auto)

abbreviation "l3_iagreement_Resp  l1_iagreement_Resp"

lemma l3_obs_iagreement_Resp [iff]: "oreach l3  l3_iagreement_Resp"
apply (rule external_invariant_translation 
         [OF l2_obs_iagreement_Resp _ l3_implements_l2])
apply (auto simp add: med23s_def l1_iagreement_Resp_def)
done

lemma l3_iagreement_Resp [iff]: "reach l3  l3_iagreement_Resp"
by (rule external_to_internal_invariant [OF l3_obs_iagreement_Resp], auto)

end
end