From 00c4d152596c8e2e0d80cf1298054cd7eea3ab83 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Wed, 26 Aug 2020 11:48:25 +0200 Subject: [PATCH] first feedback on Yakoubs CC --- src/ontologies/CC_v3.1_R5/CC_terminology.thy | 15 +- src/ontologies/CC_v3.1_R5/CC_v3_1_R5.thy | 172 +++++++++++-------- src/tests/OutOfOrderPresntn.thy | 7 +- 3 files changed, 112 insertions(+), 82 deletions(-) diff --git a/src/ontologies/CC_v3.1_R5/CC_terminology.thy b/src/ontologies/CC_v3.1_R5/CC_terminology.thy index c894472..38a8e55 100644 --- a/src/ontologies/CC_v3.1_R5/CC_terminology.thy +++ b/src/ontologies/CC_v3.1_R5/CC_terminology.thy @@ -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\The \<^verbatim>\short_tag\, if set, is used in the presentation directly.\ 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}\ -Definition* [sr_def::concept, tag="''security requirement''"] +Definition* [sr_def::concept, tag="''security requirement''", short_tag="Some(''SR'')"] \requirement, stated in a standardised language, which is meant to contribute to achieving the security objectives for a TOE\ text \@{docitem toe_def}\ -Definition* [st_def::concept, tag="''Security Target''"] -\implementation-dependent statement of security needs for a specific identified @{docitem toe_def}\ +Definition* [st_def::concept, tag="''Security Target''", short_tag="Some(''ST'')"] +\implementation-dependent statement of security needs for a specific i\
dentified @{docitem toe_def}\ Definition* [slct_def::concept, tag="''selection''"] \specification of one or more items from a list in a component\ @@ -359,9 +362,9 @@ Definition* [toe_eval_def::concept, tag="''TOE evaluation''"] Definition* [toe_res_def::concept, tag="''TOE resource''"] \anything useable or consumable in the TOE\ -Definition* [toe_sf_def::concept, tag="''TOE security functionality''"] -\combined functionality of all hardware, software, and firmware of a TOE that must be relied upon for the correct -enforcement of the SFRs\ +Definition* [toe_sf_def::concept, tag="''TOE security functionality''", short_tag= "Some(''TSF'')"] +\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\ Definition* [tr_vrb_def::concept, tag="''trace, verb''"] \perform an informal correspondence analysis between two entities with only a diff --git a/src/ontologies/CC_v3.1_R5/CC_v3_1_R5.thy b/src/ontologies/CC_v3.1_R5/CC_v3_1_R5.thy index 55e5a8c..73a087b 100644 --- a/src/ontologies/CC_v3.1_R5/CC_v3_1_R5.thy +++ b/src/ontologies/CC_v3.1_R5/CC_v3_1_R5.thy @@ -13,88 +13,113 @@ * SPDX-License-Identifier: BSD-2-Clause *************************************************************************) +(*<*) theory "CC_v3_1_R5" imports "../technical_report/technical_report" "CC_terminology" begin +(*>*) + +section \General Infrastructure on CC Evaluations\ + +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 \Security target ontology\ -doc_class st_ref_cls = text_element + - title :: string - st_version:: "(int \ int \ int)" - "authors":: "author list" - "st_date" :: string +doc_class st_ref_cls = CC_text_element + + title :: string + st_version:: "(int \ int \ 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 \ int \ 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:: + "\ X::toe_ovrw_cls . + (case eval_level X of + EAL1 \ software_req X \ [] + | EAL2 \ software_req X \ [] + | EAL3 \ software_req X \ [] + | EAL4 \ software_req X \ [] + | _ \ 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 "(\st_ref_cls\\<^sup>+ ~~ \toe_ref_cls\\<^sup>+ ~~ \toe_ovrw_cls\\<^sup>+ ~~ \toe_desc_cls\\<^sup>+)" +doc_class ST_INTRO_MNT = CC_structure_element + + tag_id:: string + accepts "\st_ref_cls\\<^sup>* ~~ \toe_ref_cls\\<^sup>* ~~ \toe_ovrw_cls\\<^sup>* ~~ \toe_desc_cls\\<^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 "(\cc_conf_claim_cls\\<^sup>+ ~~ \pp_clms_cls\\<^sup>* ~~ \pckg_claim_cls\\<^sup>+ ~~ \conf_ratio\\<^sup>*)" +doc_class CONF_CLAIMS_MNT = CC_structure_element + + tag_id:: string + accepts "(\cc_conf_claim_cls\\<^sup>+ ~~ \pp_clms_cls\\<^sup>* ~~ \pckg_claim_cls\\<^sup>+ ~~ \conf_ratio\\<^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 "((\threats_cls\\<^sup>+ || \osps_cls\\<^sup>+) ~~ \assumptions_cls\\<^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 \ toe_sec_obj_cls) list) option" @@ -103,44 +128,45 @@ doc_class sec_obj_ratio = env_thrts_obj_trace::"((threats_cls \ toe_sec_obj_cls) list) option" env_osps_obj_trace::"((osps_cls \ toe_sec_obj_cls) list) option" env_assms_obj_trace::"((assumptions_cls \ 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 "(\toe_sec_obj_cls\\<^sup>+ ~~ \env_sec_obj_cls\\<^sup>+ ~~ \sec_obj_ratio\\<^sup>*~~ \ext_comp_def\\<^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 \ 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 "(\sfrs_cls\\<^sup>+ ~~ \sfrs_ratio_cls\\<^sup>+ ~~ \sars_cls\\<^sup>+ ~~ \sars_ratio_cls\\<^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 ~~ diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index b104ea7..e4096a6 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -177,11 +177,12 @@ val _ = ) \ -textN\ \<^doof> \<^LATEX> \ +textN\ \<^doof> \<^LATEX> \ (* the same effect is achieved with : *) -setup \DOF_lib.define_shortcut ("bla",\<^here>) "\\bla"\ - +setup \DOF_lib.define_shortcut ("bla",\<^here>) "\\blabla"\ +(* Note that this assumes that the generated LaTeX macro "blabla" is defined somewhere in the + target document, for example, in the tex prelude. *) end