Quelle  Service.thy

(*****************************************************************************
 * HOL-TestGen --- theorem-prover based test case generation
 *                 http://www.brucker.ch/projects/hol-testgen/
 *
 * This file is part of HOL-TestGen.
 *
 * Copyright (c) 2010-2012 ETH Zurich, Switzerland
 *               2010-2015 Achim D. Brucker, Germany
 *               2010-2017 Université Paris-Sud, France
 *               2015-2017 The Univeristy of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

section ‹Secure Service Specification›
theory 
  Service
  imports 
    UPF
begin
text ‹
 In this section, we model a simple Web service and its access control model
 that allows the staff in a hospital to access health care records of patients.
 ›

subsection‹Datatypes for Modelling Users and Roles›
subsubsection ‹Users›
text‹
 First, we introduce a type for users that we use to model that each
 staff member has a unique id:
 ›
type_synonym user = int  (* Each NHS employee has a unique NHS_ID. *)

text ‹
 Similarly, each patient has a unique id:
 ›
type_synonym patient = int (* Each patient gets a unique id *)

subsubsection ‹Roles and Relationships›
text‹In our example, we assume three different roles for members of the clinical staff:›

datatype role =  ClinicalPractitioner | Nurse | Clerical 

text‹
 We model treatment relationships (legitimate relationships) between staff and patients
 (respectively, their health records. This access control model is inspired by our detailed
 NHS model.
 ›     
type_synonym lr_id = int
type_synonym LR    = "lr_id ⇀ (user set)"
  
text‹The security context stores all the existing LRs.›
type_synonym Σ = "patient ⇀ LR"
  
text‹The user context stores the roles the users are in.›
type_synonym υ = "user ⇀ role"
  
subsection ‹Modelling Health Records and the Web Service API›
subsubsection ‹Health Records›
text ‹The content and the status of the entries of a health record›
datatype data         = dummyContent 
datatype status       = Open | Closed
type_synonym entry_id = int
type_synonym entry    = "status × user × data"
type_synonym SCR      = "(entry_id ⇀ entry)"
type_synonym DB       = "patient ⇀ SCR"

subsubsection ‹The Web Service API›
text‹The operations provided by the service:›
datatype Operation = createSCR user role patient  
                   | appendEntry user role patient entry_id entry
                   | deleteEntry user role patient entry_id  
                   | readEntry user role patient entry_id
                   | readSCR user role patient
                   | addLR user role patient lr_id "(user set)"
                   | removeLR user role patient lr_id
                   | changeStatus user role patient entry_id status
                   | deleteSCR user role patient 
                   | editEntry user role patient entry_id entry

fun is_createSCR where
 "is_createSCR (createSCR u r p) = True"
|"is_createSCR x = False"

fun is_appendEntry where
  "is_appendEntry (appendEntry u r p e ei) = True"
 |"is_appendEntry x = False" 

fun is_deleteEntry where
  "is_deleteEntry (deleteEntry u r p e_id) = True"
 |"is_deleteEntry x = False"

fun is_readEntry where
  "is_readEntry (readEntry u r p e) = True"
 |"is_readEntry x = False"

fun is_readSCR where
  "is_readSCR (readSCR u r p) = True"
 |"is_readSCR x = False"

fun is_changeStatus where
  "is_changeStatus (changeStatus u r p s ei) = True"
 |"is_changeStatus x = False"

fun is_deleteSCR where
  "is_deleteSCR (deleteSCR u r p) = True"
 |"is_deleteSCR x = False"

fun is_addLR where
  "is_addLR (addLR u r lrid lr us) = True"
 |"is_addLR x = False"

fun is_removeLR where
  "is_removeLR (removeLR u r p lr) = True"
 |"is_removeLR x = False"

fun is_editEntry where
  "is_editEntry (editEntry u r p e_id s) = True"
 |"is_editEntry x = False"

fun SCROp :: "(Operation × DB) ⇀ SCR" where
   "SCROp ((createSCR u r p), S) = S p"
  |"SCROp ((appendEntry u r p ei e), S) = S p"
  |"SCROp ((deleteEntry u r p e_id), S) = S p"
  |"SCROp ((readEntry u r p e), S) = S p"
  |"SCROp ((readSCR u r p), S) = S p"
  |"SCROp ((changeStatus u r p s ei),S) = S p"
  |"SCROp ((deleteSCR u r p),S) = S p"
  |"SCROp ((editEntry u r p e_id s),S) = S p"
  |"SCROp x = ⊥"

fun patientOfOp :: "Operation ==> patient" where
   "patientOfOp (createSCR u r p) = p"
  |"patientOfOp (appendEntry u r p e ei) = p"
  |"patientOfOp (deleteEntry u r p e_id) = p"
  |"patientOfOp (readEntry u r p e) = p"
  |"patientOfOp (readSCR u r p) = p"
  |"patientOfOp (changeStatus u r p s ei) = p"
  |"patientOfOp (deleteSCR u r p) = p"
  |"patientOfOp (addLR u r p lr ei) = p"
  |"patientOfOp (removeLR u r p lr) = p"
  |"patientOfOp (editEntry u r p e_id s) = p"

fun userOfOp :: "Operation ==> user" where
   "userOfOp (createSCR u r p) = u"
  |"userOfOp (appendEntry u r p e ei) = u"
  |"userOfOp (deleteEntry u r p e_id) = u"
  |"userOfOp (readEntry u r p e) = u"
  |"userOfOp (readSCR u r p) = u"
  |"userOfOp (changeStatus u r p s ei) = u"
  |"userOfOp (deleteSCR u r p) = u"
  |"userOfOp (editEntry u r p e_id s) = u"
  |"userOfOp (addLR u r p lr ei) = u"
  |"userOfOp (removeLR u r p lr) = u"

fun roleOfOp :: "Operation ==> role" where
   "roleOfOp (createSCR u r p) = r"
  |"roleOfOp (appendEntry u r p e ei) = r"
  |"roleOfOp (deleteEntry u r p e_id) = r"
  |"roleOfOp (readEntry u r p e) = r"
  |"roleOfOp (readSCR u r p) = r"
  |"roleOfOp (changeStatus u r p s ei) = r"
  |"roleOfOp (deleteSCR u r p) = r"
  |"roleOfOp (editEntry u r p e_id s) = r"
  |"roleOfOp (addLR u r p lr ei) = r"
  |"roleOfOp (removeLR u r p lr) = r"

fun contentOfOp :: "Operation ==> data" where
   "contentOfOp (appendEntry u r p ei e) = (snd (snd e))"
  |"contentOfOp (editEntry u r p ei e) = (snd (snd e))"

fun contentStatic :: "Operation ==> bool" where
   "contentStatic (appendEntry u r p ei e) = ((snd (snd e)) = dummyContent)"
  |"contentStatic (editEntry u r p ei e) = ((snd (snd e)) = dummyContent)"
  |"contentStatic x = True"

fun allContentStatic where 
   "allContentStatic (x#xs) = (contentStatic x ∧ allContentStatic xs)"
  |"allContentStatic [] = True"


subsection‹Modelling Access Control›
text ‹
 In the following, we define a rather complex access control model for our
 scenario that extends traditional role-based access control
 (RBAC)~cite‹"sandhu.ea:role-based:1996"› with treatment relationships and sealed
 envelopes. Sealed envelopes (see~cite‹"bruegger:generation:2012"› for details)
 are a variant of break-the-glass access control (see~cite‹"brucker.ea:extending:2009"›
 for a general motivation and explanation of break-the-glass access control).
 ›

subsubsection ‹Sealed Envelopes›

type_synonym SEPolicy = "(Operation × DB ↦ unit) "

definition get_entry:: "DB ==> patient ==> entry_id ==> entry option" where
 "get_entry S p e_id = (case S p of ⊥ ==> ⊥
                                    | ⌊Scr⌋ ==> Scr e_id)"

definition userHasAccess:: "user ==> entry ==> bool" where
 "userHasAccess u e = ((fst e) = Open ∨ (fst (snd e) = u))"

definition readEntrySE :: SEPolicy where
 "readEntrySE x = (case x of (readEntry u r p e_id,S) ==> (case get_entry S p e_id of
                                                            ⊥ ==> ⊥
                                                          | ⌊e⌋ ==> (if (userHasAccess u e)
                                                                     then ⌊allow ()⌋
                                                                     else ⌊deny ()⌋ ))
                            | x ==> ⊥)"

definition deleteEntrySE :: SEPolicy where
 "deleteEntrySE x = (case x of (deleteEntry u r p e_id,S) ==> (case get_entry S p e_id of
                                                                ⊥ ==> ⊥
                                                              | ⌊e⌋ ==> (if (userHasAccess u e)
                                                                       then ⌊allow ()⌋
                                                                       else ⌊deny ()⌋))
                              | x ==> ⊥)"

definition editEntrySE :: SEPolicy where
 "editEntrySE x = (case x of (editEntry u r p e_id s,S) ==> (case get_entry S p e_id of
                                                               ⊥ ==> ⊥
                                                             | ⌊e⌋ ==> (if (userHasAccess u e)
                                                                      then ⌊allow ()⌋
                                                                      else ⌊deny ()⌋))
                            | x ==> ⊥)"
  
definition SEPolicy :: SEPolicy where
 "SEPolicy = editEntrySE ⨁ deleteEntrySE ⨁ readEntrySE ⨁ A_U"
  

lemmas SEsimps = SEPolicy_def get_entry_def userHasAccess_def
                 editEntrySE_def deleteEntrySE_def readEntrySE_def

subsubsection ‹Legitimate Relationships›

type_synonym LRPolicy = "(Operation × Σ, unit) policy"

fun hasLR:: "user ==> patient ==> Σ ==> bool"  where
 "hasLR u p Σ = (case Σ p of ⊥ ==> False
                           | ⌊lrs⌋ ==> (∃lr. lr∈(ran lrs) ∧ u ∈ lr))"

