Theory Infrastructure

section ‹Infrastructures›
text ‹The Isabelle Infrastructure framework supports the representation of infrastructures 
as graphs with actors and policies attached to nodes. These infrastructures 
are the {\it states} of the Kripke structure. 
The transition between states is triggered by non-parametrized
actions @{text ‹get, move, eval, put›} executed by actors. 
Actors are given by an abstract type @{text ‹actor›} and a function 
@{text ‹Actor›} that creates elements of that type from identities 
(of type @{text ‹string›}). Policies are given by pairs of predicates 
(conditions) and sets of (enabled) actions.›
subsection ‹Actors, actions, and data labels›
theory Infrastructure
  imports AT 
begin
datatype action = get | move | eval | put

typedecl actor 
type_synonym identity = string
consts Actor :: "string ⇒ actor"
type_synonym policy = "((actor ⇒ bool) * action set)"

definition ID :: "[actor, string] ⇒ bool"
  where "ID a s ≡ (a = Actor s)"
text ‹The Decentralised Label Model (DLM) \<^cite>‹"ml:98"› introduced the idea to
label data by owners and readers. We pick up this idea and formalize
a new type to encode the owner and the set of readers as a pair.
The first element is the owner of a data item, the second one is the
set of all actors that may access the data item.
This enables the unique security 
labelling of data within the system additionally taking the ownership into 
account.›
type_synonym data = nat  
type_synonym dlm = "actor * actor set"

subsection ‹Infrastructure graphs and policies›
text‹Actors are contained in an infrastructure graph. An @{text ‹igraph›} contains
a set of location pairs representing the topology of the infrastructure
as a graph of nodes and a list of actor identities associated to each node 
(location) in the graph.
Also an @{text ‹igraph›} associates actors to a pair of string sets by
a pair-valued function whose first range component is a set describing
the credentials in the possession of an actor and the second component
is a set defining the roles the actor can take on. More importantly in this 
context, an  @{text ‹igraph›} assigns locations to a pair of a string that defines
the state of the component and an element of type @{text ‹(dlm * data) set›}. This
set of labelled data may represent a condition on that data.
Corresponding projection functions for each of these components of an 
@{text ‹igraph›} are provided; they are named @{text ‹gra›} for the actual set of pairs of
locations, @{text ‹agra›} for the actor map, @{text ‹cgra›} for the credentials,
and @{text ‹lgra›} for the state of a location and the data at that location.›
datatype location = Location nat
  datatype igraph = Lgraph "(location * location)set" "location ⇒ identity set"
                           "actor ⇒ (string set * string set)"  
                           "location ⇒ string * (dlm * data) set"
datatype infrastructure = 
         Infrastructure "igraph" 
                        "[igraph, location] ⇒ policy set" 
                       
primrec loc :: "location ⇒ nat"
where  "loc(Location n) = n"
primrec gra :: "igraph ⇒ (location * location)set"
where  "gra(Lgraph g a c l) = g"
primrec agra :: "igraph ⇒ (location ⇒ identity set)"
where  "agra(Lgraph g a c l) = a"
primrec cgra :: "igraph ⇒ (actor ⇒ string set * string set)"
where  "cgra(Lgraph g a c l) = c"
primrec lgra :: "igraph ⇒ (location ⇒ string * (dlm * data) set)"
where  "lgra(Lgraph g a c l) = l"

definition nodes :: "igraph ⇒ location set" 
where "nodes g == { x. (? y. ((x,y): gra g) | ((y,x): gra g))}"

definition actors_graph :: "igraph ⇒ identity set"  
where  "actors_graph g == {x. ? y. y : nodes g ∧ x ∈ (agra g y)}"

text ‹There are projection functions text{@ ‹graphI›} and text{@ ‹delta›} when applied
to an infrastructure return the graph and the policy, respectively. Other projections
are introduced for the labels, the credential, and roles and to express their meaning.›
primrec graphI :: "infrastructure ⇒ igraph"
where "graphI (Infrastructure g d) = g"
primrec delta :: "[infrastructure, igraph, location] ⇒ policy set"
where "delta (Infrastructure g d) = d"
primrec tspace :: "[infrastructure, actor ] ⇒ string set * string set"
  where "tspace (Infrastructure g d) = cgra g"
primrec lspace :: "[infrastructure, location ] ⇒ string * (dlm * data)set"
where "lspace (Infrastructure g d) = lgra g"

definition credentials :: "string set * string set ⇒ string set"
  where  "credentials lxl ≡ (fst lxl)"
definition has :: "[igraph, actor * string] ⇒ bool"
  where "has G ac ≡ snd ac ∈ credentials(cgra G (fst ac))"
definition roles :: "string set * string set ⇒ string set"
  where  "roles lxl ≡ (snd lxl)"
definition role :: "[igraph, actor * string] ⇒ bool"
  where "role G ac ≡ snd ac ∈ roles(cgra G (fst ac))"
