access_control_module/interpretation/I_FDP_ACF.thy

(*
 * Licensed to the Apache Software Foundation (ASF) under one
 * or more contributor license agreements.  See the NOTICE file
 * distributed with this work for additional information
 * regarding copyright ownership.  The ASF licenses this file
 * to you under the Apache License, Version 2.0 (the
 * "License"); you may not use this file except in compliance
 * with the License.  You may obtain a copy of the License at
 *
 *   http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing,
 * software distributed under the License is distributed on an
 * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
 * KIND, either express or implied.  See the License for the
 * specific language governing permissions and limitations
 * under the License.
 *)

theory I_FDP_ACF
  imports Main "../FDP_ACF" I_ResrcAttr 
begin

definition task_access_function::"SubjAttr\<Rightarrow>ObjAttr\<Rightarrow>bool" where
"task_access_function sattr oattr\<equiv>
(if rel_subset_usr(subj_participants sattr) (obj_owners oattr)\<and>
    info_type(obj_resrcattr oattr)=Func
 then
 True
 else False)"

definition user_access_function::"UsrAttr\<Rightarrow>ObjAttr\<Rightarrow>bool" where
"user_access_function uattr oattr\<equiv>
(if find_usrid(obj_owners oattr) uattr\<and>
 info_type(obj_resrcattr oattr)=Func
 then
 True
 else False)"

definition task_access_data::"SubjAttr\<Rightarrow>ObjAttr\<Rightarrow>bool" where
"task_access_data sattr oattr\<equiv>
(if rel_subset_usr(subj_participants sattr) (obj_owners oattr)\<and>
    info_type(obj_resrcattr oattr)=Data
 then
 True
 else False)"

definition user_access_data::"UsrAttr\<Rightarrow>ObjAttr\<Rightarrow>bool" where
"user_access_data uattr oattr\<equiv>
(if find_usrid(obj_owners oattr) uattr\<and>
 info_type(obj_resrcattr oattr)=Data
 then
 True
 else False)"

interpretation FdpAcf1 : FdpAcf1 noresrcid valid_resrcid noinfoid valid_infoid InSgx OutSgx
                                 is_insgx Device Normal is_normal Data Func is_data
                                 noresrcattr resrc_attr presrc_id info_id
                                 trust_level presrc_type info_type
                                 nousrid valid_usrid nousrattr usr_attr usrattr_id nousrattrconf
                                 usrattr_conf is_usrattrconf find_usrid delete_usrattr
                                 get_usrattr valid_usrattrconf nosubjattr subj_attr
                                 subj_callerattr subj_participants
                                 subj_resrcattr noobjattr obj_attr
                                 obj_owners obj_resrcattr rel_subset_usr
                                 task_access_function user_access_function task_access_data
                                 user_access_data
proof
  fix sattr
  fix oattr
  show "rel_subset_usr (subj_participants sattr)
       (obj_owners oattr) \<and>
       info_type (obj_resrcattr oattr) = InfoType.Func \<Longrightarrow>
       task_access_function sattr oattr" by (auto simp:task_access_function_def)
next
  fix sattr
  fix oattr
  show " \<not> rel_subset_usr (subj_participants sattr)
       (obj_owners oattr) \<and>
       info_type (obj_resrcattr oattr) = InfoType.Func \<Longrightarrow>
       \<not> task_access_function sattr oattr" by (auto simp:task_access_function_def)
next
  fix sattr
  fix oattr
  show "rel_subset_usr (subj_participants sattr)
       (obj_owners oattr) \<and>
       info_type (obj_resrcattr oattr) \<noteq> InfoType.Func \<Longrightarrow>
       \<not>task_access_function sattr oattr" by (auto simp:task_access_function_def)
next
  fix oattr
  fix uattr
  show "find_usrid (obj_owners oattr) uattr \<and>
       info_type (obj_resrcattr oattr) = InfoType.Func \<Longrightarrow>
       user_access_function uattr oattr" by (auto simp:user_access_function_def)
next
  fix oattr
  fix uattr
  show "\<not> find_usrid (obj_owners oattr) uattr \<and>
       info_type (obj_resrcattr oattr) = InfoType.Func \<Longrightarrow>
       \<not> user_access_function uattr oattr" by (auto simp:user_access_function_def)
next
  fix oattr
  fix uattr
  show "find_usrid (obj_owners oattr) uattr \<and>
       info_type (obj_resrcattr oattr) \<noteq> InfoType.Func \<Longrightarrow>
       \<not> user_access_function uattr oattr" by (auto simp:user_access_function_def)
next
  fix sattr
  fix oattr
  show "rel_subset_usr (subj_participants sattr)
       (obj_owners oattr) \<and>
       info_type (obj_resrcattr oattr) = Data \<Longrightarrow>
       task_access_data sattr oattr" by (auto simp:task_access_data_def)
next
  fix sattr
  fix oattr
  show "\<not> rel_subset_usr (subj_participants sattr)
       (obj_owners oattr) \<and>
       info_type (obj_resrcattr oattr) = Data \<Longrightarrow>
       \<not> task_access_data sattr oattr" by (auto simp:task_access_data_def)
next
  fix sattr
  fix oattr
  show "rel_subset_usr (subj_participants sattr)
       (obj_owners oattr) \<and>
       info_type (obj_resrcattr oattr) \<noteq> Data \<Longrightarrow>
       \<not>task_access_data sattr oattr" by (auto simp:task_access_data_def)
next
  fix oattr
  fix uattr
  show "find_usrid (obj_owners oattr) uattr \<and>
       info_type (obj_resrcattr oattr) = Data \<Longrightarrow>
       user_access_data uattr oattr" by (auto simp:user_access_data_def)
next
  fix oattr
  fix uattr
  show "\<not> find_usrid (obj_owners oattr) uattr \<and>
       info_type (obj_resrcattr oattr) = Data \<Longrightarrow>
       \<not> user_access_data uattr oattr" by (auto simp:user_access_data_def)
next
  fix oattr
  fix uattr
  show "find_usrid (obj_owners oattr) uattr \<and>
       info_type (obj_resrcattr oattr) \<noteq> Data \<Longrightarrow>
       \<not> user_access_data uattr oattr" by (auto simp:user_access_data_def)
next
  fix oattr
  fix uattr
  show "\<not> (find_usrid (obj_owners oattr) uattr \<and>
       info_type (obj_resrcattr oattr) = Data) \<Longrightarrow>
       \<not> user_access_data uattr oattr" by (auto simp:user_access_data_def)
next
  fix sattr
  fix oattr
  show "\<not> (rel_subset_usr (subj_participants sattr) (obj_owners oattr) \<and>
       info_type (obj_resrcattr oattr) = Data) \<Longrightarrow>
       \<not> task_access_data sattr oattr" by (auto simp:task_access_data_def)
qed

end