definition LRPolicy :: LRPolicy where 
 "LRPolicy = (λ(x,y). (if hasLR (userOfOp x) (patientOfOp x) y
                       then ⌊allow ()⌋
                       else ⌊deny ()⌋))"

definition createSCRPolicy :: LRPolicy where
 "createSCRPolicy x = (if (is_createSCR (fst x))
                       then ⌊allow ()⌋
                       else ⊥)"

definition addLRPolicy :: LRPolicy where
 "addLRPolicy x = (if (is_addLR (fst x))
                   then ⌊allow ()⌋
                   else ⊥)"

definition LR_Policy where  "LR_Policy = createSCRPolicy ⨁ addLRPolicy ⨁ LRPolicy ⨁ A_U"

lemmas LRsimps = LR_Policy_def createSCRPolicy_def addLRPolicy_def LRPolicy_def

type_synonym FunPolicy = "(Operation × DB × Σ,unit) policy" 

fun createFunPolicy :: FunPolicy where
   "createFunPolicy ((createSCR u r p),(D,S)) = (if p ∈ dom D
                                                 then ⌊deny ()⌋
                                                 else ⌊allow ()⌋)"
  |"createFunPolicy x = ⊥"

fun addLRFunPolicy :: FunPolicy where
   "addLRFunPolicy ((addLR u r p l us),(D,S)) = (if l ∈ dom S
                                                 then ⌊deny ()⌋
                                                 else ⌊allow ()⌋)"
  |"addLRFunPolicy x = ⊥"

fun removeLRFunPolicy :: FunPolicy where
   "removeLRFunPolicy ((removeLR u r p l),(D,S)) = (if l ∈ dom S
                                                    then ⌊allow ()⌋
                                                    else ⌊deny ()⌋)"
  |"removeLRFunPolicy x = ⊥"

fun readSCRFunPolicy :: FunPolicy where
   "readSCRFunPolicy ((readSCR u r p),(D,S)) = (if p ∈ dom D
                                                then ⌊allow ()⌋
                                                else ⌊deny ()⌋)"
  |"readSCRFunPolicy x = ⊥"

fun deleteSCRFunPolicy :: FunPolicy where
   "deleteSCRFunPolicy ((deleteSCR u r p),(D,S)) = (if p ∈ dom D
                                                    then ⌊allow ()⌋
                                                    else ⌊deny ()⌋)"
  |"deleteSCRFunPolicy x = ⊥"

fun changeStatusFunPolicy  :: FunPolicy where
   "changeStatusFunPolicy (changeStatus u r p e s,(d,S)) =
          (case d p of ⌊x⌋ ==> (if e ∈ dom x
                                  then ⌊allow ()⌋
                                  else ⌊deny ()⌋)
                     | _ ==> ⌊deny ()⌋)" 
  |"changeStatusFunPolicy x = ⊥"

fun deleteEntryFunPolicy  :: FunPolicy where
   "deleteEntryFunPolicy (deleteEntry u r p e,(d,S)) =
          (case d p of ⌊x⌋ ==> (if e ∈ dom x
                                  then ⌊allow ()⌋
                                  else ⌊deny ()⌋)
                     | _ ==> ⌊deny ()⌋)" 
  |"deleteEntryFunPolicy x = ⊥"

fun readEntryFunPolicy :: FunPolicy where
   "readEntryFunPolicy (readEntry u r p e,(d,S)) =
          (case d p of ⌊x⌋ ==> (if e ∈ dom x
                                   then ⌊allow ()⌋
                                   else ⌊deny ()⌋)
                      | _ ==> ⌊deny ()⌋)" 
  |"readEntryFunPolicy x = ⊥"

fun appendEntryFunPolicy  :: FunPolicy where
   "appendEntryFunPolicy (appendEntry u r p e ed,(d,S)) =
          (case d p of ⌊x⌋ ==> (if e ∈ dom x
                                   then ⌊deny ()⌋
                                   else ⌊allow ()⌋)
                      | _ ==> ⌊deny ()⌋)" 
  |"appendEntryFunPolicy x = ⊥"

fun editEntryFunPolicy  :: FunPolicy where
   "editEntryFunPolicy (editEntry u r p ei e,(d,S)) =
               (case d p of ⌊x⌋ ==> (if ei ∈ dom x
                                       then ⌊allow ()⌋
                                       else ⌊deny ()⌋)
                          | _ ==> ⌊deny ()⌋)" 
  |"editEntryFunPolicy x = ⊥"

definition FunPolicy where 
 "FunPolicy = editEntryFunPolicy ⨁ appendEntryFunPolicy ⨁
              readEntryFunPolicy ⨁ deleteEntryFunPolicy ⨁
              changeStatusFunPolicy ⨁ deleteSCRFunPolicy ⨁
              removeLRFunPolicy ⨁ readSCRFunPolicy ⨁
              addLRFunPolicy ⨁ createFunPolicy ⨁ A_U"

subsubsection‹Modelling Core RBAC›

type_synonym RBACPolicy = "Operation × υ ↦ unit"

definition RBAC :: "(role × Operation) set" where 
 "RBAC = {(r,f). r = Nurse ∧ is_readEntry f} ∪
        {(r,f). r = Nurse ∧ is_readSCR f} ∪
        {(r,f). r = ClinicalPractitioner ∧ is_appendEntry f} ∪
        {(r,f). r = ClinicalPractitioner ∧ is_deleteEntry f} ∪
        {(r,f). r = ClinicalPractitioner ∧ is_readEntry f} ∪
        {(r,f). r = ClinicalPractitioner ∧ is_readSCR f} ∪
        {(r,f). r = ClinicalPractitioner ∧ is_changeStatus f} ∪
        {(r,f). r = ClinicalPractitioner ∧ is_editEntry f} ∪
        {(r,f). r = Clerical ∧ is_createSCR f} ∪
        {(r,f). r = Clerical ∧ is_deleteSCR f} ∪
        {(r,f). r = Clerical ∧ is_addLR f} ∪
        {(r,f). r = Clerical ∧ is_removeLR f}"

definition RBACPolicy :: RBACPolicy where
 "RBACPolicy = (λ (f,uc).
     if ((roleOfOp f,f) ∈ RBAC ∧ ⌊roleOfOp f⌋ = uc (userOfOp f))
     then ⌊allow ()⌋
     else ⌊deny ()⌋)"

subsection ‹The State Transitions and Output Function›

subsubsection‹State Transition›