definition isin :: "[igraph,location, string] ⇒ bool" 
  where "isin G l s ≡ s = fst (lgra G l)"

text ‹Predicates and projections for the labels to encode their meaning.›
definition owner :: "dlm * data ⇒ actor" where "owner d ≡ fst(fst d)"
definition owns :: "[igraph, location, actor, dlm * data] ⇒ bool"
  where "owns G l a d ≡ owner d = a"
definition readers :: "dlm * data ⇒ actor set"
  where "readers d ≡ snd (fst d)"

text ‹The predicate @{text ‹has_access›} is true for owners or readers.› 
definition has_access :: "[igraph, location, actor, dlm * data] ⇒ bool"    
where "has_access G l a d ≡ owns G l a d ∨ a ∈ readers d"

(*
text ‹Actors can delete data.›
definition actor_can_delete ::   "[infrastructure, actor, location] ⇒ bool"
where actor_can_delete_def: "actor_can_delete I h l ≡  
                   (∀ as n. ((h, as), n) ∉ (snd (lgra (graphI I) l)))"
*)
text ‹We define a type of functions that preserves the security labeling and a 
   corresponding function application  operator.›  
typedef label_fun = "{f :: dlm * data ⇒ dlm * data. 
                        ∀ x:: dlm * data. fst x = fst (f x)}"  
  by (fastforce)

definition secure_process :: "label_fun ⇒ dlm * data ⇒ dlm * data" (infixr "⇕" 50)
  where "f  ⇕ d ≡ (Rep_label_fun f) d" 

(* This part is relevant to model Insiders but is not needed for Infrastructures.

datatype psy_states = happy | depressed | disgruntled | angry | stressed
datatype motivations = financial | political | revenge | curious | competitive_advantage | power | peer_recognition

datatype actor_state = Actor_state "psy_states" "motivations set"
primrec motivation :: "actor_state ⇒ motivations set" 
where "motivation  (Actor_state p m) =  m"
primrec psy_state :: "actor_state ⇒ psy_states" 
where "psy_state  (Actor_state p m) = p"

definition tipping_point :: "actor_state ⇒ bool" where
  "tipping_point a ≡ ((motivation a ≠ {}) ∧ (happy ≠ psy_state a))"

consts astate :: "identity ⇒ actor_state"

(* Two versions of an impersonation predicate "a can act as b". 
   The first one is stronger and allows substitution of the insider in any context; 
   the second one is parameterized over a context predicate to describe this.   *)
definition UasI ::  "[identity, identity] ⇒ bool " 
where "UasI a b ≡ (Actor a = Actor b) ∧ (∀ x y. x ≠ a ∧ y ≠ a ∧ Actor x = Actor y ⟶ x = y)"

definition UasI' ::  "[actor => bool, identity, identity] ⇒ bool " 
where "UasI' P a b ≡ P (Actor b) ⟶ P (Actor a)"

definition Insider :: "[identity, identity set] ⇒ bool" 
where "Insider a C ≡ (tipping_point (astate a) ⟶ (∀ b∈C. UasI a b))"

definition Insider' :: "[actor ⇒ bool, identity, identity set] ⇒ bool" 
where "Insider' P a C ≡ (tipping_point (astate a) ⟶ (∀ b∈C. UasI' P a b ∧ inj_on Actor C))"
*)

text ‹The predicate atI -- mixfix syntax @{text ‹@⇘G⇙›} -- expresses that an actor (identity) 
      is at a certain location in an igraph.›
definition atI :: "[identity, igraph, location] ⇒ bool" ("_ @⇘(_)⇙ _" 50)
where "a @⇘G⇙ l ≡ a ∈ (agra G l)"

text ‹Policies specify the expected behaviour of actors of an infrastructure. 
They are defined by the @{text ‹enables›} predicate:
an actor @{text ‹h›} is enabled to perform an action @{text ‹a›} 
in infrastructure @{text ‹I›}, at location @{text ‹l›}
if there exists a pair @{text ‹(p,e)›} in the local policy of @{text ‹l›}
(@{text ‹delta I l›} projects to the local policy) such that the action 
@{text ‹a›} is a member of the action set @{text ‹e›} and the policy 
predicate @{text ‹p›} holds for actor @{text ‹h›}.›
definition enables :: "[infrastructure, location, actor, action] ⇒ bool"
where
"enables I l a a' ≡  (∃ (p,e) ∈ delta I (graphI I) l. a' ∈ e ∧ p a)"

text ‹The behaviour is the good behaviour, i.e. everything allowed by the policy of infrastructure I.›
definition behaviour :: "infrastructure ⇒ (location * actor * action)set"
where "behaviour I ≡ {(t,a,a'). enables I t a a'}"

text ‹The misbehaviour is the complement of the behaviour of an infrastructure I.›
definition misbehaviour :: "infrastructure ⇒ (location * actor * action)set"
where "misbehaviour I ≡ -(behaviour I)"

