access_control_module/TeaclaveRequirements.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 TeaclaveRequirements
  imports Main TeaclaveAccessControl
begin

locale TeaclaveRequirements=TeaclaveAccessControl
begin

theorem TEACLAVESRS1:"request_user_access_data mconf uid oid=
                     (find_usrid(objattr_owners(read_objattr mconf oid)) (usr_attr uid)\<and>
                     resrcattr_infotype(objattr_resrcattr(read_objattr mconf oid))=data)"
proof (simp add:read_objattr_def request_user_access_data_def read_subjattr_def)
  show "user_access_data (usr_attr uid) (get_objattr (modelconf_obj mconf) oid) =
       (find_usrid(objattr_owners (get_objattr (modelconf_obj mconf) oid)) (usr_attr uid) \<and>
        resrcattr_infotype(objattr_resrcattr (get_objattr (modelconf_obj mconf) oid))=data)"
  proof
    assume "user_access_data (usr_attr uid) (get_objattr (modelconf_obj mconf) oid)"
    from this show "find_usrid(objattr_owners((get_objattr (modelconf_obj mconf) oid))) (usr_attr uid)\<and>
                   resrcattr_infotype(objattr_resrcattr (get_objattr (modelconf_obj mconf) oid))=data"
      proof (rule contrapos_pp)
        assume "\<not> (find_usrid
                    (objattr_owners(get_objattr (modelconf_obj mconf) oid))
                    (usr_attr uid) \<and>
              resrcattr_infotype(objattr_resrcattr(get_objattr (modelconf_obj mconf) oid))=data)"
        from this show "\<not> user_access_data (usr_attr uid) (get_objattr (modelconf_obj mconf) oid)"
          by (rule FDPACF1HLR13)
      qed
    next
    assume "find_usrid(objattr_owners (get_objattr (modelconf_obj mconf) oid)) (usr_attr uid) \<and>
           resrcattr_infotype(objattr_resrcattr (get_objattr (modelconf_obj mconf) oid))=data"
    from this show "user_access_data (usr_attr uid) (get_objattr (modelconf_obj mconf) oid)"
      by (rule FDPACF1HLR10)
  qed
qed

theorem TEACLAVESRS2:"request_task_access_data mconf sid oid\<Longrightarrow>
                     ((rel_subset(subjattr_participants(read_subjattr mconf sid)) 
                                 (objattr_owners(read_objattr mconf oid)))\<and>
                     resrcattr_infotype(objattr_resrcattr(read_objattr mconf oid))=data)"
proof (simp add:read_objattr_def request_task_access_data_def read_subjattr_def)
  assume 0:"task_access_data (get_subjattr (modelconf_subj mconf) sid)
           (get_objattr (modelconf_obj mconf) oid)"
  from this have 1:"rel_subset(subjattr_participants(get_subjattr (modelconf_subj mconf) sid)) 
                   (objattr_owners(get_objattr (modelconf_obj mconf) oid))\<and>
                   resrcattr_infotype(objattr_resrcattr(get_objattr (modelconf_obj mconf) oid))=data"
  proof (rule contrapos_pp)
    assume "\<not> (rel_subset
           (subjattr_participants(get_subjattr (modelconf_subj mconf) sid))
           (objattr_owners (get_objattr (modelconf_obj mconf) oid)) \<and>
           resrcattr_infotype (objattr_resrcattr(get_objattr (modelconf_obj mconf) oid)) = data)"
    from this show "\<not> task_access_data (get_subjattr (modelconf_subj mconf) sid)
                   (get_objattr (modelconf_obj mconf) oid)" by (rule FDPACF1HLR14)
  qed
  from this show "rel_subset(subjattr_participants(get_subjattr (modelconf_subj mconf) sid))
                 (objattr_owners (get_objattr (modelconf_obj mconf) oid)) \<and>
                 resrcattr_infotype(objattr_resrcattr (get_objattr (modelconf_obj mconf) oid))=data"
    by auto
qed

end

print_locale! TeaclaveRequirements

end