Theory GDPRhealthcare

section ‹Application example from IoT healthcare› 
text ‹The  example of an IoT healthcare systems is taken from the context of the CHIST-ERA project
SUCCESS \<^cite>‹"suc:16"›.  In this system architecture, data is collected by sensors 
in the home or via a smart phone helping to monitor bio markers of the patient. The data 
collection is in a cloud based server to enable hospitals (or scientific institutions) 
to access the data which is controlled via the smart phone.
The identities Patient and Doctor represent patients
and their doctors; double quotes ''s'' indicate strings 
in Isabelle/HOL.
The global policy is `only the patient and the doctor can access the data in the cloud'.›
theory GDPRhealthcare
imports Infrastructure
begin
text ‹Local policies are represented as a function over an @{text ‹igraph G›} 
      that additionally assigns each location of a scenario to its local policy 
      given as a pair of requirements to an actor (first element of the pair) in 
      order to grant him actions in the location (second element of the pair). 
      The predicate @{text ‹@G›} checks whether an actor is at a given location 
       in the @{text ‹igraph G›}.›
locale scenarioGDPR = 
fixes gdpr_actors :: "identity set"
defines gdpr_actors_def: "gdpr_actors ≡ {''Patient'', ''Doctor''}"
fixes gdpr_locations :: "location set"
defines gdpr_locations_def: "gdpr_locations ≡ 
          {Location 0, Location 1, Location 2, Location 3}"
fixes sphone :: "location"
defines sphone_def: "sphone ≡ Location 0"
fixes home :: "location"
defines home_def: "home ≡ Location 1"
fixes hospital :: "location"
defines hospital_def: "hospital ≡ Location 2"
fixes cloud :: "location"
defines cloud_def: "cloud ≡ Location 3"
fixes global_policy :: "[infrastructure, identity] ⇒ bool"
defines global_policy_def: "global_policy I a ≡ a ≠ ''Doctor'' 
                 ⟶ ¬(enables I hospital (Actor a) eval)"
fixes global_policy' :: "[infrastructure, identity] ⇒ bool"
defines global_policy'_def: "global_policy' I a ≡ a ∉ gdpr_actors 
                 ⟶ ¬(enables I cloud (Actor a) get)"  
fixes ex_creds :: "actor ⇒ (string set * string set)"
defines ex_creds_def: "ex_creds ≡ (λ x. if x = Actor ''Patient'' then 
                         ({''PIN'',''skey''}, {}) else 
                            (if x = Actor ''Doctor'' then
                                ({''PIN''},{}) else ({},{})))"
fixes ex_locs :: "location ⇒ string * (dlm * data) set"
defines "ex_locs ≡ (λ x.  if x = cloud then
             (''free'',{((Actor ''Patient'',{Actor ''Doctor''}),42)}) 
             else ('''',{}))"
fixes ex_loc_ass :: "location ⇒ identity set"
defines ex_loc_ass_def: "ex_loc_ass ≡
          (λ x.  if x = home then {''Patient''}  
                 else (if x = hospital then {''Doctor'', ''Eve''} 
                       else {}))"
(* The nicer representation with case suffers from
   not so nice presentation in the cases (need to unfold the syntax)  
fixes ex_loc_ass_alt :: "location ⇒ identity set"
defines ex_loc_ass_alt_def: "ex_loc_ass_alt ≡
          (λ x.  (case x of 
             Location (Suc 0) ⇒ {''Patient''}  
           | Location (Suc (Suc 0)) ⇒ {''Doctor'', ''Eve''} 
           |  _ ⇒ {}))"
*)
fixes ex_graph :: "igraph"
defines ex_graph_def: "ex_graph ≡ Lgraph 
     {(home, cloud), (sphone, cloud), (cloud,hospital)}
     ex_loc_ass
     ex_creds ex_locs"
fixes ex_graph' :: "igraph"
defines ex_graph'_def: "ex_graph' ≡ Lgraph 
     {(home, cloud), (sphone, cloud), (cloud,hospital)}
       (λ x. if x = cloud then {''Patient''} else 
           (if x = hospital then {''Doctor'',''Eve''} else {})) 
     ex_creds ex_locs"
fixes ex_graph'' :: "igraph"
defines ex_graph''_def: "ex_graph'' ≡ Lgraph 
     {(home, cloud), (sphone, cloud), (cloud,hospital)}
       (λ x. if x = cloud then {''Patient'', ''Eve''} else 
           (if x = hospital then {''Doctor''} else {})) 
     ex_creds ex_locs"
(* Same as above: the nicer representation with case suffers from
   not so nice presentation in the cases (need to unfold the syntax) 
fixes local_policies_alt :: "[igraph, location] ⇒ policy set"
defines local_policies_alt_def: "local_policies_alt G ≡ 
    (λ x. case x of 
         Location (Suc 0) ⇒ {(λ y. True, {put,get,move,eval})}
       | Location 0 ⇒ {((λ y. has G (y, ''PIN'')), {put,get,move,eval})} 
       | Location (Suc (Suc (Suc 0))) ⇒ {(λ y. True, {put,get,move,eval})}
       | Location (Suc (Suc 0)) ⇒
                {((λ y. (∃ n. (n  @⇘G⇙ hospital) ∧ Actor n = y ∧ 
                           has G (y, ''skey''))), {put,get,move,eval})} 
       | _ ⇒  {})"
*)
fixes local_policies :: "[igraph, location] ⇒ policy set"
defines local_policies_def: "local_policies G ≡ 
    (λ x. if x = home then
        {(λ y. True, {put,get,move,eval})}
          else (if x = sphone then 
             {((λ y. has G (y, ''PIN'')), {put,get,move,eval})} 
                else (if x = cloud then
                {(λ y. True, {put,get,move,eval})}
                       else (if x = hospital then
                {((λ y. (∃ n. (n  @⇘G⇙ hospital) ∧ Actor n = y ∧ 
                           has G (y, ''skey''))), {put,get,move,eval})} else {}))))"
(* problems with case in locales?
defines local_policies_def: "local_policies G x ≡ 
     (case x of 
       home ⇒ {(λ y. True, {put,get,move,eval})}
     | sphone ⇒ {((λ y. has G (y, ''PIN'')), {put,get,move,eval})} 
     | cloud ⇒ {(λ y. True, {put,get,move,eval})}
     | hospital ⇒ {((λ y. (∃ n. (n  @⇘G⇙ hospital) ∧ Actor n = y ∧ 
                           has G (y, ''skey''))), {put,get,move,eval})} 
     | _ ⇒  {})"
*)
fixes gdpr_scenario :: "infrastructure"
defines gdpr_scenario_def:
"gdpr_scenario ≡ Infrastructure ex_graph local_policies"
fixes Igdpr :: "infrastructure set"
defines Igdpr_def:
  "Igdpr ≡ {gdpr_scenario}"
(* other states of scenario *)
(* First step: Patient goes onto cloud *)
fixes gdpr_scenario' :: "infrastructure"
defines gdpr_scenario'_def:
"gdpr_scenario' ≡ Infrastructure ex_graph' local_policies"
fixes GDPR' :: "infrastructure set"
defines GDPR'_def:
  "GDPR' ≡ {gdpr_scenario'}"
(* Second step: Eve goes onto cloud from where she'll be able to get the data *)
fixes gdpr_scenario'' :: "infrastructure"
defines gdpr_scenario''_def:
"gdpr_scenario'' ≡ Infrastructure ex_graph'' local_policies"
fixes GDPR'' :: "infrastructure set"
defines GDPR''_def:
  "GDPR'' ≡ {gdpr_scenario''}"
fixes gdpr_states
defines gdpr_states_def: "gdpr_states ≡ { I. gdpr_scenario →⇩i* I }"
fixes gdpr_Kripke
defines "gdpr_Kripke ≡ Kripke gdpr_states {gdpr_scenario}"
fixes sgdpr 
defines "sgdpr ≡ {x. ¬ (global_policy' x ''Eve'')}"  
begin
subsection ‹Using Attack Tree Calculus›
text ‹Since we consider a predicate transformer semantics, we use sets of states 
     to represent properties. For example, the attack property is given by the above
     @{text ‹set sgdpr›}.

The attack we are interested in is to see whether for the scenario

@{text ‹gdpr scenario ≡ Infrastructure ex_graph local_policies›}

from the initial state 

@{text ‹Igdpr ≡{gdpr scenario}›}, 

the critical state
@{text ‹sgdpr›} can be reached, i.e., is there a valid attack @{text ‹(Igdpr,sgdpr)›}?

We first present a number of lemmas showing single and multi-step state transitions
for relevant states reachable from our @{text ‹gdpr_scenario›}.›
lemma step1: "gdpr_scenario  →⇩n gdpr_scenario'"
proof (rule_tac l = home and a = "''Patient''" and l' = cloud in move)
  show "graphI gdpr_scenario = graphI gdpr_scenario" by (rule refl)
next show "''Patient'' @⇘graphI gdpr_scenario⇙ home" 
    by (simp add: gdpr_scenario_def ex_graph_def ex_loc_ass_def atI_def nodes_def)
next show "home ∈ nodes (graphI gdpr_scenario)"
    by (simp add: gdpr_scenario_def ex_graph_def ex_loc_ass_def atI_def nodes_def, blast)
next show "cloud ∈ nodes (graphI gdpr_scenario)"
    by (simp add: gdpr_scenario_def nodes_def ex_graph_def, blast)
next show "''Patient'' ∈ actors_graph (graphI gdpr_scenario)"
    by (simp add: actors_graph_def gdpr_scenario_def ex_graph_def ex_loc_ass_def nodes_def, blast)
next show "enables gdpr_scenario cloud (Actor ''Patient'') move"
    by (simp add: enables_def gdpr_scenario_def ex_graph_def local_policies_def
                    ex_creds_def ex_locs_def has_def credentials_def)
next show "gdpr_scenario' =
    Infrastructure (move_graph_a ''Patient'' home cloud (graphI gdpr_scenario)) (delta gdpr_scenario)"
    apply (simp add: gdpr_scenario'_def ex_graph'_def move_graph_a_def 
                     gdpr_scenario_def ex_graph_def home_def cloud_def hospital_def
                     ex_loc_ass_def ex_creds_def)
    apply (rule ext)
    by (simp add: hospital_def)
qed

lemma step1r: "gdpr_scenario  →⇩n* gdpr_scenario'"
proof (simp add: state_transition_in_refl_def)
  show " (gdpr_scenario, gdpr_scenario') ∈ {(x::infrastructure, y::infrastructure). x →⇩n y}⇧*"
  by (insert step1, auto)
qed

lemma step2: "gdpr_scenario'  →⇩n gdpr_scenario''"
proof (rule_tac l = hospital and a = "''Eve''" and l' = cloud in move, rule refl)
  show "''Eve'' @⇘graphI gdpr_scenario'⇙ hospital"
   by (simp add: gdpr_scenario'_def ex_graph'_def hospital_def cloud_def atI_def nodes_def)
next show "hospital ∈ nodes (graphI gdpr_scenario')"
    by (simp add: gdpr_scenario'_def ex_graph'_def hospital_def cloud_def atI_def nodes_def, blast)
next show "cloud ∈ nodes (graphI gdpr_scenario')"
    by (simp add: gdpr_scenario'_def nodes_def ex_graph'_def, blast)
next show "''Eve'' ∈ actors_graph (graphI gdpr_scenario')"
    by (simp add: actors_graph_def gdpr_scenario'_def ex_graph'_def nodes_def
                     hospital_def cloud_def, blast)
next show "enables gdpr_scenario' cloud (Actor ''Eve'') move"
    by (simp add: enables_def gdpr_scenario'_def ex_graph_def local_policies_def
                  ex_creds_def ex_locs_def has_def credentials_def cloud_def sphone_def)
next show "gdpr_scenario'' =
    Infrastructure (move_graph_a ''Eve'' hospital cloud (graphI gdpr_scenario')) (delta gdpr_scenario')"
    apply (simp add: gdpr_scenario'_def ex_graph''_def move_graph_a_def gdpr_scenario''_def 
                     ex_graph'_def home_def cloud_def hospital_def ex_creds_def)
    apply (rule ext)
    apply (simp add: hospital_def)
    by blast
qed

lemma step2r: "gdpr_scenario'  →⇩n* gdpr_scenario''"
proof (simp add: state_transition_in_refl_def)
  show "(gdpr_scenario', gdpr_scenario'') ∈ {(x::infrastructure, y::infrastructure). x →⇩n y}⇧*"
    by (insert step2, auto)
qed
     
(* Attack example: Eve can get onto cloud and get Patient's data 
   because the policy allows Eve to get on cloud.
   This attack can easily be fixed by disabling Eve to "get"
   in the policy (just change the "True" for cloud to a set with no 
   Eve in it).
   However, it would not prevent Insider attacks (where Eve is 
   impersonating the Doctor, for example). Insider attacks can
   be checked using the UasI predicate.
*)
text ‹For the Kripke structure

@{text ‹gdpr_Kripke ≡ Kripke { I. gdpr_scenario →⇩i* I } {gdpr_scenario}›}

we first derive a valid and-attack using the attack tree proof calculus.

@{text ‹"⊢[𝒩⇘(Igdpr,GDPR')⇙, 𝒩⇘(GDPR',sgdpr)⇙] ⊕⇩∧⇗(Igdpr,sgdpr)⇖›}

The set @{text ‹GDPR'›} (see above) is an intermediate state where Eve accesses the cloud.›

lemma gdpr_ref: "[𝒩⇘(Igdpr,sgdpr)⇙] ⊕⇩∧⇗(Igdpr,sgdpr)⇖ ⊑
                  ([𝒩⇘(Igdpr,GDPR')⇙, 𝒩⇘(GDPR',sgdpr)⇙] ⊕⇩∧⇗(Igdpr,sgdpr)⇖)"  
proof (rule_tac l = "[]" and l' = "[𝒩⇘(Igdpr,GDPR')⇙, 𝒩⇘(GDPR',sgdpr)⇙]" and
                  l'' = "[]" and si = Igdpr and si' = Igdpr and 
                  si'' = sgdpr and si''' = sgdpr in refI, simp, rule refl)
  show "([𝒩⇘(Igdpr, GDPR')⇙, 𝒩⇘(GDPR', sgdpr)⇙] ⊕⇩∧⇗(Igdpr, sgdpr)⇖) =
    ([] @ [𝒩⇘(Igdpr, GDPR')⇙, 𝒩⇘(GDPR', sgdpr)⇙] @ [] ⊕⇩∧⇗(Igdpr, sgdpr)⇖)"
  by simp
qed

lemma att_gdpr: "⊢([𝒩⇘(Igdpr,GDPR')⇙, 𝒩⇘(GDPR',sgdpr)⇙] ⊕⇩∧⇗(Igdpr,sgdpr)⇖)"
proof (subst att_and, simp, rule conjI)
  show " ⊢𝒩⇘(Igdpr, GDPR')⇙"
    apply (simp add: Igdpr_def GDPR'_def att_base)
    using state_transition_infra_def step1 by blast
next 
  have "¬ global_policy' gdpr_scenario'' ''Eve''" "gdpr_scenario' →⇩n gdpr_scenario''"
      using step2
      by (auto simp: global_policy'_def gdpr_scenario''_def gdpr_actors_def 
                      enables_def local_policies_def cloud_def sphone_def intro!: step2)
  then show "⊢([𝒩⇘(GDPR', sgdpr)⇙] ⊕⇩∧⇗(GDPR', sgdpr)⇖)"
    apply (subst att_and)
    apply (simp add: GDPR'_def sgdpr_def att_base)
    using state_transition_infra_def by blast
qed

lemma gdpr_abs_att: "⊢⇩V([𝒩⇘(Igdpr,sgdpr)⇙] ⊕⇩∧⇗(Igdpr,sgdpr)⇖)"
  by (rule ref_valI, rule gdpr_ref, rule att_gdpr)

text ‹We can then simply apply the Correctness theorem @{text ‹AT EF›} to immediately 
      prove the following CTL statement.

      @{text ‹gdpr_Kripke ⊢ EF sgdpr›}

This application of the meta-theorem of Correctness of attack trees saves us
proving the CTL formula tediously by exploring the state space.›
lemma gdpr_att: "gdpr_Kripke ⊢ EF {x. ¬(global_policy' x ''Eve'')}"
proof -
  have a: " ⊢([𝒩⇘(Igdpr, GDPR')⇙, 𝒩⇘(GDPR', sgdpr)⇙] ⊕⇩∧⇗(Igdpr, sgdpr)⇖)"
    by (rule att_gdpr)
  hence "(Igdpr,sgdpr) = attack ([𝒩⇘(Igdpr, GDPR')⇙, 𝒩⇘(GDPR', sgdpr)⇙] ⊕⇩∧⇗(Igdpr, sgdpr)⇖)"
    by simp
  hence "Kripke {s::infrastructure. ∃i::infrastructure∈Igdpr. i →⇩i* s} Igdpr ⊢ EF sgdpr"
    using ATV_EF gdpr_abs_att by fastforce 
  thus "gdpr_Kripke ⊢ EF {x::infrastructure. ¬ global_policy' x ''Eve''}"
    by (simp add: gdpr_Kripke_def gdpr_states_def Igdpr_def sgdpr_def)
qed

theorem gdpr_EF: "gdpr_Kripke ⊢ EF sgdpr"
  using gdpr_att sgdpr_def by blast 

text ‹Similarly, vice-versa, the CTL statement proved in @{text ‹gdpr_EF›}
    can now be directly translated into Attack Trees using the Completeness 
    Theorem\footnote{This theorem could easily 
    be proved as a direct instance of @{text ‹att_gdpr›} above but we want to illustrate
    an alternative proof method using Completeness here.}.›
theorem gdpr_AT: "∃ A. ⊢ A ∧ attack A = (Igdpr,sgdpr)"
proof -
  have a: "gdpr_Kripke ⊢ EF sgdpr " by (rule gdpr_EF)
  have b: "Igdpr ≠ {}" by (simp add: Igdpr_def)
  thus "∃A::infrastructure attree. ⊢A ∧ attack A = (Igdpr, sgdpr)" 
  proof (rule Completeness)
    show "Kripke {s. ∃i∈Igdpr. i →⇩i* s} Igdpr ⊢ EF sgdpr"
      using a by (simp add: gdpr_Kripke_def Igdpr_def gdpr_states_def)
  qed (auto simp: Igdpr_def)
qed

text ‹Conversely, since we have an attack given by rule @{text ‹gdpr_AT›}, we can immediately 
   infer @{text ‹EF s›} using Correctness @{text ‹AT_EF›}\footnote{Clearly, this theorem is identical
   to @{text ‹gdpr_EF›} and could thus be inferred from that one but we want to show here an 
   alternative way of proving it using the Correctness theorem @{text ‹AT_EF›}.}.›
theorem gdpr_EF': "gdpr_Kripke ⊢ EF sgdpr"
  using gdpr_AT by (auto simp: gdpr_Kripke_def gdpr_states_def Igdpr_def dest: AT_EF)


(* However, when integrating DLM into the model and hence labeling
   information becomes part of the conditions of the get_data rule this isn't
   possible any more: gdpr_EF is not true any more *)    
(** GDPR properties  for the illustration of the DLM labeling **)    
section ‹Data Protection by Design for GDPR compliance›
subsection ‹General Data Protection Regulation (GDPR)›
text ‹Since 26th May 2018, the GDPR has become mandatory within the European Union and hence 
also for any supplier of IT products. Breaches of the regulation will be fined with penalties 
of 20 Million EUR. Despite the relatively large size of the document of 209 pages, the technically 
relevant portion for us is only about 30 pages (Pages 81--111, Chapters I to Chapter III, Section 3). 
In summary, Chapter III specifies that the controller must give the data subject read access (1) 
to any information, communications, and ``meta-data'' of the data, e.g., retention time and purpose. 
In addition, the system must enable deletion of data (2) and restriction of processing.
An invariant condition for data processing resulting from these Articles is that the system functions 
must preserve any of the access rights of personal data (3).

Using labeled data, we can now express the essence of Article 4 Paragraph (1): 
`personal data' means any information relating to an identified or identifiable natural 
person (`data subject').

The labels of data must not be changed by processing: we have identified this  as 
an invariant (3) resulting from the GDPR above. This invariant is formalized in 
our Isabelle model by the type definition of functions on labeled data @{text ‹label_fun›}
(see Section 4.2) that preserve the data labels.›

subsection ‹Policy enforcement and privacy preservation›
text ‹We can now use the labeled data to encode the privacy constraints of the 
    GDPR in the rules. For example, the get data rule (see Section 4.3) has labelled data 
    @{text ‹((Actor a', as), n)›} and uses the labeling in the precondition to guarantee 
    that only entitled users can get data.

We can prove that processing preserves ownership as defined in the initial state for all paths 
globally (AG) within the Kripke structure and in all locations of the graph.›
(* GDPR three: Processing preserves ownership in any location *)    
lemma gdpr_three: "h ∈ gdpr_actors ⟹ l ∈ gdpr_locations ⟹
         owns (Igraph gdpr_scenario) l (Actor h) d ⟹
         gdpr_Kripke ⊢ AG {x. ∀ l ∈ gdpr_locations. owns (Igraph x) l (Actor h) d }"  
proof (simp add: gdpr_Kripke_def check_def, rule conjI)
  show "gdpr_scenario ∈ gdpr_states" by (simp add: gdpr_states_def state_transition_refl_def)
next 
  show "h ∈ gdpr_actors ⟹
    l ∈ gdpr_locations ⟹
    owns (Igraph gdpr_scenario) l (Actor h) d ⟹
    gdpr_scenario ∈ AG {x::infrastructure. ∀l∈gdpr_locations. owns (Igraph x) l (Actor h) d}"
    apply (simp add: AG_def gfp_def)
    apply (rule_tac x = "{x::infrastructure. ∀l∈gdpr_locations. owns (Igraph x) l (Actor h) d}" in exI)
    by (auto simp: AX_def gdpr_scenario_def owns_def)
qed

text ‹The final application example of Correctness contraposition 
   shows that there is no attack to ownership possible.
The proved meta-theory for attack trees can be applied to facilitate the proof. 
The contraposition of the Correctness property grants that if there is no attack on 
@{text ‹(I,¬f)›}, then @{text ‹(EF ¬f)›} does not hold in the Kripke structure. This 
yields the theorem since the @{text ‹AG f›} statement corresponds to @{text ‹¬(EF ¬f)›}.
›
theorem no_attack_gdpr_three: 
"h ∈ gdpr_actors ⟹ l ∈ gdpr_locations ⟹ 
 owns (Igraph gdpr_scenario) l (Actor h) d ⟹
attack A = (Igdpr, -{x. ∀ l ∈ gdpr_locations. owns (Igraph x) l (Actor h) d })
⟹ ¬ (⊢ A)"
proof (rule_tac I = Igdpr and 
           s = "-{x::infrastructure. ∀l∈gdpr_locations. owns (Igraph x) l (Actor h) d}" 
       in contrapos_corr)
  show "h ∈ gdpr_actors ⟹
    l ∈ gdpr_locations ⟹
    owns (Igraph gdpr_scenario) l (Actor h) d ⟹
    attack A = (Igdpr, - {x::infrastructure. ∀l∈gdpr_locations. owns (Igraph x) l (Actor h) d}) ⟹
    ¬ (Kripke {s::infrastructure. ∃i::infrastructure∈Igdpr. i →⇩i* s}
        Igdpr ⊢ EF (- {x::infrastructure. ∀l∈gdpr_locations. owns (Igraph x) l (Actor h) d}))"
    apply (rule AG_imp_notnotEF) 
     apply (simp add: gdpr_Kripke_def Igdpr_def gdpr_states_def)
    using Igdpr_def gdpr_Kripke_def gdpr_states_def gdpr_three by auto
qed
end
end