Merge pull request #2 from SeanVer/master
update README.md of root directory
diff --git a/README.md b/README.md
index e8698cf..011e34d 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,161 @@
# Teaclave Verification
This repository contains formal descriptions, specifications, and proofs for Teaclave.
+
+## [`access_control_module`](access_control_module/)
+
+This directory contains formal description and verification of access control
+module of Teaclave described in [`access-control.md`][0]. It uses [`security
+functional requirements`][1] to restate the design specifications, then proves
+the required security objectives in [`Isabelle`][2].
+
+ [0]: https://github.com/apache/incubator-teaclave/blob/master/docs/access-control.md
+ [1]: https://www.commoncriteriaportal.org/files/ccfiles/CCPART2V3.1R5.pdf
+ [2]: https://isabelle.in.tum.de/index.html
+
+### security problem definition
+
+The purpose of security problem definition is to identify the scope of problems to be
+solved by the access control module. The security problem of access control module of
+Teaclave is defined in terms of the assets protected by the module, the threats encountered
+by the module and the preconditions assumed to be true to the module.
+
+ * Assets: the confidentiality and integrity of critical data operated by the tasks
+ and functions defined by Teaclave
+
+ * Threats: runtime tasks and functions abuse which compromise the confidentiality
+ and integrity of critical data.
+
+ * Assumptions: the critical data can only be accessed through tasks and functions
+ defined by Teaclave; the identification and authentication of users is achieved by
+ the other modules of Teaclave.
+
+### security objectives
+
+The security objective of access control module is to prevent unauthorized users from
+accessing the critical data through tasks and functions. By achieving the security
+objective, the threats of runtime tasks and functions abuse are eliminated under the
+assumptions identified in security problem definition.
+
+### security requirements
+
+Security functional requirements of [`Common Criteria`][3] are used for decomposing
+security objectives with standardized language. The security objective of Teaclave
+access control module is decomposed as follows:
+
+ * FIA_UAU.2 User authentication before any action <br>
+ Dependencies：FIA_UID.1 timing of identification
+
+ * FIA_UAU.2.1 The Teaclave access control module shall require each user to be
+ successfully authenticated before allowing any other Teaclave-mediated actions on
+ behalf of that user. *(This requirement is already covered by assumption, so it is
+ not formalized.)*
+
+ * FIA_UID.2 User identification before any action <br>
+ Dependencies：No dependencies
+
+ * FIA_UID.2.1 The Teaclave access control module shall require each user to be
+ successfully identified before allowing any other Teaclave-mediated actions on
+ behalf of that user. *(This requirement is already covered by assumption, so it
+ is not formalized.)*
+
+ * FIA_UAU.3 Unforgeable authentication <br>
+ Dependencies：No dependencies
+
+ * FIA_UAU.3.1 The Teaclave access control module shall prevent use of authentication
+ data that has been forged by any user of the Teaclave access control module. *(This
+ requirement is already covered by assumption, so it is not formalized.)*
+
+ * FIA_UAU.3.2 The Teaclave access control module shall prevent use of authentication
+ data that has been copied from any other user of the Teaclave access control module.
+ *(This requirement is already covered by assumption, so it is not formalized.)*
+
+ * FIA_USB.1 User-subject binding <br>
+ Dependencies：FIA_ATD.1 User attribute definition
+
+ * FIA_USB.1.1 The Teaclave access control module shall associate the following user
+ security attributes with subjects acting on the behalf of that user: UsrId.
+
+ * FIA_USB.1.2 The Teaclave access control module shall enforce the following rules on
+ the initial association of user security attributes with subjects acting on the behalf
+ of users: UsrId is in the participants of subjects.
+
+ * FIA_USB.1.3 The Teaclave access control module shall enforce the following rules
+ governing changes to the user security attributes associated with subjects acting on the
+ behalf of users: None.
+
+ * FIA_ATD.1 User attribute definition <br>
+ Dependencies：No dependencies
+
+ * FIA_ATD.1 The Teaclave access control module shall maintain the following list of
+ security attributes belonging to individual users: UsrId.
+
+ * FDP_ACC.1 Subset access control <br>
+ Dependencies：FDP_ACF.1 Security attribute based access control
+
+ * FDP_ACC.1.1 The Teaclave access control module shall enforce the Teaclave Subset
+ access control SFP on: <br>
+ subject: task, user; <br>
+ object: function, data; <br>
+ operation: task_access_data, task_access_function, user_access_data, user_access_function.
+
+ * FDP_ACF.1 Security attribute based access control <br>
+ Dependencies：FDP_ACC.1 Subset access control；<br>
+ FMT_MSA.3：Static attribute initialisation
+
+ * FDP_ACF.1.1 The Teaclave access control module shall enforce the Teaclave Subset access
+ control SFP to objects based on the following: <br>
+ subject attributes: task_participant; UsrId <br>
+ object attributes: function_owner; data_owner.
+
+ * FDP_ACF.1.2 The TSF shall enforce the following rules to determine if an operation among
+ controlled subjects and controlled objects is allowed: <br>
+ task_access_data is allowed if data_owner is the subset of task_participant; <br>
+ task_access_function is allowed if function_owner is the subset of task_participant; <br>
+ user_access_data is allowed if UsrId is in data_owner; <br>
+ user_access_function is allowed if UsrId is in function_owner.
+
+ * FDP_ACF.1.3 The TSF shall explicitly authorize access of subjects to objects based on the
+ following additional rules: NONE.
+
+ * FDP_ACF.1.4 The TSF shall explicitly deny access of subjects to objects based on the
+ following additional rules: NONE.
+
+ * FMT_MSA.3 Static attribute initialization <br>
+ Dependencies：FMT_MSA.1 Management of security attributes；<br>
+ FMT_SMR.1 Security roles
+
+ * FMT_MSA.3.1 The Teaclave access control shall enforce the Teaclave Subset access control
+ SFP to provide permissive default values for security attributes that are used to enforce
+ the SFP.
+
+ * FMT_MSA.3.2 The TSF shall not allow the Users to specify alternative initial values to
+ override the default values when an object or information is created.
+
+ * FMT_MSA.1 Management of security attributes <br>
+ Dependencies：FDP_IFC.1 Subset information flow control；<br>
+ FMT_SMR.1 Security roles；<br>
+ FMT_SMF.1 Specification of Management Functions
+
+ * FMT_MSA.1.1 The Teaclave access control module shall enforce the Teaclave Subset access
+ control SFP to restrict the ability to query the security attributes to Users.
+
+ * FMT_SMR.1 Security roles <br>
+ Dependencies：FIA_UID.1 Timing of identification
+
+ * FMT_SMR.1.1 The Teaclave access control module shall maintain the roles: User.
+
+ * FMT_SMR.1.2 The Teaclave access control module shall be able to associate users with roles.
+
+ * FMT_SMF.1 Specification of Management Functions <br>
+ Dependencies：No dependencies
+
+ * FMT_SMF.1.1 The Teaclave access control module shall be capable of performing the following
+ management functions: <br>
+ request_user_access_data, request_user_access_function, request_task_access_data,
+ request_task_access_function, request_user_access_task.
+
+Each security functional requirement listed above is formalized and located in different files. For more information,
+please refer to [`access control module introduction`](access_control_module/README.md).
+
+ [3]: https://www.commoncriteriaportal.org/files/ccfiles/CCPART2V3.1R5.pdf
diff --git a/access_control_module/AttrConf.thy b/access_control_module/AttrConf.thy
index c7ceef2..9c1c149 100644
--- a/access_control_module/AttrConf.thy
+++ b/access_control_module/AttrConf.thy
@@ -36,65 +36,108 @@
assumes ATTRCONFHLR2:"is_attrconf(attr_conf conf attr)"
assumes ATTRCONFHLR3:"x=noattrconf\<or>(\<exists>conf attr. x=attr_conf conf attr)"
assumes ATTRCONFHLR4:"attr_elem noattr=noelem"
- assumes ATTRCONFHLR5:"\<not>find_elem noattrconf attr"
- assumes ATTRCONFHLR6:"conf=noattrconf\<and>
- attr_elem attr\<noteq>noelem\<and>
- attr_elem attrx=attr_elem attr\<Longrightarrow>
+ assumes ATTRCONFHLR6:"\<not>find_elem noattrconf attr"
+ assumes ATTRCONFHLR7:"attr_elem attrx=attr_elem attr\<Longrightarrow>
find_elem(attr_conf conf attrx) attr"
- assumes ATTRCONFHLR7:"conf\<noteq>noattrconf\<and>
- attr_elem attr\<noteq>noelem\<and>
- attr_elem attrx=attr_elem attr\<Longrightarrow>
+ assumes ATTRCONFHLR8:"find_elem conf attr\<Longrightarrow>
find_elem(attr_conf conf attrx) attr"
- assumes ATTRCONFHLR8:"find_elem conf attr\<and>
- attr_elem attr=attr_elem attrx\<Longrightarrow>
- find_elem conf attrx"
- assumes ATTRCONFHLR9:"conf\<noteq>noattrconf\<and>
- find_elem conf attr\<Longrightarrow>
- find_elem(attr_conf conf attrx) attr"
- assumes ATTRCONFHLR10:"\<not>((conf=noattrconf\<and>
- attr_elem attr\<noteq>noelem\<and>
- attr_elem attrx=attr_elem attr)\<or>
- (conf\<noteq>noattrconf\<and>
- attr_elem attr\<noteq>noelem\<and>
- attr_elem attrx=attr_elem attr)\<or>
- (conf\<noteq>noattrconf\<and>
- find_elem conf attr))\<Longrightarrow>
+ assumes ATTRCONFHLR9:"(\<not>find_elem conf attr)\<and>
+ attr_elem attrx\<noteq>attr_elem attr\<Longrightarrow>
\<not>find_elem(attr_conf conf attrx) attr"
- assumes ATTRCONFHLR11:"delete_attr noattrconf attr=noattrconf"
- assumes ATTRCONFHLR12:"attr_elem attrx=attr_elem attr\<and>
- attr_elem attr\<noteq>noelem\<Longrightarrow>
- delete_attr(attr_conf conf attrx) attr=conf"
- assumes ATTRCONFHLR13:"attr_elem attr=noelem\<Longrightarrow>
- delete_attr(attr_conf conf attrx) attr=attr_conf conf attrx"
- assumes ATTRCONFHLR14:"attr_elem attrx\<noteq>attr_elem attr\<and>
- attr_elem attr\<noteq>noelem\<Longrightarrow>
+ assumes ATTRCONFHLR10:"delete_attr noattrconf attr=noattrconf"
+ assumes ATTRCONFHLR11:"attr_elem attrx=attr_elem attr\<Longrightarrow>
+ delete_attr(attr_conf conf attrx) attr=delete_attr conf attr"
+ assumes ATTRCONFHLR12:"attr_elem attrx\<noteq>attr_elem attr\<Longrightarrow>
delete_attr(attr_conf conf attrx) attr=
- attr_conf(delete_attr conf attr) attrx"
- assumes ATTRCONFHLR15:"get_attr noattrconf elem=noattr"
- assumes ATTRCONFHLR16:"elem\<noteq>noelem\<and>
- attr_elem attr=elem\<Longrightarrow>
+ attr_conf (delete_attr conf attr) attrx"
+ assumes ATTRCONFHLR13:"get_attr noattrconf elem=noattr"
+ assumes ATTRCONFHLR14:"attr_elem attr=elem\<Longrightarrow>
get_attr(attr_conf conf attr) elem=attr"
- assumes ATTRCONFHLR17:"elem=noelem\<Longrightarrow>
+ assumes ATTRCONFHLR15:"get_attr conf elem=noattr\<and>
+ attr_elem attr\<noteq>elem\<Longrightarrow>
get_attr(attr_conf conf attr) elem=noattr"
- assumes ATTRCONFHLR18:"elem\<noteq>noelem\<and>
+ assumes ATTRCONFHLR16:"get_attr conf elem\<noteq>noattr\<and>
attr_elem attr\<noteq>elem\<Longrightarrow>
get_attr(attr_conf conf attr) elem=get_attr conf elem"
- assumes ATTRCONFHLR19:"\<not>valid_attrconf noattrconf"
- assumes ATTRCONFHLR20:"conf=noattrconf\<and>
- \<not>find_elem conf attr\<Longrightarrow>
+ assumes ATTRCONFHLR17:"\<not>valid_attrconf noattrconf"
+ assumes ATTRCONFHLR18:"attr_elem attr\<noteq>noelem\<and>
+ conf=noattrconf\<Longrightarrow>
valid_attrconf(attr_conf conf attr)"
+ assumes ATTRCONFHLR19:"valid_attrconf conf\<and>
+ (\<not>find_elem conf attr)\<and>
+ attr_elem attr\<noteq>noelem\<Longrightarrow>
+ valid_attrconf(attr_conf conf attr)"
+ assumes ATTRCONFHLR20:"attr_elem attr=noelem\<Longrightarrow>\<not>valid_attrconf(attr_conf conf attr)"
assumes ATTRCONFHLR21:"conf\<noteq>noattrconf\<and>
- \<not>find_elem conf attr\<and>
- valid_attrconf conf\<Longrightarrow>
- valid_attrconf(attr_conf conf attr)"
- assumes ATTRCONFHLR22:"\<not>((conf=noattrconf\<and>
- \<not>find_elem conf attr)\<or>
- (conf\<noteq>noattrconf\<and>
- \<not>find_elem conf attr\<and>
- valid_attrconf conf))\<Longrightarrow>
+ \<not>valid_attrconf conf\<Longrightarrow>
\<not>valid_attrconf(attr_conf conf attr)"
+ assumes ATTRCONFHLR22:"conf\<noteq>noattrconf\<and>
+ find_elem conf attr\<Longrightarrow>
+ \<not>valid_attrconf(attr_conf conf attr)"
+ assumes ATTRCONFINDUCT:"\<lbrakk>P noattrconf;\<And>conf1 attr1. P conf1\<Longrightarrow>P(attr_conf conf1 attr1)\<rbrakk>\<Longrightarrow>P conf"
begin
+lemma find_total:"find_elem conf attr\<or>
+ attr_elem attrx=attr_elem attr\<Longrightarrow>find_elem(attr_conf conf attrx) attr"
+proof (erule disjE)
+ assume "find_elem conf attr"
+ from this show "find_elem (attr_conf conf attrx) attr" by (rule ATTRCONFHLR8)
+next
+ assume "attr_elem attrx = attr_elem attr"
+ from this show "find_elem (attr_conf conf attrx) attr" by (rule ATTRCONFHLR7)
+qed
+
+lemma find_dual:
+ "find_elem conf attr\<or>
+ attr_elem attrx=attr_elem attr=
+ (\<not>((\<not>find_elem conf attr)\<and>attr_elem attrx\<noteq>attr_elem attr))"
+ by blast
+
+lemma valid_total:"(attr_elem attr\<noteq>noelem\<and>
+ conf=noattrconf)\<or>
+ (valid_attrconf conf\<and>
+ (\<not>find_elem conf attr)\<and>
+ attr_elem attr\<noteq>noelem)\<Longrightarrow>valid_attrconf(attr_conf conf attr)"
+proof (erule disjE)
+ assume "attr_elem attr \<noteq> noelem \<and> conf = noattrconf"
+ from this show "valid_attrconf (attr_conf conf attr)" by (rule ATTRCONFHLR18)
+next
+ assume "valid_attrconf conf \<and>
+ \<not> find_elem conf attr \<and> attr_elem attr \<noteq> noelem"
+ from this show "valid_attrconf (attr_conf conf attr)" by (rule ATTRCONFHLR19)
+qed
+
+lemma not_valid_total:"attr_elem attr=noelem\<or>
+ ((\<not>valid_attrconf conf)\<and>
+ conf\<noteq>noattrconf)\<or>
+ (conf\<noteq>noattrconf\<and>
+ find_elem conf attr)\<Longrightarrow>\<not>valid_attrconf(attr_conf conf attr)"
+proof (erule disjE)
+ assume "attr_elem attr = noelem"
+ from this show "\<not>valid_attrconf(attr_conf conf attr)" by (rule ATTRCONFHLR20)
+next
+ show "\<not> valid_attrconf conf \<and>
+ conf \<noteq> noattrconf \<or>
+ conf \<noteq> noattrconf \<and>
+ find_elem conf attr \<Longrightarrow>
+ \<not> valid_attrconf (attr_conf conf attr)"
+ proof (erule disjE)
+ assume "\<not> valid_attrconf conf \<and> conf \<noteq> noattrconf"
+ from this show "\<not> valid_attrconf (attr_conf conf attr)" by (auto simp: ATTRCONFHLR21)
+ next
+ assume "conf \<noteq> noattrconf \<and> find_elem conf attr"
+ from this show "\<not> valid_attrconf (attr_conf conf attr)" by (auto simp: ATTRCONFHLR22)
+ qed
+qed
+
+lemma valid_dual:
+ "(attr_elem attr\<noteq>noelem\<and>conf=noattrconf)\<or>
+ (valid_attrconf conf\<and>(\<not>find_elem conf attr)\<and>attr_elem attr\<noteq>noelem)=
+ (\<not>(attr_elem attr=noelem\<or>
+ ((\<not>valid_attrconf conf)\<and>conf\<noteq>noattrconf)\<or>
+ (conf\<noteq>noattrconf\<and>find_elem conf attr)))"
+ by blast
+
lemma ATTRCONFHLR23:"noattrconf\<noteq>attr_conf conf attr"
proof
fix conf attr
@@ -110,19 +153,94 @@
from ATTRCONFHLR3 0 show "\<exists>sconf oconf. x = attr_conf sconf oconf" by blast
qed
-lemma ATTRCONFHLR25:"conf=noattrconf\<and>
- attr_elem attrx\<noteq>attr_elem attr\<Longrightarrow>\<not>find_elem(attr_conf conf attrx) attr"
-proof -
- assume "conf = noattrconf \<and> attr_elem attrx \<noteq> attr_elem attr"
- from this have "\<not>((conf=noattrconf\<and>
- attr_elem attr\<noteq>noelem\<and>
- attr_elem attrx=attr_elem attr)\<or>
- (conf\<noteq>noattrconf\<and>
- attr_elem attr\<noteq>noelem\<and>
- attr_elem attrx=attr_elem attr)\<or>
- (conf\<noteq>noattrconf\<and>
- find_elem conf attr))" by blast
- from this show "\<not>find_elem(attr_conf conf attrx) attr" by (rule ATTRCONFHLR10)
+lemma ATTRCONFHLR25:"valid_attrconf conf\<and>
+ find_elem conf attr\<Longrightarrow>attr_elem attr\<noteq>noelem"
+proof (induction rule:ATTRCONFINDUCT)
+ show "valid_attrconf noattrconf \<and> find_elem noattrconf attr \<Longrightarrow>
+ attr_elem attr \<noteq> noelem" by (auto simp:ATTRCONFHLR17)
+next
+ fix conf1 attr1
+ show "(valid_attrconf conf1 \<and> find_elem conf1 attr \<Longrightarrow>
+ attr_elem attr \<noteq> noelem) \<Longrightarrow>
+ valid_attrconf (attr_conf conf1 attr1) \<and>
+ find_elem (attr_conf conf1 attr1) attr \<Longrightarrow>
+ attr_elem attr \<noteq> noelem"
+ proof (auto)
+ assume 1:"valid_attrconf conf1 \<and> find_elem conf1 attr \<Longrightarrow> False"
+ assume 2:"find_elem (attr_conf conf1 attr1) attr"
+ assume 3:"noelem = attr_elem attr"
+ assume "valid_attrconf (attr_conf conf1 attr1)"
+ from this have 4:"(attr_elem attr1\<noteq>noelem\<and>
+ conf1=noattrconf)\<or>
+ (valid_attrconf conf1\<and>
+ (\<not>find_elem conf1 attr1)\<and>
+ attr_elem attr1\<noteq>noelem)"
+ proof (rule contrapos_pp)
+ assume "\<not> (attr_elem attr1 \<noteq> noelem \<and>
+ conf1 = noattrconf \<or>
+ valid_attrconf conf1 \<and>
+ \<not> find_elem conf1 attr1 \<and>
+ attr_elem attr1 \<noteq> noelem)"
+ from this have "attr_elem attr1=noelem\<or>
+ ((\<not>valid_attrconf conf1)\<and>
+ conf1\<noteq>noattrconf)\<or>
+ (conf1\<noteq>noattrconf\<and>
+ find_elem conf1 attr1)" by (auto simp:valid_dual)
+ from this show "\<not> valid_attrconf (attr_conf conf1 attr1)" by (rule not_valid_total)
+ qed
+ from 2 have 2:"find_elem conf1 attr\<or>
+ attr_elem attr1=attr_elem attr"
+ proof (rule contrapos_pp)
+ assume "\<not> (find_elem conf1 attr \<or>
+ attr_elem attr1 = attr_elem attr)"
+ from this have "((\<not>find_elem conf1 attr)\<and>
+ attr_elem attr1\<noteq>attr_elem attr)" by (auto simp:find_dual)
+ from this show "\<not> find_elem (attr_conf conf1 attr1) attr" by (rule ATTRCONFHLR9)
+ qed
+ from 2 3 4 have "(find_elem conf1 attr \<or>
+ attr_elem attr1 = attr_elem attr)\<and>
+ (noelem = attr_elem attr)\<and>
+ (attr_elem attr1 \<noteq> noelem \<and>
+ conf1 = noattrconf \<or>
+ valid_attrconf conf1 \<and>
+ \<not> find_elem conf1 attr1 \<and>
+ attr_elem attr1 \<noteq> noelem)" by auto
+ from this show False
+ proof (auto simp:ATTRCONFHLR6)
+ from 1 show "noelem = attr_elem attr \<Longrightarrow>
+ find_elem conf1 attr \<Longrightarrow>
+ valid_attrconf conf1 \<Longrightarrow>
+ \<not> find_elem conf1 attr1 \<Longrightarrow>
+ attr_elem attr1 \<noteq> attr_elem attr \<Longrightarrow> False" by (auto simp:1)
+ qed
+ qed
+qed
+
+lemma ATTRCONFHLR26:"find_elem conf attr\<and>
+ attr_elem attr=attr_elem attrx\<Longrightarrow>find_elem conf attrx"
+proof (induction conf rule:ATTRCONFINDUCT)
+ assume "find_elem noattrconf attr \<and> attr_elem attr = attr_elem attrx"
+ from this show "find_elem noattrconf attrx" by (auto simp:ATTRCONFHLR6)
+next
+ fix conf1 attr1
+ assume 0:"find_elem conf1 attr \<and>
+ attr_elem attr = attr_elem attrx \<Longrightarrow>
+ find_elem conf1 attrx"
+ assume "find_elem (attr_conf conf1 attr1) attr \<and>
+ attr_elem attr = attr_elem attrx"
+ from this have 1:"attr_elem attr = attr_elem attrx"
+ and 2:"find_elem (attr_conf conf1 attr1) attr" by auto
+ from 2 have 2:"find_elem conf1 attr\<or>
+ attr_elem attr1=attr_elem attr"
+ proof (rule contrapos_pp)
+ assume "\<not> (find_elem conf1 attr \<or>
+ attr_elem attr1 = attr_elem attr)"
+ from this have "((\<not>find_elem conf1 attr)\<and>
+ attr_elem attr1\<noteq>attr_elem attr)" by (auto simp:find_dual)
+ from this show "\<not> find_elem (attr_conf conf1 attr1) attr" by (rule ATTRCONFHLR9)
+ qed
+ from 1 2 show "find_elem (attr_conf conf1 attr1) attrx"
+ by (auto simp add:0 ATTRCONFHLR8 ATTRCONFHLR7)
qed
end
@@ -142,7 +260,7 @@
and get_attr::"'attrconf\<Rightarrow>'element\<Rightarrow>'attr"
and valid_attrconf::"'attrconf\<Rightarrow>bool" +
fixes rel_subset::"'attrconf\<Rightarrow>'attrconf\<Rightarrow>bool"
- assumes ATTRCONFRELHLR1:"\<not>rel_subset confx noattrconf"
+ assumes ATTRCONFRELHLR1:"rel_subset confx noattrconf"
assumes ATTRCONFRELHLR2:"conf=noattrconf\<and>
find_elem confx attr\<Longrightarrow>
rel_subset confx (attr_conf conf attr)"
@@ -150,13 +268,90 @@
find_elem confx attr\<and>
rel_subset confx conf\<Longrightarrow>
rel_subset confx (attr_conf conf attr)"
- assumes ATTRCONFRELHLR4:"\<not>((conf\<noteq>noattrconf\<and>
- find_elem confx attr\<and>
- rel_subset confx conf)\<or>
- (conf=noattrconf\<and>
- find_elem confx attr))\<Longrightarrow>
+ assumes ATTRCONFRELHLR4:"\<not>rel_subset confx conf\<Longrightarrow>
\<not>rel_subset confx (attr_conf conf attr)"
- assumes ATTRCONFRELHLR5:"rel_subset confx conf\<and>find_elem conf attr\<Longrightarrow>find_elem confx attr"
+ assumes ATTRCONFRELHLR5:"rel_subset confx conf\<and>
+ \<not>find_elem confx attr\<Longrightarrow>
+ \<not>rel_subset confx (attr_conf conf attr)"
+begin
+
+lemma rel_subset_total:"(conf=noattrconf\<and>
+ find_elem confx attr)\<or>
+ (conf\<noteq>noattrconf\<and>
+ find_elem confx attr\<and>
+ rel_subset confx conf)\<Longrightarrow>rel_subset confx (attr_conf conf attr)"
+proof (erule disjE)
+ assume "conf = noattrconf \<and> find_elem confx attr"
+ from this show "rel_subset confx (attr_conf conf attr)" by (rule ATTRCONFRELHLR2)
+next
+ assume "conf \<noteq> noattrconf \<and> find_elem confx attr \<and> rel_subset confx conf"
+ from this show "rel_subset confx (attr_conf conf attr)" by (rule ATTRCONFRELHLR3)
+qed
+
+lemma not_rel_subset_total:"(\<not>rel_subset confx conf)\<or>
+ (rel_subset confx conf\<and>\<not>find_elem confx attr)\<Longrightarrow>
+ \<not>rel_subset confx (attr_conf conf attr)"
+proof (erule disjE)
+ assume "\<not> rel_subset confx conf"
+ from this show "\<not> rel_subset confx (attr_conf conf attr)" by (rule ATTRCONFRELHLR4)
+next
+ assume "rel_subset confx conf \<and> \<not> find_elem confx attr"
+ from this show "\<not> rel_subset confx (attr_conf conf attr)" by (rule ATTRCONFRELHLR5)
+qed
+
+lemma rel_subset_dual:
+ "(conf=noattrconf\<and>find_elem confx attr)\<or>
+ (conf\<noteq>noattrconf\<and>find_elem confx attr\<and>rel_subset confx conf)=
+ (\<not>((\<not>rel_subset confx conf)\<or>(rel_subset confx conf\<and>\<not>find_elem confx attr)))"
+ by blast
+
+lemma ATTRCONFRELHLR6:"rel_subset confx conf\<and>find_elem conf attr\<Longrightarrow>find_elem confx attr"
+proof (induction conf rule:ATTRCONFINDUCT)
+ assume "rel_subset confx noattrconf \<and> find_elem noattrconf attr"
+ from this show "find_elem confx attr" by (auto simp:ATTRCONFHLR6)
+next
+ fix conf1 attr1
+ assume 0:"rel_subset confx conf1 \<and> find_elem conf1 attr \<Longrightarrow>
+ find_elem confx attr"
+ assume "rel_subset confx (attr_conf conf1 attr1) \<and>
+ find_elem (attr_conf conf1 attr1) attr"
+ from this have 1:"rel_subset confx (attr_conf conf1 attr1)"
+ and 2:"find_elem (attr_conf conf1 attr1) attr" by auto
+ from 1 have 1:"(conf1=noattrconf\<and>
+ find_elem confx attr1)\<or>
+ (conf1\<noteq>noattrconf\<and>
+ find_elem confx attr1\<and>
+ rel_subset confx conf1)"
+ proof (rule contrapos_pp)
+ assume "\<not> (conf1 = noattrconf \<and> find_elem confx attr1 \<or>
+ conf1 \<noteq> noattrconf \<and>
+ find_elem confx attr1 \<and> rel_subset confx conf1)"
+ from this have "((\<not>rel_subset confx conf1)\<or>
+ (rel_subset confx conf1\<and>\<not>find_elem confx attr1))"
+ by (auto simp:rel_subset_dual)
+ from this show "\<not> rel_subset confx (attr_conf conf1 attr1)"
+ by (auto simp:not_rel_subset_total)
+ qed
+ from 2 have 2:"find_elem conf1 attr\<or>
+ attr_elem attr1=attr_elem attr"
+ proof (rule contrapos_pp)
+ assume "\<not> (find_elem conf1 attr \<or>
+ attr_elem attr1 = attr_elem attr)"
+ from this have "((\<not>find_elem conf1 attr)\<and>
+ attr_elem attr1\<noteq>attr_elem attr)" by (auto simp:find_dual)
+ from this show "\<not> find_elem (attr_conf conf1 attr1) attr" by (rule ATTRCONFHLR9)
+ qed
+ from 1 2 have "(conf1 = noattrconf \<and>
+ find_elem confx attr1 \<or>
+ conf1 \<noteq> noattrconf \<and>
+ find_elem confx attr1 \<and>
+ rel_subset confx conf1)\<and>
+ (find_elem conf1 attr \<or>
+ attr_elem attr1 = attr_elem attr)" by auto
+ from this show ?thesis by (auto simp add:0 ATTRCONFHLR26 ATTRCONFHLR6)
+qed
+
+end
print_locale! AttrConfRel
diff --git a/access_control_module/interpretation/I_AttrConf.thy b/access_control_module/interpretation/I_AttrConf.thy
index 9e7561c..d4240d6 100644
--- a/access_control_module/interpretation/I_AttrConf.thy
+++ b/access_control_module/interpretation/I_AttrConf.thy
@@ -24,11 +24,12 @@
datatype UsrAttrConf = nousrattrconf |
is_usrattrconf:usrattr_conf UsrAttrConf UsrAttr
+print_theorems
+
primrec find_usrid::"UsrAttrConf\<Rightarrow>UsrAttr\<Rightarrow>bool" where
"find_usrid nousrattrconf attr= False"
| "find_usrid (usrattr_conf conf attrx) attr=
-(if usrattr_id attrx=usrattr_id attr\<and>
- usrattr_id attr\<noteq>nousrid
+(if usrattr_id attrx=usrattr_id attr
then
True
else find_usrid conf attr)"
@@ -36,25 +37,20 @@
primrec delete_usrattr::"UsrAttrConf\<Rightarrow>UsrAttr\<Rightarrow>UsrAttrConf" where
"delete_usrattr nousrattrconf attr=nousrattrconf"
| "delete_usrattr (usrattr_conf conf attrx) attr=
-(if usrattr_id attrx=usrattr_id attr\<and>
- usrattr_id attr\<noteq>nousrid
+(if usrattr_id attrx=usrattr_id attr
then
-conf
-else if usrattr_id attrx\<noteq>usrattr_id attr\<and>
- usrattr_id attr\<noteq>nousrid
+delete_usrattr conf attr
+else if usrattr_id attrx\<noteq>usrattr_id attr
then usrattr_conf(delete_usrattr conf attr) attrx
else usrattr_conf conf attrx)"
-
primrec get_usrattr::"UsrAttrConf\<Rightarrow>UsrId\<Rightarrow>UsrAttr" where
"get_usrattr nousrattrconf uid=nousrattr"
| "get_usrattr (usrattr_conf conf attr) uid=
-(if usrattr_id attr=uid\<and>
- uid\<noteq>nousrid
+(if usrattr_id attr=uid
then
attr
-else if usrattr_id attr\<noteq>uid\<and>
- uid\<noteq>nousrid
+else if usrattr_id attr\<noteq>uid
then
get_usrattr conf uid
else nousrattr)"
@@ -62,11 +58,11 @@
primrec valid_usrattrconf::"UsrAttrConf\<Rightarrow>bool" where
"valid_usrattrconf nousrattrconf=False"
| "valid_usrattrconf (usrattr_conf conf attr)=
-(if (\<not>find_usrid conf attr)\<and>
+(if usrattr_id attr\<noteq>nousrid\<and>
conf=nousrattrconf
then
True
-else if conf\<noteq>nousrattrconf\<and>
+else if usrattr_id attr\<noteq>nousrid\<and>
(\<not>find_usrid conf attr)\<and>
valid_usrattrconf conf
then
@@ -74,7 +70,7 @@
else False)"
primrec rel_subset_usr::"UsrAttrConf\<Rightarrow>UsrAttrConf\<Rightarrow>bool" where
-"rel_subset_usr conf1 nousrattrconf=False" |
+"rel_subset_usr conf1 nousrattrconf=True" |
"rel_subset_usr conf1 (usrattr_conf conf attr)=
(if conf=nousrattrconf\<and>
find_usrid conf1 attr
@@ -117,72 +113,36 @@
show "\<not>find_usrid nousrattrconf attr" by auto
next
fix conf
- fix attrx
fix attr
- show "conf = nousrattrconf \<and>
- usrattr_id attr \<noteq> nousrid \<and>
- usrattr_id attrx = usrattr_id attr \<Longrightarrow>
- find_usrid (usrattr_conf conf attrx) attr" by (auto simp:nousrattr_def)
-next
- fix conf
fix attrx
- fix attr
- show "conf \<noteq> nousrattrconf \<and>
- usrattr_id attr \<noteq> nousrid \<and>
- usrattr_id attrx = usrattr_id attr \<Longrightarrow>
- find_usrid (usrattr_conf conf attrx) attr" by (auto simp:nousrattr_def)
-next
- fix conf attr attrx
- show "find_usrid conf attr \<and> usrattr_id attr = usrattr_id attrx \<Longrightarrow>
- find_usrid conf attrx"
- proof (induct conf)
- case nousrattrconf
- then show ?case by auto
- next
- case (usrattr_conf conf x2)
- then show ?case by auto
- qed
-next
- fix conf
- fix attrx
- fix attr
- show "conf \<noteq> nousrattrconf \<and> find_usrid conf attr \<Longrightarrow>
+ show "usrattr_id attrx = usrattr_id attr \<Longrightarrow>
find_usrid (usrattr_conf conf attrx) attr" by auto
next
fix conf
fix attrx
fix attr
- show "\<not> (conf = nousrattrconf \<and>
- usrattr_id attr \<noteq> nousrid \<and>
- usrattr_id attrx = usrattr_id attr \<or>
- conf \<noteq> nousrattrconf \<and>
- usrattr_id attr \<noteq> nousrid \<and>
- usrattr_id attrx = usrattr_id attr \<or>
- conf \<noteq> nousrattrconf \<and> find_usrid conf attr) \<Longrightarrow>
- \<not> find_usrid (usrattr_conf conf attrx) attr" by (auto simp:nousrid_def)
+ show "find_usrid conf attr \<Longrightarrow>
+ find_usrid (usrattr_conf conf attrx) attr" by auto
+next
+ fix conf attr attrx
+ show "\<not> find_usrid conf attr \<and>
+ usrattr_id attrx \<noteq> usrattr_id attr \<Longrightarrow>
+ \<not> find_usrid (usrattr_conf conf attrx) attr" by auto
next
fix attr
show "delete_usrattr nousrattrconf attr = nousrattrconf" by auto
next
+ fix conf
fix attrx
fix attr
- fix conf
- show "usrattr_id attrx = usrattr_id attr \<and>
- usrattr_id attr \<noteq> nousrid \<Longrightarrow>
- delete_usrattr (usrattr_conf conf attrx) attr = conf" by auto
-next
- fix attrx
- fix attr
- fix conf
- show "usrattr_id attr = nousrid \<Longrightarrow>
+ show "usrattr_id attrx = usrattr_id attr \<Longrightarrow>
delete_usrattr (usrattr_conf conf attrx) attr =
- usrattr_conf conf attrx" by auto
+ delete_usrattr conf attr" by auto
next
fix attrx
fix attr
fix conf
- show "usrattr_id attrx \<noteq> usrattr_id attr \<and>
- usrattr_id attr \<noteq> nousrid \<Longrightarrow>
+ show "usrattr_id attrx \<noteq> usrattr_id attr \<Longrightarrow>
delete_usrattr (usrattr_conf conf attrx) attr =
usrattr_conf (delete_usrattr conf attr) attrx" by auto
next
@@ -192,41 +152,60 @@
fix attr
fix elem
fix conf
- show "elem \<noteq> nousrid \<and> usrattr_id attr = elem \<Longrightarrow>
+ show "usrattr_id attr = elem \<Longrightarrow>
get_usrattr (usrattr_conf conf attr) elem = attr" by auto
next
- fix attr
fix elem
+ fix attr
fix conf
- show "elem = nousrid \<Longrightarrow>
+ show "get_usrattr conf elem = nousrattr \<and>
+ usrattr_id attr \<noteq> elem \<Longrightarrow>
get_usrattr (usrattr_conf conf attr) elem = nousrattr" by auto
next
+ fix conf
fix elem
fix attr
- fix conf
- show "elem \<noteq> nousrid \<and> usrattr_id attr \<noteq> elem \<Longrightarrow>
- get_usrattr (usrattr_conf conf attr) elem =
- get_usrattr conf elem" by auto
+ show "get_usrattr conf elem \<noteq> nousrattr \<and>
+ usrattr_id attr \<noteq> elem \<Longrightarrow>
+ get_usrattr (usrattr_conf conf attr) elem = get_usrattr conf elem" by auto
next
show "\<not> valid_usrattrconf nousrattrconf" by auto
next
fix conf
fix attr
- show "conf = nousrattrconf \<and> \<not> find_usrid conf attr \<Longrightarrow>
+ show "usrattr_id attr \<noteq> nousrid \<and> conf = nousrattrconf \<Longrightarrow>
valid_usrattrconf (usrattr_conf conf attr)" by auto
next
fix conf
fix attr
- show "conf \<noteq> nousrattrconf \<and>
- \<not> find_usrid conf attr \<and> valid_usrattrconf conf \<Longrightarrow>
+ show "valid_usrattrconf conf \<and>
+ \<not> find_usrid conf attr \<and> usrattr_id attr \<noteq> nousrid \<Longrightarrow>
valid_usrattrconf (usrattr_conf conf attr)" by auto
next
fix conf
fix attr
- show "\<not> (conf = nousrattrconf \<and> \<not> find_usrid conf attr \<or>
- conf \<noteq> nousrattrconf \<and>
- \<not> find_usrid conf attr \<and> valid_usrattrconf conf) \<Longrightarrow>
+ show "usrattr_id attr = nousrid \<Longrightarrow>
\<not> valid_usrattrconf (usrattr_conf conf attr)" by auto
+next
+ fix conf
+ fix attr
+ show "conf \<noteq> nousrattrconf \<and> \<not> valid_usrattrconf conf \<Longrightarrow>
+ \<not> valid_usrattrconf (usrattr_conf conf attr)" by auto
+next
+ fix conf
+ fix attr
+ show "conf \<noteq> nousrattrconf \<and> find_usrid conf attr \<Longrightarrow>
+ \<not> valid_usrattrconf (usrattr_conf conf attr)" by auto
+next
+ show "\<And>P conf.
+ P nousrattrconf \<Longrightarrow>
+ (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (usrattr_conf conf1 attr1)) \<Longrightarrow>
+ P conf"
+ proof (erule UsrAttrConf.induct)
+ show "\<And>P conf x1 x2.
+ (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (usrattr_conf conf1 attr1)) \<Longrightarrow>
+ P x1 \<Longrightarrow> P (usrattr_conf x1 x2)" by auto
+ qed
qed
interpretation UsrAttrConfRel : AttrConfRel nousrid nousrattr nousrattrconf usrattr_conf is_usrattrconf
@@ -234,7 +213,7 @@
rel_subset_usr
proof
fix confx
- show "\<not> rel_subset_usr confx nousrattrconf" by auto
+ show "rel_subset_usr confx nousrattrconf" by auto
next
fix conf
fix confx
@@ -252,128 +231,14 @@
fix conf
fix confx
fix attr
- show "\<not> (conf \<noteq> nousrattrconf \<and>
- find_usrid confx attr \<and> rel_subset_usr confx conf \<or>
- conf = nousrattrconf \<and> find_usrid confx attr) \<Longrightarrow>
+ show "\<not> rel_subset_usr confx conf \<Longrightarrow>
\<not> rel_subset_usr confx (usrattr_conf conf attr)" by auto
next
- fix confx conf attr
- show "rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow>
- find_usrid confx attr"
- proof (induct conf)
- case nousrattrconf
- then show ?case by auto
- next
- case (usrattr_conf conf x2)
- then show ?case
- proof (auto)
- show "(rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow>
- find_usrid confx attr) \<Longrightarrow>
- if conf = nousrattrconf \<and> find_usrid confx x2 then True
- else if conf \<noteq> nousrattrconf \<and> find_usrid confx x2
- then rel_subset_usr confx conf else False \<Longrightarrow>
- if usrattr_id x2 = usrattr_id attr \<and> usrattr_id attr \<noteq> nousrid
- then True else find_usrid conf attr \<Longrightarrow>
- find_usrid confx attr"
- proof (split if_split_asm)
- show "if usrattr_id x2 = usrattr_id attr \<and> usrattr_id attr \<noteq> nousrid
- then True else find_usrid conf attr \<Longrightarrow>
- (rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow>
- find_usrid confx attr) \<Longrightarrow>
- conf = nousrattrconf \<Longrightarrow>
- find_usrid confx x2 \<Longrightarrow> True \<Longrightarrow> find_usrid confx attr"
- proof (split if_split_asm)
- assume 0:"find_usrid confx x2"
- assume 1:"usrattr_id x2 = usrattr_id attr"
- from 0 1 show "find_usrid confx attr"
- proof (induct confx)
- case nousrattrconf
- then show ?case by auto
- next
- case (usrattr_conf confx x2)
- then show ?case by auto
- qed
- next
- show "(rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow>
- find_usrid confx attr) \<Longrightarrow>
- conf = nousrattrconf \<Longrightarrow>
- find_usrid confx x2 \<Longrightarrow>
- True \<Longrightarrow>
- \<not> (usrattr_id x2 = usrattr_id attr \<and>
- usrattr_id attr \<noteq> nousrid) \<Longrightarrow>
- find_usrid conf attr \<Longrightarrow> find_usrid confx attr " by auto
- qed
- next
- show "if usrattr_id x2 = usrattr_id attr \<and> usrattr_id attr \<noteq> nousrid
- then True else find_usrid conf attr \<Longrightarrow>
- (rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow>
- find_usrid confx attr) \<Longrightarrow>
- \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow>
- if conf \<noteq> nousrattrconf \<and> find_usrid confx x2
- then rel_subset_usr confx conf else False \<Longrightarrow>
- find_usrid confx attr"
- proof (split if_split_asm)
- show "(rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow>
- find_usrid confx attr) \<Longrightarrow>
- \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow>
- if conf \<noteq> nousrattrconf \<and> find_usrid confx x2
- then rel_subset_usr confx conf else False \<Longrightarrow>
- usrattr_id x2 = usrattr_id attr \<Longrightarrow>
- usrattr_id attr \<noteq> nousrid \<Longrightarrow> True \<Longrightarrow> find_usrid confx attr"
- proof (split if_split_asm)
- show "usrattr_id x2 = usrattr_id attr \<Longrightarrow>
- usrattr_id attr \<noteq> nousrid \<Longrightarrow>
- True \<Longrightarrow>
- (rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow>
- find_usrid confx attr) \<Longrightarrow>
- \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow>
- \<not> (conf \<noteq> nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow>
- False \<Longrightarrow> find_usrid confx attr" by auto
- next
- assume 0:"find_usrid confx x2"
- assume 1:"usrattr_id x2 = usrattr_id attr"
- from 0 1 show "find_usrid confx attr"
- proof (induct confx)
- case nousrattrconf
- then show ?case by auto
- next
- case (usrattr_conf confx x2)
- then show ?case by auto
- qed
- qed
- next
- show "(rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow>
- find_usrid confx attr) \<Longrightarrow>
- \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow>
- if conf \<noteq> nousrattrconf \<and> find_usrid confx x2
- then rel_subset_usr confx conf else False \<Longrightarrow>
- \<not> (usrattr_id x2 = usrattr_id attr \<and>
- usrattr_id attr \<noteq> nousrid) \<Longrightarrow>
- find_usrid conf attr \<Longrightarrow> find_usrid confx attr"
- proof (split if_split_asm)
- show " \<not> (usrattr_id x2 = usrattr_id attr \<and>
- usrattr_id attr \<noteq> nousrid) \<Longrightarrow>
- find_usrid conf attr \<Longrightarrow>
- (rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow>
- find_usrid confx attr) \<Longrightarrow>
- \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow>
- conf \<noteq> nousrattrconf \<Longrightarrow>
- find_usrid confx x2 \<Longrightarrow>
- rel_subset_usr confx conf \<Longrightarrow> find_usrid confx attr" by auto
- next
- show "\<not> (usrattr_id x2 = usrattr_id attr \<and>
- usrattr_id attr \<noteq> nousrid) \<Longrightarrow>
- find_usrid conf attr \<Longrightarrow>
- (rel_subset_usr confx conf \<and> find_usrid conf attr \<Longrightarrow>
- find_usrid confx attr) \<Longrightarrow>
- \<not> (conf = nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow>
- \<not> (conf \<noteq> nousrattrconf \<and> find_usrid confx x2) \<Longrightarrow>
- False \<Longrightarrow> find_usrid confx attr" by auto
- qed
- qed
- qed
- qed
- qed
+ fix confx
+ fix conf
+ fix attr
+ show "rel_subset_usr confx conf \<and> \<not> find_usrid confx attr \<Longrightarrow>
+ \<not> rel_subset_usr confx (usrattr_conf conf attr)" by auto
qed
end
diff --git a/access_control_module/interpretation/I_FMT_MSA.thy b/access_control_module/interpretation/I_FMT_MSA.thy
index 480fbca..2d92a2b 100644
--- a/access_control_module/interpretation/I_FMT_MSA.thy
+++ b/access_control_module/interpretation/I_FMT_MSA.thy
@@ -30,8 +30,7 @@
primrec find_subjid::"SubjAttrConf\<Rightarrow>SubjAttr\<Rightarrow>bool" where
"find_subjid nosubjattrconf sattr=False"
| "find_subjid (subjattr_conf conf sattrx) sattr=
-(if subjattr_subjid sattrx=subjattr_subjid sattr\<and>
- subjattr_subjid sattr\<noteq>noresrcid
+(if subjattr_subjid sattrx=subjattr_subjid sattr
then
True
else find_subjid conf sattr)"
@@ -39,12 +38,10 @@
primrec delete_subjattr::"SubjAttrConf\<Rightarrow>SubjAttr\<Rightarrow>SubjAttrConf" where
"delete_subjattr nosubjattrconf sattr=nosubjattrconf"
| "delete_subjattr (subjattr_conf conf sattrx) sattr=
-(if subjattr_subjid sattrx=subjattr_subjid sattr\<and>
- subjattr_subjid sattr\<noteq>noresrcid
+(if subjattr_subjid sattrx=subjattr_subjid sattr
then
-conf
-else if subjattr_subjid sattrx\<noteq>subjattr_subjid sattr\<and>
- subjattr_subjid sattr\<noteq>noresrcid
+delete_subjattr conf sattr
+else if subjattr_subjid sattrx\<noteq>subjattr_subjid sattr
then
subjattr_conf(delete_subjattr conf sattr) sattrx
else subjattr_conf conf sattrx)"
@@ -52,12 +49,10 @@
primrec get_subjattr::"SubjAttrConf\<Rightarrow>ResrcId\<Rightarrow>SubjAttr" where
"get_subjattr nosubjattrconf rid=nosubjattr"
| "get_subjattr (subjattr_conf conf sattr) rid=
-(if subjattr_subjid sattr=rid\<and>
- rid\<noteq>noresrcid
+(if subjattr_subjid sattr=rid
then
sattr
-else if subjattr_subjid sattr\<noteq>rid\<and>
- rid\<noteq>noresrcid
+else if subjattr_subjid sattr\<noteq>rid
then
get_subjattr conf rid
else nosubjattr)"
@@ -65,11 +60,11 @@
primrec subjattrconf_uniq::"SubjAttrConf\<Rightarrow>bool" where
"subjattrconf_uniq nosubjattrconf=False"
| "subjattrconf_uniq (subjattr_conf conf sattr)=
-(if (\<not>find_subjid conf sattr)\<and>
+(if subjattr_subjid sattr\<noteq>noresrcid\<and>
conf=nosubjattrconf
then
True
-else if conf\<noteq>nosubjattrconf\<and>
+else if subjattr_subjid sattr\<noteq>noresrcid\<and>
(\<not>find_subjid conf sattr)\<and>
subjattrconf_uniq conf
then
@@ -126,56 +121,30 @@
(\<exists>conf attr. x = subjattr_conf conf attr)" by auto
qed
next
+ show "subjattr_subjid nosubjattr = noresrcid"
+ by (auto simp add:subjattr_subjid_def nosubjattr_def noresrcattr_def)
+next
fix attr
show "\<not> find_subjid nosubjattrconf attr" by auto
next
- show "subjattr_subjid nosubjattr = noresrcid"
- by (auto simp:subjattr_subjid_def nosubjattr_def noresrcattr_def)
+ fix attrx
+ fix attr
+ fix conf
+ show "subjattr_subjid attrx = subjattr_subjid attr \<Longrightarrow>
+ find_subjid (subjattr_conf conf attrx) attr"
+ by auto
next
fix conf
fix attrx
fix attr
- show "conf = nosubjattrconf \<and>
- subjattr_subjid attr \<noteq> noresrcid \<and>
- subjattr_subjid attrx = subjattr_subjid attr \<Longrightarrow>
+ show "find_subjid conf attr \<Longrightarrow>
find_subjid (subjattr_conf conf attrx) attr" by auto
next
fix conf
fix attrx
fix attr
- show "conf \<noteq> nosubjattrconf \<and>
- subjattr_subjid attr \<noteq> noresrcid \<and>
- subjattr_subjid attrx = subjattr_subjid attr \<Longrightarrow>
- find_subjid (subjattr_conf conf attrx) attr" by auto
-next
- fix conf
- fix attrx
- fix attr
- show "conf \<noteq> nosubjattrconf \<and> find_subjid conf attr \<Longrightarrow>
- find_subjid (subjattr_conf conf attrx) attr" by auto
-next
- fix conf attr attrx
- show "find_subjid conf attr \<and>
- subjattr_subjid attr = subjattr_subjid attrx \<Longrightarrow>
- find_subjid conf attrx"
- proof (induct conf)
- case nosubjattrconf
- then show ?case by auto
- next
- case (subjattr_conf conf x2)
- then show ?case by auto
- qed
-next
- fix conf
- fix attrx
- fix attr
- show "\<not> (conf = nosubjattrconf \<and>
- subjattr_subjid attr \<noteq> noresrcid \<and>
- subjattr_subjid attrx = subjattr_subjid attr \<or>
- conf \<noteq> nosubjattrconf \<and>
- subjattr_subjid attr \<noteq> noresrcid \<and>
- subjattr_subjid attrx = subjattr_subjid attr \<or>
- conf \<noteq> nosubjattrconf \<and> find_subjid conf attr) \<Longrightarrow>
+ show "\<not> find_subjid conf attr \<and>
+ subjattr_subjid attrx \<noteq> subjattr_subjid attr \<Longrightarrow>
\<not> find_subjid (subjattr_conf conf attrx) attr" by auto
next
fix attr
@@ -184,22 +153,14 @@
fix attrx
fix attr
fix conf
- show "subjattr_subjid attrx = subjattr_subjid attr \<and>
- subjattr_subjid attr \<noteq> noresrcid \<Longrightarrow>
- delete_subjattr (subjattr_conf conf attrx) attr = conf" by auto
-next
- fix attrx
- fix attr
- fix conf
- show "subjattr_subjid attr = noresrcid \<Longrightarrow>
+ show "subjattr_subjid attrx = subjattr_subjid attr \<Longrightarrow>
delete_subjattr (subjattr_conf conf attrx) attr =
- subjattr_conf conf attrx" by auto
+ delete_subjattr conf attr" by auto
next
fix attrx
fix attr
fix conf
- show "subjattr_subjid attrx \<noteq> subjattr_subjid attr \<and>
- subjattr_subjid attr \<noteq> noresrcid \<Longrightarrow>
+ show "subjattr_subjid attrx \<noteq> subjattr_subjid attr \<Longrightarrow>
delete_subjattr (subjattr_conf conf attrx) attr =
subjattr_conf (delete_subjattr conf attr) attrx" by auto
next
@@ -209,19 +170,21 @@
fix attr
fix elem
fix conf
- show "elem \<noteq> noresrcid \<and> subjattr_subjid attr = elem \<Longrightarrow>
+ show "subjattr_subjid attr = elem \<Longrightarrow>
get_subjattr (subjattr_conf conf attr) elem = attr" by auto
next
fix attr
fix elem
fix conf
- show "elem = noresrcid \<Longrightarrow>
+ show "get_subjattr conf elem = nosubjattr \<and>
+ subjattr_subjid attr \<noteq> elem \<Longrightarrow>
get_subjattr (subjattr_conf conf attr) elem = nosubjattr" by auto
next
fix elem
fix attr
fix conf
- show "elem \<noteq> noresrcid \<and> subjattr_subjid attr \<noteq> elem \<Longrightarrow>
+ show "get_subjattr conf elem \<noteq> nosubjattr \<and>
+ subjattr_subjid attr \<noteq> elem \<Longrightarrow>
get_subjattr (subjattr_conf conf attr) elem =
get_subjattr conf elem" by auto
next
@@ -229,22 +192,40 @@
next
fix conf
fix attr
- show "conf = nosubjattrconf \<and> \<not> find_subjid conf attr \<Longrightarrow>
+ show "subjattr_subjid attr \<noteq> noresrcid \<and> conf = nosubjattrconf \<Longrightarrow>
subjattrconf_uniq (subjattr_conf conf attr)" by auto
next
fix conf
fix attr
- show "conf \<noteq> nosubjattrconf \<and>
- \<not> find_subjid conf attr \<and> subjattrconf_uniq conf \<Longrightarrow>
+ show "subjattrconf_uniq conf \<and>
+ \<not> find_subjid conf attr \<and> subjattr_subjid attr \<noteq> noresrcid \<Longrightarrow>
subjattrconf_uniq (subjattr_conf conf attr)" by auto
next
fix conf
fix attr
- show "\<not> (conf = nosubjattrconf \<and> \<not> find_subjid conf attr \<or>
- conf \<noteq> nosubjattrconf \<and>
- \<not> find_subjid conf attr \<and> subjattrconf_uniq conf) \<Longrightarrow>
+ show "subjattr_subjid attr = noresrcid \<Longrightarrow>
\<not> subjattrconf_uniq (subjattr_conf conf attr)" by auto
next
+ fix conf
+ fix attr
+ show "conf \<noteq> nosubjattrconf \<and> \<not> subjattrconf_uniq conf \<Longrightarrow>
+ \<not> subjattrconf_uniq (subjattr_conf conf attr)" by auto
+next
+ fix conf
+ fix attr
+ show "conf \<noteq> nosubjattrconf \<and> find_subjid conf attr \<Longrightarrow>
+ \<not> subjattrconf_uniq (subjattr_conf conf attr)" by auto
+next
+ show "\<And>P conf.
+ P nosubjattrconf \<Longrightarrow>
+ (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (subjattr_conf conf1 attr1)) \<Longrightarrow>
+ P conf"
+ proof (erule SubjAttrConf.induct)
+ show "\<And>P conf x1 x2.
+ (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (subjattr_conf conf1 attr1)) \<Longrightarrow>
+ P x1 \<Longrightarrow> P (subjattr_conf x1 x2)" by auto
+ qed
+next
fix sattr
show "subjattr_subjid sattr = presrc_id (subj_resrcattr sattr)"
by (auto simp:subjattr_subjid_def)
@@ -319,8 +300,7 @@
primrec find_objid::"ObjAttrConf\<Rightarrow>ObjAttr\<Rightarrow>bool" where
"find_objid noobjattrconf oattr=False"
| "find_objid (objattr_conf conf oattrx) oattr=
-(if objattr_objid oattrx=objattr_objid oattr \<and>
- objattr_objid oattr\<noteq>noresrcid
+(if objattr_objid oattrx=objattr_objid oattr
then
True
else find_objid conf oattr)"
@@ -328,12 +308,10 @@
primrec delete_objattr::"ObjAttrConf\<Rightarrow>ObjAttr\<Rightarrow>ObjAttrConf" where
"delete_objattr noobjattrconf oattr=noobjattrconf"
| "delete_objattr (objattr_conf conf oattrx) oattr=
-(if objattr_objid oattrx=objattr_objid oattr \<and>
- objattr_objid oattr\<noteq>noresrcid
+(if objattr_objid oattrx=objattr_objid oattr
then
-conf
-else if objattr_objid oattrx\<noteq>objattr_objid oattr \<and>
- objattr_objid oattr\<noteq>noresrcid
+delete_objattr conf oattr
+else if objattr_objid oattrx\<noteq>objattr_objid oattr
then
objattr_conf(delete_objattr conf oattr) oattrx
else objattr_conf conf oattrx)"
@@ -341,12 +319,10 @@
primrec get_objattr::"ObjAttrConf\<Rightarrow>ResrcId\<Rightarrow>ObjAttr" where
"get_objattr noobjattrconf rid=noobjattr"
| "get_objattr (objattr_conf conf oattr) rid=
-(if objattr_objid oattr=rid \<and>
- rid\<noteq>noresrcid
+(if objattr_objid oattr=rid
then
oattr
-else if objattr_objid oattr\<noteq>rid \<and>
- rid\<noteq>noresrcid
+else if objattr_objid oattr\<noteq>rid
then
get_objattr conf rid
else noobjattr)"
@@ -354,11 +330,11 @@
primrec valid_objattrconf::"ObjAttrConf\<Rightarrow>bool" where
"valid_objattrconf noobjattrconf=False"
| "valid_objattrconf (objattr_conf conf oattr)=
-(if (\<not>find_objid conf oattr)\<and>
+(if objattr_objid oattr\<noteq>noresrcid\<and>
conf=noobjattrconf
then
True
-else if conf\<noteq>noobjattrconf\<and>
+else if objattr_objid oattr\<noteq>noresrcid\<and>
(\<not>find_objid conf oattr)\<and>
valid_objattrconf conf
then
@@ -405,47 +381,19 @@
fix conf
fix attrx
fix attr
- show "conf = noobjattrconf \<and>
- objattr_objid attr \<noteq> noresrcid \<and>
- objattr_objid attrx = objattr_objid attr \<Longrightarrow>
+ show "objattr_objid attrx = objattr_objid attr \<Longrightarrow>
find_objid (objattr_conf conf attrx) attr" by auto
next
fix conf
fix attrx
fix attr
- show "conf \<noteq> noobjattrconf \<and>
- objattr_objid attr \<noteq> noresrcid \<and>
- objattr_objid attrx = objattr_objid attr \<Longrightarrow>
- find_objid (objattr_conf conf attrx) attr" by auto
+ show "find_objid conf attr \<Longrightarrow> find_objid (objattr_conf conf attrx) attr" by auto
next
fix conf
fix attrx
fix attr
- show "conf \<noteq> noobjattrconf \<and> find_objid conf attr \<Longrightarrow>
- find_objid (objattr_conf conf attrx) attr" by auto
-next
- fix conf attr attrx
- show "find_objid conf attr \<and>
- objattr_objid attr = objattr_objid attrx \<Longrightarrow>
- find_objid conf attrx"
- proof (induct conf)
- case noobjattrconf
- then show ?case by auto
- next
- case (objattr_conf conf x2)
- then show ?case by auto
- qed
-next
- fix conf
- fix attrx
- fix attr
- show "\<not> (conf = noobjattrconf \<and>
- objattr_objid attr \<noteq> noresrcid \<and>
- objattr_objid attrx = objattr_objid attr \<or>
- conf \<noteq> noobjattrconf \<and>
- objattr_objid attr \<noteq> noresrcid \<and>
- objattr_objid attrx = objattr_objid attr \<or>
- conf \<noteq> noobjattrconf \<and> find_objid conf attr) \<Longrightarrow>
+ show "\<not> find_objid conf attr \<and>
+ objattr_objid attrx \<noteq> objattr_objid attr \<Longrightarrow>
\<not> find_objid (objattr_conf conf attrx) attr" by auto
next
fix attr
@@ -454,22 +402,14 @@
fix attrx
fix attr
fix conf
- show "objattr_objid attrx = objattr_objid attr \<and>
- objattr_objid attr \<noteq> noresrcid \<Longrightarrow>
- delete_objattr (objattr_conf conf attrx) attr = conf" by auto
-next
- fix attrx
- fix attr
- fix conf
- show "objattr_objid attr = noresrcid \<Longrightarrow>
+ show "objattr_objid attrx = objattr_objid attr \<Longrightarrow>
delete_objattr (objattr_conf conf attrx) attr =
- objattr_conf conf attrx" by auto
+ delete_objattr conf attr" by auto
next
fix attrx
fix attr
fix conf
- show "objattr_objid attrx \<noteq> objattr_objid attr \<and>
- objattr_objid attr \<noteq> noresrcid \<Longrightarrow>
+ show "objattr_objid attrx \<noteq> objattr_objid attr \<Longrightarrow>
delete_objattr (objattr_conf conf attrx) attr =
objattr_conf (delete_objattr conf attr) attrx" by auto
next
@@ -479,42 +419,59 @@
fix attr
fix elem
fix conf
- show "elem \<noteq> noresrcid \<and> objattr_objid attr = elem \<Longrightarrow>
+ show "objattr_objid attr = elem \<Longrightarrow>
get_objattr (objattr_conf conf attr) elem = attr" by auto
next
fix attr
fix elem
fix conf
- show "elem = noresrcid \<Longrightarrow>
+ show "get_objattr conf elem = noobjattr \<and> objattr_objid attr \<noteq> elem \<Longrightarrow>
get_objattr (objattr_conf conf attr) elem = noobjattr" by auto
next
fix elem
fix attr
fix conf
- show "elem \<noteq> noresrcid \<and> objattr_objid attr \<noteq> elem \<Longrightarrow>
- get_objattr (objattr_conf conf attr) elem =
- get_objattr conf elem" by auto
+ show "get_objattr conf elem \<noteq> noobjattr \<and> objattr_objid attr \<noteq> elem \<Longrightarrow>
+ get_objattr (objattr_conf conf attr) elem = get_objattr conf elem" by auto
next
show "\<not> valid_objattrconf noobjattrconf" by auto
next
fix conf
fix attr
- show "conf = noobjattrconf \<and> \<not> find_objid conf attr \<Longrightarrow>
+ show "objattr_objid attr \<noteq> noresrcid \<and> conf = noobjattrconf \<Longrightarrow>
valid_objattrconf (objattr_conf conf attr)" by auto
next
fix conf
fix attr
- show "conf \<noteq> noobjattrconf \<and>
- \<not> find_objid conf attr \<and> valid_objattrconf conf \<Longrightarrow>
+ show "valid_objattrconf conf \<and>
+ \<not> find_objid conf attr \<and> objattr_objid attr \<noteq> noresrcid \<Longrightarrow>
valid_objattrconf (objattr_conf conf attr)" by auto
next
fix conf
fix attr
- show "\<not> (conf = noobjattrconf \<and> \<not> find_objid conf attr \<or>
- conf \<noteq> noobjattrconf \<and>
- \<not> find_objid conf attr \<and> valid_objattrconf conf) \<Longrightarrow>
+ show "objattr_objid attr = noresrcid \<Longrightarrow>
\<not> valid_objattrconf (objattr_conf conf attr)" by auto
next
+ fix conf
+ fix attr
+ show "conf \<noteq> noobjattrconf \<and> \<not> valid_objattrconf conf \<Longrightarrow>
+ \<not> valid_objattrconf (objattr_conf conf attr)" by auto
+next
+ fix conf
+ fix attr
+ show "conf \<noteq> noobjattrconf \<and> find_objid conf attr \<Longrightarrow>
+ \<not> valid_objattrconf (objattr_conf conf attr)" by auto
+next
+ show "\<And>P conf.
+ P noobjattrconf \<Longrightarrow>
+ (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (objattr_conf conf1 attr1)) \<Longrightarrow>
+ P conf"
+ proof (erule ObjAttrConf.induct)
+ show "\<And>P conf x1 x2.
+ (\<And>conf1 attr1. P conf1 \<Longrightarrow> P (objattr_conf conf1 attr1)) \<Longrightarrow>
+ P x1 \<Longrightarrow> P (objattr_conf x1 x2)" by auto
+ qed
+next
fix oattr
show "objattr_objid oattr = presrc_id (obj_resrcattr oattr)"
by (auto simp:objattr_objid_def)