subsection "State transition on infrastructures"
text ‹The state transition defines how actors may act on infrastructures through actions
    within the boundaries of the policy. It is given as an inductive definition over the 
    states which are infrastructures.  This state transition relation is dependent on actions but also on
    enabledness and the current state of the infrastructure.

    First we introduce some auxiliary functions dealing
    with repetitions in lists and actors moving in an igraph.›
primrec jonce :: "['a, 'a list] ⇒ bool"
where
jonce_nil: "jonce a [] = False" |
jonce_cons: "jonce a (x#ls) = (if x = a then (a ∉ (set ls)) else jonce a ls)"
(*
primrec nodup :: "['a, 'a list] ⇒ bool"
  where 
    nodup_nil: "nodup a [] = True" |
    nodup_step: "nodup a (x # ls) = (if x = a then (a ∉ (set ls)) else nodup a ls)"
*)
definition move_graph_a :: "[identity, location, location, igraph] ⇒ igraph"
where "move_graph_a n l l' g ≡ Lgraph (gra g) 
                    (if n ∈ ((agra g) l) &  n ∉ ((agra g) l') then 
                     ((agra g)(l := (agra g l) - {n}))(l' := (insert n (agra g l')))
                     else (agra g))(cgra g)(lgra g)"

inductive state_transition_in :: "[infrastructure, infrastructure] ⇒ bool" ("(_ →⇩n _)" 50)
where
  move: "⟦ G = graphI I; a @⇘G⇙ l; l ∈ nodes G; l' ∈ nodes G;
          (a) ∈ actors_graph(graphI I); enables I l' (Actor a) move;
         I' = Infrastructure (move_graph_a a l l' (graphI I))(delta I) ⟧ ⟹ I →⇩n I'" 
| get : "⟦ G = graphI I; a @⇘G⇙ l; a' @⇘G⇙ l; has G (Actor a, z);
        enables I l (Actor a) get;
        I' = Infrastructure 
                   (Lgraph (gra G)(agra G)
                           ((cgra G)(Actor a' := 
                                (insert z (fst(cgra G (Actor a'))), snd(cgra G (Actor a')))))
                           (lgra G))
                   (delta I)
         ⟧ ⟹ I →⇩n I'"
| get_data : "G = graphI I ⟹ a @⇘G⇙ l ⟹
        enables I l' (Actor a) get ⟹ 
       ((Actor a', as), n) ∈ snd (lgra G l') ⟹ Actor a ∈ as ⟹ 
        I' = Infrastructure 
                   (Lgraph (gra G)(agra G)(cgra G)
                   ((lgra G)(l := (fst (lgra G l), 
                                   snd (lgra G l)  ∪ {((Actor a', as), n)}))))
                   (delta I)
         ⟹ I →⇩n I'"
| process : "G = graphI I ⟹ a @⇘G⇙ l ⟹
        enables I l (Actor a) eval ⟹ 
       ((Actor a', as), n) ∈ snd (lgra G l) ⟹ Actor a ∈ as ⟹
        I' = Infrastructure 
                   (Lgraph (gra G)(agra G)(cgra G)
                   ((lgra G)(l := (fst (lgra G l), 
                    snd (lgra G l)  - {((Actor a', as), n)}
                    ∪ {(f :: label_fun) ⇕ ((Actor a', as), n)}))))
                   (delta I)
         ⟹ I →⇩n I'"  
| del_data : "G = graphI I ⟹ a ∈ actors G ⟹ l ∈ nodes G ⟹
       ((Actor a, as), n) ∈ snd (lgra G l) ⟹ 
        I' = Infrastructure 
                   (Lgraph (gra G)(agra G)(cgra G)
                   ((lgra G)(l := (fst (lgra G l), snd (lgra G l) - {((Actor a, as), n)}))))
                   (delta I)
         ⟹ I →⇩n I'"
| put : "G = graphI I ⟹ a @⇘G⇙ l ⟹ enables I l (Actor a) put ⟹
        I' = Infrastructure 
                  (Lgraph (gra G)(agra G)(cgra G)
                          ((lgra G)(l := (s, snd (lgra G l) ∪ {((Actor a, as), n)}))))
                   (delta I)
          ⟹ I →⇩n I'"

text ‹Note that the type infrastructure can now be instantiated to the axiomatic type class 
      @{text‹state›} which enables the use of the underlying Kripke structures and CTL.›
instantiation "infrastructure" :: state
begin
definition 
   state_transition_infra_def: "(i →⇩i i') =  (i →⇩n (i' :: infrastructure))"

instance
  by (rule state.intro_of_class)

definition state_transition_in_refl ("(_ →⇩n* _)" 50)
where "s →⇩n* s' ≡ ((s,s') ∈ {(x,y). state_transition_in x y}⇧*)"

end
      
lemma move_graph_eq: "move_graph_a a l l g = g"  
  by (simp add: move_graph_a_def, case_tac g, force)
     
end