first feedback on Yakoubs CC
This commit is contained in:
parent
1dd07880ea
commit
00c4d15259
|
|
@ -14,6 +14,9 @@ doc_class concept_definition = "definition" +
|
|||
status :: status <= "semiformal"
|
||||
mcc :: math_content_class <= "terminology"
|
||||
tag :: string
|
||||
short_tag :: "string option" <= "None"
|
||||
|
||||
text\<open>The \<^verbatim>\<open>short_tag\<close>, if set, is used in the presentation directly.\<close>
|
||||
|
||||
type_synonym concept = concept_definition
|
||||
|
||||
|
|
@ -316,12 +319,12 @@ the TOE is intended to address This statement consists of a combination of:
|
|||
\item the assumptions that are upheld for the operational environment of the TOE.
|
||||
\end{itemize}\<close>
|
||||
|
||||
Definition* [sr_def::concept, tag="''security requirement''"]
|
||||
Definition* [sr_def::concept, tag="''security requirement''", short_tag="Some(''SR'')"]
|
||||
\<open>requirement, stated in a standardised language, which is meant to contribute
|
||||
to achieving the security objectives for a TOE\<close>
|
||||
text \<open>@{docitem toe_def}\<close>
|
||||
Definition* [st_def::concept, tag="''Security Target''"]
|
||||
\<open>implementation-dependent statement of security needs for a specific identified @{docitem toe_def}\<close>
|
||||
Definition* [st_def::concept, tag="''Security Target''", short_tag="Some(''ST'')"]
|
||||
\<open>implementation-dependent statement of security needs for a specific i\<section>dentified @{docitem toe_def}\<close>
|
||||
|
||||
Definition* [slct_def::concept, tag="''selection''"]
|
||||
\<open>specification of one or more items from a list in a component\<close>
|
||||
|
|
@ -359,9 +362,9 @@ Definition* [toe_eval_def::concept, tag="''TOE evaluation''"]
|
|||
Definition* [toe_res_def::concept, tag="''TOE resource''"]
|
||||
\<open>anything useable or consumable in the TOE\<close>
|
||||
|
||||
Definition* [toe_sf_def::concept, tag="''TOE security functionality''"]
|
||||
\<open>combined functionality of all hardware, software, and firmware of a TOE that must be relied upon for the correct
|
||||
enforcement of the SFRs\<close>
|
||||
Definition* [toe_sf_def::concept, tag="''TOE security functionality''", short_tag= "Some(''TSF'')"]
|
||||
\<open>combined functionality of all hardware, software, and firmware of a TOE that must be relied upon
|
||||
for the correct enforcement of the @{docitem sfr_def}s\<close>
|
||||
|
||||
Definition* [tr_vrb_def::concept, tag="''trace, verb''"]
|
||||
\<open>perform an informal correspondence analysis between two entities with only a
|
||||
|
|
|
|||
|
|
@ -13,88 +13,113 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*************************************************************************)
|
||||
|
||||
(*<*)
|
||||
theory "CC_v3_1_R5"
|
||||
imports "../technical_report/technical_report"
|
||||
"CC_terminology"
|
||||
|
||||
|
||||
begin
|
||||
(*>*)
|
||||
|
||||
section \<open>General Infrastructure on CC Evaluations\<close>
|
||||
|
||||
datatype EALs = EAL1 | EAL2 | EAL3 | EAL4 | EAL5 | EAL6 | EAL7
|
||||
|
||||
doc_class CC_structure_element =(* text_element + *)
|
||||
tag_id :: string
|
||||
eval_level :: EALs
|
||||
|
||||
doc_class CC_text_element = text_element +
|
||||
eval_level :: EALs
|
||||
|
||||
section \<open>Security target ontology\<close>
|
||||
|
||||
|
||||
doc_class st_ref_cls = text_element +
|
||||
title :: string
|
||||
st_version:: "(int \<times> int \<times> int)"
|
||||
"authors":: "author list"
|
||||
"st_date" :: string
|
||||
doc_class st_ref_cls = CC_text_element +
|
||||
title :: string
|
||||
st_version:: "(int \<times> int \<times> int)"
|
||||
"authors":: "author list"
|
||||
"st_date" :: string
|
||||
|
||||
doc_class toe_ref_cls = text_element +
|
||||
doc_class toe_ref_cls = CC_text_element +
|
||||
dev_name:: string
|
||||
toe_name:: string
|
||||
toe_version:: "(int \<times> int \<times> int)"
|
||||
prod_name::"string option" <= None
|
||||
|
||||
doc_class toe_ovrw_cls = text_element +
|
||||
toe_type :: string
|
||||
software_req :: "text_element list option" <= None
|
||||
hardware_req :: "text_element list option" <= None
|
||||
firmeware_req:: "text_element list option" <= None
|
||||
features_req :: "text_element list option" <= None
|
||||
|
||||
doc_class toe_desc_cls = text_element +
|
||||
software_list :: "text_element list option" <= None
|
||||
hardware_list :: "text_element list option" <= None
|
||||
firmeware_list:: "text_element list option" <= None
|
||||
sec_features_list:: "text_element list option" <= None
|
||||
doc_class toe_ovrw_cls = CC_text_element +
|
||||
toe_type :: string
|
||||
software_req :: "CC_text_element list" <= "[]"
|
||||
hardware_req :: "CC_text_element list" <= "[]"
|
||||
firmeware_req:: "CC_text_element list" <= "[]"
|
||||
features_req :: "CC_text_element list" <= "[]"
|
||||
invariant eal_consistency::
|
||||
"\<lambda> X::toe_ovrw_cls .
|
||||
(case eval_level X of
|
||||
EAL1 \<Rightarrow> software_req X \<noteq> []
|
||||
| EAL2 \<Rightarrow> software_req X \<noteq> []
|
||||
| EAL3 \<Rightarrow> software_req X \<noteq> []
|
||||
| EAL4 \<Rightarrow> software_req X \<noteq> []
|
||||
| _ \<Rightarrow> undefined)"
|
||||
|
||||
thm eal_consistency_inv_def
|
||||
|
||||
doc_class toe_desc_cls = CC_text_element +
|
||||
software_list :: "CC_text_element list" <= "[]"
|
||||
hardware_list :: "CC_text_element list" <= "[]"
|
||||
firmeware_list :: "CC_text_element list" <= "[]"
|
||||
sec_features_list:: "CC_text_element list" <= "[]"
|
||||
|
||||
doc_class ST_INTRO_MNT =
|
||||
stint_id:: string
|
||||
accepts "(\<lbrace>st_ref_cls\<rbrace>\<^sup>+ ~~ \<lbrace>toe_ref_cls\<rbrace>\<^sup>+ ~~ \<lbrace>toe_ovrw_cls\<rbrace>\<^sup>+ ~~ \<lbrace>toe_desc_cls\<rbrace>\<^sup>+)"
|
||||
doc_class ST_INTRO_MNT = CC_structure_element +
|
||||
tag_id:: string
|
||||
accepts "\<lbrace>st_ref_cls\<rbrace>\<^sup>* ~~ \<lbrace>toe_ref_cls\<rbrace>\<^sup>* ~~ \<lbrace>toe_ovrw_cls\<rbrace>\<^sup>* ~~ \<lbrace>toe_desc_cls\<rbrace>\<^sup>*"
|
||||
|
||||
doc_class cc_conf_claim_cls = text_element +
|
||||
cc_version:: string
|
||||
ext_srs_list::"text_element list option"
|
||||
doc_class cc_conf_claim_cls = CC_text_element +
|
||||
cc_version:: string
|
||||
ext_srs_list::"CC_text_element list option"
|
||||
|
||||
doc_class pp_clms_cls = text_element +
|
||||
pp_pckgs_list::"text_element list option"
|
||||
pp_config_list::"text_element list option"
|
||||
doc_class pp_clms_cls = CC_text_element +
|
||||
pp_pckgs_list::"CC_text_element list option"
|
||||
pp_config_list::"CC_text_element list option"
|
||||
|
||||
doc_class pckg_claim_cls = text_element +
|
||||
pckgs_list::"text_element list option"
|
||||
doc_class pckg_claim_cls = CC_text_element +
|
||||
pckgs_list::"CC_text_element list option"
|
||||
|
||||
doc_class conf_ratio =
|
||||
pp_config_list::"text_element list option"
|
||||
pp_config_list::"CC_text_element list option"
|
||||
|
||||
doc_class CONF_CLAIMS_MNT =
|
||||
ccl_id:: string
|
||||
accepts "(\<lbrace>cc_conf_claim_cls\<rbrace>\<^sup>+ ~~ \<lbrace>pp_clms_cls\<rbrace>\<^sup>* ~~ \<lbrace>pckg_claim_cls\<rbrace>\<^sup>+ ~~ \<lbrace>conf_ratio\<rbrace>\<^sup>*)"
|
||||
doc_class CONF_CLAIMS_MNT = CC_structure_element +
|
||||
tag_id:: string
|
||||
accepts "(\<lbrace>cc_conf_claim_cls\<rbrace>\<^sup>+ ~~ \<lbrace>pp_clms_cls\<rbrace>\<^sup>* ~~ \<lbrace>pckg_claim_cls\<rbrace>\<^sup>+ ~~ \<lbrace>conf_ratio\<rbrace>\<^sup>*)"
|
||||
|
||||
doc_class threats_cls = text_element +
|
||||
toe_thrts_list::"text_element list option"
|
||||
env_thrts_list::"text_element list option"
|
||||
thrt_agnts_list:: "text_element list option"
|
||||
advrt_acts_list:: "text_element list option"
|
||||
assts_list:: "text_element list option"
|
||||
doc_class threats_cls = CC_text_element +
|
||||
toe_thrts_list::"CC_text_element list option"
|
||||
env_thrts_list::"CC_text_element list option"
|
||||
thrt_agnts_list:: "CC_text_element list option"
|
||||
advrt_acts_list:: "CC_text_element list option"
|
||||
assts_list:: "CC_text_element list option"
|
||||
|
||||
doc_class osps_cls = text_element +
|
||||
toe_osps_list::"text_element list option"
|
||||
env_osps_list::"text_element list option"
|
||||
doc_class osps_cls = CC_text_element +
|
||||
toe_osps_list::"CC_text_element list option"
|
||||
env_osps_list::"CC_text_element list option"
|
||||
|
||||
doc_class assumptions_cls = text_element +
|
||||
assms_phy_list::"text_element list option"
|
||||
assms_prsnl_list::"text_element list option"
|
||||
assms_cnct_list::"text_element list option"
|
||||
doc_class assumptions_cls = CC_text_element +
|
||||
assms_phy_list::"CC_text_element list option"
|
||||
assms_prsnl_list::"CC_text_element list option"
|
||||
assms_cnct_list::"CC_text_element list option"
|
||||
|
||||
doc_class SEC_PROB_DEF_MNT =
|
||||
spd_id:: string
|
||||
doc_class SEC_PROB_DEF_MNT = CC_structure_element +
|
||||
tag_id:: string
|
||||
accepts "((\<lbrace>threats_cls\<rbrace>\<^sup>+ || \<lbrace>osps_cls\<rbrace>\<^sup>+) ~~ \<lbrace>assumptions_cls\<rbrace>\<^sup>+)"
|
||||
|
||||
doc_class toe_sec_obj_cls = text_element +
|
||||
toe_obj_list:: "text_element list"
|
||||
doc_class toe_sec_obj_cls = CC_text_element +
|
||||
toe_obj_list:: "CC_text_element list"
|
||||
|
||||
doc_class env_sec_obj_cls = text_element +
|
||||
env_goals_list:: "text_element list"
|
||||
env_sites_list :: "text_element list"
|
||||
doc_class env_sec_obj_cls = CC_text_element +
|
||||
env_goals_list:: "CC_text_element list"
|
||||
env_sites_list :: "CC_text_element list"
|
||||
|
||||
doc_class sec_obj_ratio =
|
||||
toe_thrts_obj_trace::"((threats_cls \<times> toe_sec_obj_cls) list) option"
|
||||
|
|
@ -103,44 +128,45 @@ doc_class sec_obj_ratio =
|
|||
env_thrts_obj_trace::"((threats_cls \<times> toe_sec_obj_cls) list) option"
|
||||
env_osps_obj_trace::"((osps_cls \<times> toe_sec_obj_cls) list) option"
|
||||
env_assms_obj_trace::"((assumptions_cls \<times> toe_sec_obj_cls) list) option"
|
||||
toe_thrts_just_list::"(text_element list) option"
|
||||
toe_osps_just_list::"(text_element list) option"
|
||||
toe_assms_just_list::"text_element list"
|
||||
env_thrts_just_list::"(text_element list) option"
|
||||
env_osps_just_list::"(text_element list) option"
|
||||
env_assms_just_list::"text_element list"
|
||||
toe_thrts_just_list::"(CC_text_element list) option"
|
||||
toe_osps_just_list::"(CC_text_element list) option"
|
||||
toe_assms_just_list::"CC_text_element list"
|
||||
env_thrts_just_list::"(CC_text_element list) option"
|
||||
env_osps_just_list::"(CC_text_element list) option"
|
||||
env_assms_just_list::"CC_text_element list"
|
||||
|
||||
doc_class ext_comp_def =
|
||||
ext_comp_list::"(text_element list) option"
|
||||
ext_comp_list::"(CC_text_element list) option"
|
||||
|
||||
doc_class SEC_OBJ_MNT =
|
||||
ccl_id:: string
|
||||
doc_class SEC_OBJ_MNT = CC_structure_element +
|
||||
tag_id:: string
|
||||
accepts "(\<lbrace>toe_sec_obj_cls\<rbrace>\<^sup>+ ~~ \<lbrace>env_sec_obj_cls\<rbrace>\<^sup>+ ~~ \<lbrace>sec_obj_ratio\<rbrace>\<^sup>*~~ \<lbrace>ext_comp_def\<rbrace>\<^sup>*)"
|
||||
|
||||
|
||||
doc_class sfrs_cls = text_element +
|
||||
doc_class sfrs_cls = CC_text_element +
|
||||
sfrs_language::"string"
|
||||
sfrs_operation::"text_element"
|
||||
sfrs_dependency::"text_element list option"
|
||||
sfrs_operation::"CC_text_element"
|
||||
sfrs_dependency::"CC_text_element list option"
|
||||
|
||||
doc_class sfrs_ratio_cls = text_element +
|
||||
doc_class sfrs_ratio_cls = CC_text_element +
|
||||
toe_sec_obj_sfrs_trace:: "(sfrs_cls \<times> toe_sec_obj_cls) list"
|
||||
toe_sec_obj_sfrs_just::"text_element list option"
|
||||
toe_sec_obj_sfrs_just::"CC_text_element list option"
|
||||
|
||||
doc_class sars_cls = text_element +
|
||||
doc_class sars_cls = CC_text_element +
|
||||
sars_language::"string"
|
||||
sars_operation::"text_element"
|
||||
sars_dependency::"text_element list option"
|
||||
sars_operation::"CC_text_element"
|
||||
sars_dependency::"CC_text_element list option"
|
||||
|
||||
doc_class sars_ratio_cls = text_element +
|
||||
sars_explain::"text_element list"
|
||||
doc_class sars_ratio_cls = CC_text_element +
|
||||
sars_explain::"CC_text_element list"
|
||||
|
||||
doc_class SEC_REQ_MNT =
|
||||
spd_id:: string
|
||||
accepts "(\<lbrace>sfrs_cls\<rbrace>\<^sup>+ ~~ \<lbrace>sfrs_ratio_cls\<rbrace>\<^sup>+ ~~ \<lbrace>sars_cls\<rbrace>\<^sup>+ ~~ \<lbrace>sars_ratio_cls\<rbrace>\<^sup>+)"
|
||||
|
||||
doc_class ST_MNT =
|
||||
st_id :: string
|
||||
doc_class ST_MNT = CC_structure_element +
|
||||
tag_id :: string
|
||||
level :: EALs
|
||||
accepts "(ST_INTRO_MNT ~~
|
||||
CONF_CLAIMS_MNT ~~
|
||||
SEC_PROB_DEF_MNT ~~
|
||||
|
|
|
|||
|
|
@ -177,11 +177,12 @@ val _ =
|
|||
)
|
||||
\<close>
|
||||
|
||||
textN\<open> \<^doof> \<^LATEX> \<close>
|
||||
textN\<open> \<^doof> \<^LATEX> \<close>
|
||||
|
||||
(* the same effect is achieved with : *)
|
||||
setup \<open>DOF_lib.define_shortcut ("bla",\<^here>) "\\bla"\<close>
|
||||
|
||||
setup \<open>DOF_lib.define_shortcut ("bla",\<^here>) "\\blabla"\<close>
|
||||
(* Note that this assumes that the generated LaTeX macro "blabla" is defined somewhere in the
|
||||
target document, for example, in the tex prelude. *)
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue