Theory Service

(*****************************************************************************
 * 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 ⨂⇩∨⇩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 ⨂⇩∨⇩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 ⨂⇩∨⇩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) ⨂⇩∇ SE_LR_RBAC_Policy) 
                                     o (λx.(x,x)))"

definition PolMon :: "Operation ⇒ (Output decision,DB × Σ × υ) MON⇩S⇩E" 
where     "PolMon = (policy2MON SE_LR_RBAC_ST_Policy)" 

end