fun OpSuccessDB :: "(Operation × DB) ⇀ DB"  where
   "OpSuccessDB (createSCR u r p,S) = (case S p of ⊥ ==> ⌊S(p↦∅)⌋
                                                 | ⌊x⌋ ==> ⌊S⌋)" 
  |"OpSuccessDB ((appendEntry u r p ei e),S) =
                                      (case S p of ⊥ ==> ⌊S⌋
                                                | ⌊x⌋ ==> ((if ei ∈ (dom x)
                                                              then ⌊S⌋
                                                              else ⌊S(p ↦ x(ei↦e))⌋)))"
  |"OpSuccessDB ((deleteSCR u r p),S) = (Some (S(p:=⊥)))"
  |"OpSuccessDB ((deleteEntry u r p ei),S) =
                                      (case S p of ⊥ ==> ⌊S⌋
                                                 | ⌊x⌋ ==> Some (S(p↦(x(ei:=⊥)))))"
  |"OpSuccessDB ((changeStatus u r p ei s),S) =
                                      (case S p of ⊥ ==> ⌊S⌋
                                                 | ⌊x⌋ ==> (case x ei of
                                                            ⌊e⌋ ==> ⌊S(p ↦ x(ei↦(s,snd e)))⌋
                                                          | ⊥ ==> ⌊S⌋))"
  |"OpSuccessDB ((editEntry u r p ei e),S) =
                                      (case S p of ⊥ ==>⌊S⌋
                                                 | ⌊x⌋ ==> (case x ei of
                                                                 ⌊e⌋ ==> ⌊S(p↦(x(ei↦(e))))⌋
                                                              | ⊥ ==> ⌊S⌋))"
  |"OpSuccessDB (x,S) = ⌊S⌋"


fun OpSuccessSigma :: "(Operation × Σ) ⇀ Σ" where
   "OpSuccessSigma (addLR u r p lr_id us,S) =
                   (case S p of ⌊lrs⌋ ==> (case (lrs lr_id) of
                                               ⊥ ==> ⌊S(p↦(lrs(lr_id↦us)))⌋
                                             | ⌊x⌋ ==> ⌊S⌋)
                              | ⊥ ==> ⌊S(p↦(Map.empty(lr_id↦us)))⌋)"
  |"OpSuccessSigma (removeLR u r p lr_id,S) =
                   (case S p of Some lrs ==> ⌊S(p↦(lrs(lr_id:=⊥)))⌋
                              | ⊥ ==> ⌊S⌋)"
  |"OpSuccessSigma (x,S) = ⌊S⌋"



fun OpSuccessUC :: "(Operation × υ) ⇀ υ" where
   "OpSuccessUC (f,u) = ⌊u⌋"

subsubsection ‹Output›

type_synonym Output = unit  

fun OpSuccessOutput :: "(Operation) ⇀ Output" where 
   "OpSuccessOutput x = ⌊()⌋"
 

fun OpFailOutput :: "Operation ⇀ Output" where
   "OpFailOutput x = ⌊()⌋"

subsection ‹Combine All Parts›

definition SE_LR_Policy :: "(Operation × DB × Σ, unit) policy" where
   "SE_LR_Policy = (λ(x,x). x) o_f (SEPolicy ⨂_\<or>_D LR_Policy) o (λ(a,b,c). ((a,b),a,c))"

definition SE_LR_FUN_Policy :: "(Operation × DB × Σ, unit) policy" where
  "SE_LR_FUN_Policy = ((λ(x,x). x) o_f (FunPolicy ⨂_\<or>_D SE_LR_Policy) o (λa. (a,a)))"

definition SE_LR_RBAC_Policy :: "(Operation × DB × Σ × υ, unit) policy" where
  "SE_LR_RBAC_Policy = (λ(x,x). x)
                        o_f (RBACPolicy ⨂_\<or>_D SE_LR_FUN_Policy)
                        o (λ(a,b,c,d). ((a,d),(a,b,c)))"

definition ST_Allow :: "Operation × DB × Σ × υ ⇀ Output × DB × Σ × υ" 
where     "ST_Allow = ((OpSuccessOutput ⨂_M (OpSuccessDB ⨂_S OpSuccessSigma ⨂_S OpSuccessUC))
                      o ( (λ(a,b,c). ((a),(a,b,c)))))"
      

definition ST_Deny :: "Operation × DB × Σ × υ ⇀ Output × DB × Σ × υ" 
where     "ST_Deny = (λ (ope,sp,si,uc). Some ((), sp,si,uc))"


definition SE_LR_RBAC_ST_Policy :: "Operation × DB × Σ × υ ↦ Output × DB × Σ × υ"
where     "SE_LR_RBAC_ST_Policy = ((λ (x,y).y)
                                     o_f ((ST_Allow,ST_Deny) ⨂_\<nabla> SE_LR_RBAC_Policy)
                                     o (λx.(x,x)))"

definition PolMon :: "Operation ==> (Output decision,DB × Σ × υ) MON_SE" 
where     "PolMon = (policy2MON SE_LR_RBAC_ST_Policy)" 

end