From 73e3cb1098f4f21cf8653c0eaeb018101549056f Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 19 Feb 2023 20:57:06 +0000 Subject: [PATCH 1/3] Marked session as AFP candidate. --- Isabelle_DOF/ROOT | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Isabelle_DOF/ROOT b/Isabelle_DOF/ROOT index aa393d9..78b759a 100644 --- a/Isabelle_DOF/ROOT +++ b/Isabelle_DOF/ROOT @@ -1,4 +1,4 @@ -session "Isabelle_DOF" = "Functional-Automata" + +session "Isabelle_DOF" (AFP) = "Functional-Automata" + options [document = pdf, document_output = "output", document_build = dof] sessions "Regular-Sets" From 00eff9f819e3d595e1a46baa41330efa58816f61 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 19 Feb 2023 22:15:37 +0000 Subject: [PATCH 2/3] Initial document setup. --- .../CC_v3_1_R5/CC_terminology.thy | 83 ++++++++++--------- .../CC_v3_1_R5/CC_v3_1_R5.thy | 3 +- .../Conceptual/Conceptual.thy | 5 +- Isabelle_DOF-Ontologies/ROOT | 5 +- Isabelle_DOF-Ontologies/document/.empty | 0 Isabelle_DOF-Ontologies/document_setup.thy | 11 +++ .../small_math/small_math.thy | 6 +- 7 files changed, 67 insertions(+), 46 deletions(-) create mode 100644 Isabelle_DOF-Ontologies/document/.empty create mode 100644 Isabelle_DOF-Ontologies/document_setup.thy diff --git a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy index 3a1c478..ffa8e6b 100644 --- a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy +++ b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy @@ -15,10 +15,12 @@ chapter\Common Criteria Definitions\ (*<<*) theory CC_terminology -imports "Isabelle_DOF.technical_report" +imports +"document_setup" +"Isabelle_DOF.technical_report" begin - +(*>>*) text\We re-use the class @\typ math_content\, which provides also a framework for semi-formal terminology, which we re-use by this definition.\ @@ -35,7 +37,6 @@ type_synonym concept = concept_definition declare[[ Definition_default_class="concept_definition"]] -(*>>*) section \Terminology\ @@ -45,10 +46,10 @@ subsection \Terms and definitions common in the CC\ Definition* [aas_def, tag= "''adverse actions''"] \actions performed by a threat agent on an asset\ -declare_reference*[toe_def] +declare_reference*[toeDef] Definition* [assts_def, tag="''assets''"] - \entities that the owner of the @{docitem toe_def} presumably places value upon \ + \entities that the owner of the @{docitem toeDef} presumably places value upon \ Definition* [asgn_def, tag="''assignment''"] \the specification of an identified parameter in a component (of the CC) or requirement.\ @@ -56,7 +57,7 @@ Definition* [asgn_def, tag="''assignment''"] declare_reference*[sfrs_def] Definition* [assrc_def, tag="''assurance''"] - \grounds for confidence that a @{docitem toe_def} meets the @{docitem sfrs_def}\ + \grounds for confidence that a @{docitem toeDef} meets the @{docitem sfrs_def}\ Definition* [attptl_def, tag="''attack potential''"] \measure of the effort to be expended in attacking a TOE, expressed in terms of @@ -69,9 +70,9 @@ Definition* [authdata_def, tag="''authentication data''"] \information used to verify the claimed identity of a user\ Definition* [authusr_def, tag = "''authorised user''"] -\@{docitem toe_def} user who may, in accordance with the @{docitem sfrs_def}, perform an operation\ +\@{docitem toeDef} user who may, in accordance with the @{docitem sfrs_def}, perform an operation\ -Definition* [bpp_def, tag="''Base Protection Profile''"] +Definition* [bppDef, tag="''Base Protection Profile''"] \Protection Profile used as a basis to build a Protection Profile Configuration\ Definition* [cls_def,tag="''class''"] @@ -104,8 +105,8 @@ Definition* [cfrm_def,tag="''confirm''"] term is only applied to evaluator actions.\ Definition* [cnnctvty_def, tag="''connectivity''"] -\property of the @{docitem toe_def} allowing interaction with IT entities external to the - @{docitem toe_def} +\property of the @{docitem toeDef} allowing interaction with IT entities external to the + @{docitem toeDef} This includes exchange of data by wire or by wireless means, over any distance in any environment or configuration.\ @@ -118,17 +119,17 @@ Definition* [cnt_vrb_def, tag="''counter, verb''"] \meet an attack where the impact of a particular threat is mitigated but not necessarily eradicated\ -declare_reference*[st_def] -declare_reference*[pp_def] +declare_reference*[stDef] +declare_reference*[ppDef] Definition* [dmnst_conf_def, tag="''demonstrable conformance''"] -\relation between an @{docitem st_def} and a @{docitem pp_def}, where the @{docitem st_def} +\relation between an @{docitem stDef} and a @{docitem ppDef}, where the @{docitem stDef} provides a solution which solves the generic security problem in the PP -The @{docitem pp_def} and the @{docitem st_def} may contain entirely different statements that discuss +The @{docitem ppDef} and the @{docitem stDef} may contain entirely different statements that discuss different entities, use different concepts etc. Demonstrable conformance is -also suitable for a @{docitem toe_def} type where several similar @{docitem pp_def}s already exist, thus -allowing the ST author to claim conformance to these @{docitem pp_def}s simultaneously, +also suitable for a @{docitem toeDef} type where several similar @{docitem ppDef}s already exist, thus +allowing the ST author to claim conformance to these @{docitem ppDef}s simultaneously, thereby saving work.\ Definition* [dmstrt_def, tag="''demonstrate''"] @@ -136,9 +137,9 @@ Definition* [dmstrt_def, tag="''demonstrate''"] Definition* [dpndcy, tag="''dependency''"] \relationship between components such that if a requirement based on the depending - component is included in a @{docitem pp_def}, ST or package, a requirement based on - the component that is depended upon must normally also be included in the @{docitem pp_def}, - @{docitem st_def} or package\ + component is included in a @{docitem ppDef}, ST or package, a requirement based on + the component that is depended upon must normally also be included in the @{docitem ppDef}, + @{docitem stDef} or package\ Definition* [dscrb_def, tag="''describe''"] \provide specific details of an entity\ @@ -153,7 +154,7 @@ Definition* [dtrmn_def, tag="''determine''"] performed which needs to be reviewed\ Definition* [devenv_def, tag="''development environment''"] -\environment in which the @{docitem toe_def} is developed\ +\environment in which the @{docitem toeDef} is developed\ Definition* [elmnt_def, tag="''element''"] \indivisible statement of a security need\ @@ -165,7 +166,7 @@ Definition* [ensr_def, tag="''ensure''"] consequence is not fully certain, on the basis of that action alone.\ Definition* [eval_def, tag="''evaluation''"] -\assessment of a @{docitem pp_def}, an @{docitem st_def} or a @{docitem toe_def}, +\assessment of a @{docitem ppDef}, an @{docitem stDef} or a @{docitem toeDef}, against defined criteria.\ Definition* [eal_def, tag= "''evaluation assurance level''"] @@ -181,11 +182,11 @@ Definition* [eval_schm_def, tag="''evaluation scheme''"] \administrative and regulatory framework under which the CC is applied by an evaluation authority within a specific community\ -Definition* [exst_def, tag="''exhaustive''"] +Definition* [exstDef, tag="''exhaustive''"] \characteristic of a methodical approach taken to perform an analysis or activity according to an unambiguous plan This term is used in the CC with respect to conducting an analysis or other -activity. It is related to “systematic” but is considerably stronger, in that it +activity. It is related to ``systematic'' but is considerably stronger, in that it indicates not only that a methodical approach has been taken to perform the analysis or activity according to an unambiguous plan, but that the plan that was followed is sufficient to ensure that all possible avenues have been @@ -236,7 +237,7 @@ Definition* [intl_com_chan_def, tag ="''internal communication channel''"] Definition* [int_toe_trans, tag="''internal TOE transfer''"] \communicating data between separated parts of the TOE\ -Definition* [inter_consist_def, tag="''internally consistent''"] +Definition* [inter_consistDef, tag="''internally consistent''"] \no apparent contradictions exist between any aspects of an entity In terms of documentation, this means that there can be no statements within @@ -271,7 +272,7 @@ Definition* [org_sec_po_def, tag="''organisational security policy''"] Definition* [pckg_def, tag="''package''"] \named set of either security functional or security assurance requirements - An example of a package is “EAL 3”.\ + An example of a package is ``EAL 3''.\ Definition* [pp_config_def, tag="''Protection Profile Configuration''"] \Protection Profile composed of Base Protection Profiles and Protection Profile Module\ @@ -279,7 +280,7 @@ Definition* [pp_config_def, tag="''Protection Profile Configuration''"] Definition* [pp_eval_def, tag="''Protection Profile evaluation''"] \ assessment of a PP against defined criteria \ -Definition* [pp_def, tag="''Protection Profile''"] +Definition* [ppDef, tag="''Protection Profile''"] \implementation-independent statement of security needs for a TOE type\ Definition* [ppm_def, tag="''Protection Profile Module''"] @@ -299,7 +300,7 @@ Definition* [ref_def, tag="''refinement''"] Definition* [role_def, tag="''role''"] \predefined set of rules establishing the allowed interactions between - a user and the @{docitem toe_def}\ + a user and the @{docitem toeDef}\ declare_reference*[sfp_def] @@ -309,7 +310,7 @@ Definition* [scrt_def, tag="''secret''"] declare_reference*[sfr_def] -Definition* [sec_st_def, tag="''secure state''"] +Definition* [sec_stDef, tag="''secure state''"] \state in which the @{docitem tsf_def} data are consistent and the @{docitem tsf_def} continues correct enforcement of the @{docitem sfr_def}s\ @@ -329,18 +330,20 @@ Definition* [sec_obj_def, tag="''security objective''"] Definition* [sec_prob_def, tag ="''security problem''"] \statement which in a formal manner defines the nature and scope of the security that the TOE is intended to address This statement consists of a combination of: - \begin{itemize} - \item threats to be countered by the TOE and its operational environment, - \item the OSPs enforced by the TOE and its operational environment, and - \item the assumptions that are upheld for the operational environment of the TOE. - \end{itemize}\ +\begin{itemize} +\item threats to be countered by the TOE and its operational environment, +\item the OSPs enforced by the TOE and its operational environment, and +\item the assumptions that are upheld for the operational environment of the TOE. +\end{itemize}\ Definition* [sr_def, 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, tag="''Security Target''", short_tag="Some(''ST'')"] -\implementation-dependent statement of security needs for a specific i\
dentified @{docitem toe_def}\ +(*<*) +text \@{docitem toeDef}\ +(*>*) +Definition* [st, tag="''Security Target''", short_tag="Some(''ST'')"] +\implementation-dependent statement of security needs for a specific identified @{docitem toeDef}\ Definition* [slct_def, tag="''selection''"] \specification of one or more items from a list in a component\ @@ -386,7 +389,7 @@ Definition* [tr_vrb_def, tag="''trace, verb''"] \perform an informal correspondence analysis between two entities with only a minimal level of rigour\ -Definition* [trnsfs_out_toe_def, tag="''transfers outside of the TOE''"] +Definition* [trnsfs_out_toeDef, tag="''transfers outside of the TOE''"] \TSF mediated communication of data to entities not under the control of the TSF\ Definition* [transl_def, tag= "''translation''"] @@ -431,13 +434,13 @@ effort is required of the evaluator.\ Definition* [dev_def, tag="''Developer''"] \who respond to actual or perceived consumer security requirements in - constructing a @{docitem toe_def}, reference this CC_Part_3 + constructing a @{docitem toeDef}, reference this CC\_Part\_3 when interpreting statements of assurance requirements and determining assurance approaches of @{docitem toe}s.\ Definition*[evalu_def, tag="'' Evaluator''"] -\who use the assurance requirements defined in CC_Part_3 +\who use the assurance requirements defined in CC\_Part\_3 as mandatory statement of evaluation criteria when determining the assurance - of @{docitem toe_def}s and when evaluating @{docitem pp_def}s and @{docitem st_def}s.\ + of @{docitem toeDef}s and when evaluating @{docitem ppDef}s and @{docitem stDef}s.\ end diff --git a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy index 14e8176..35b64a9 100644 --- a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy +++ b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy @@ -12,7 +12,8 @@ (*<*) theory "CC_v3_1_R5" - imports "Isabelle_DOF.technical_report" + imports + "Isabelle_DOF.technical_report" "CC_terminology" diff --git a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy index 5f01f72..3263a99 100644 --- a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy +++ b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy @@ -16,6 +16,7 @@ section\A conceptual introduction into DOF and its features:\ theory Conceptual imports +"document_setup" "Isabelle_DOF.Isa_DOF" "Isabelle_DOF.Isa_COL" begin @@ -31,12 +32,12 @@ text\This class definition leads an implicit Isabelle/HOL \<^theory_text> (cf. \<^url>\https://isabelle.in.tum.de/doc/isar-ref.pdf\, chapter 11.6.). Consequently, \<^theory_text>\doc_class\'es inherit the entire theory-infrastructure from Isabelle records: \<^enum> there is a HOL-type \<^typ>\A\ and its extensible version \<^typ>\'a A_scheme\ -\<^enum> there are HOL-terms representing \<^emph>\doc_class instances\ with the high-level syntax: +\<^enum> there are HOL-terms representing \<^emph>\doc\_class instances\ with the high-level syntax: \<^enum> \<^term>\undefined\level := Some (1::int), x := 5::int \ :: A\ (Note that this way to construct an instance is not necessarily computable \<^enum> \<^term>\\tag_attribute = X, level = Y, x = Z\ :: A\ \<^enum> \<^term>\\tag_attribute = X, level = Y, x = Z, \ = M\ :: ('a A_scheme)\ -\<^enum> there is an entire proof infra-structure allowing to reason about \<^emph>\doc_class instances\; +\<^enum> there is an entire proof infra-structure allowing to reason about \<^emph>\doc\_class instances\; this involves the constructor, the selectors (representing the \<^emph>\attributes\ in OO lingo) the update functions, the rules to establish equality and, if possible the code generator setups: diff --git a/Isabelle_DOF-Ontologies/ROOT b/Isabelle_DOF-Ontologies/ROOT index 879f5ef..0bf46f3 100644 --- a/Isabelle_DOF-Ontologies/ROOT +++ b/Isabelle_DOF-Ontologies/ROOT @@ -1,11 +1,14 @@ session "Isabelle_DOF-Ontologies" = "Isabelle_DOF" + - options [document = false] + options [document = pdf, document_output = "output", document_build = dof] directories "CC_v3_1_R5" "Conceptual" "small_math" theories + "document_setup" "CC_v3_1_R5/CC_v3_1_R5" "CC_v3_1_R5/CC_terminology" "Conceptual/Conceptual" "small_math/small_math" + document_files + ".empty" diff --git a/Isabelle_DOF-Ontologies/document/.empty b/Isabelle_DOF-Ontologies/document/.empty new file mode 100644 index 0000000..e69de29 diff --git a/Isabelle_DOF-Ontologies/document_setup.thy b/Isabelle_DOF-Ontologies/document_setup.thy new file mode 100644 index 0000000..689192d --- /dev/null +++ b/Isabelle_DOF-Ontologies/document_setup.thy @@ -0,0 +1,11 @@ +(*<*) +theory "document_setup" + imports + "Isabelle_DOF.technical_report" +begin + +use_template "scrreprt-modern" +use_ontology "technical_report" + +end +(*>*) diff --git a/Isabelle_DOF-Ontologies/small_math/small_math.thy b/Isabelle_DOF-Ontologies/small_math/small_math.thy index 62e8367..639d633 100644 --- a/Isabelle_DOF-Ontologies/small_math/small_math.thy +++ b/Isabelle_DOF-Ontologies/small_math/small_math.thy @@ -14,7 +14,9 @@ section\An example ontology for a math paper\ theory small_math - imports "Isabelle_DOF.Isa_COL" + imports +"document_setup" +"Isabelle_DOF.Isa_COL" begin doc_class title = @@ -89,7 +91,7 @@ doc_class "conclusion" = text_section + establish :: "(contribution_claim \ result) set" text\ Besides subtyping, there is another relation between -doc_classes: a class can be a \<^emph>\monitor\ to other ones, +doc\_classes: a class can be a \<^emph>\monitor\ to other ones, which is expressed by occurrence in the where clause. While sub-classing refers to data-inheritance of attributes, a monitor captures structural constraints -- the order -- From 30eb47d80c63122e17a27aa6bbdb920158746c03 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 19 Feb 2023 22:26:18 +0000 Subject: [PATCH 3/3] Fixed section structure. --- Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy | 7 ++++--- Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy | 5 +++-- Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy | 8 ++++---- Isabelle_DOF-Ontologies/document_setup.thy | 5 +++++ Isabelle_DOF-Ontologies/small_math/small_math.thy | 2 +- 5 files changed, 17 insertions(+), 10 deletions(-) diff --git a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy index ffa8e6b..7d77b0d 100644 --- a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy +++ b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy @@ -10,7 +10,8 @@ * SPDX-License-Identifier: BSD-2-Clause *************************************************************************) -chapter\Common Criteria Definitions\ +chapter\Common Criteria\ +section\Terminology\ (*<<*) theory CC_terminology @@ -38,10 +39,10 @@ declare[[ Definition_default_class="concept_definition"]] -section \Terminology\ +subsection \Terminology\ -subsection \Terms and definitions common in the CC\ +subsubsection \Terms and definitions common in the CC\ Definition* [aas_def, tag= "''adverse actions''"] \actions performed by a threat agent on an asset\ diff --git a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy index 35b64a9..5cfd161 100644 --- a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy +++ b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy @@ -10,6 +10,7 @@ * SPDX-License-Identifier: BSD-2-Clause *************************************************************************) +section\CC 3.1.R5\ (*<*) theory "CC_v3_1_R5" imports @@ -20,7 +21,7 @@ theory "CC_v3_1_R5" begin (*>*) -section \General Infrastructure on CC Evaluations\ +subsection \General Infrastructure on CC Evaluations\ datatype EALs = EAL1 | EAL2 | EAL3 | EAL4 | EAL5 | EAL6 | EAL7 @@ -31,7 +32,7 @@ doc_class CC_structure_element =(* text_element + *) doc_class CC_text_element = text_element + eval_level :: EALs -section \Security target ontology\ +subsection \Security target ontology\ doc_class st_ref_cls = CC_text_element + diff --git a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy index 3263a99..b3b359d 100644 --- a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy +++ b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy @@ -11,7 +11,7 @@ * SPDX-License-Identifier: BSD-2-Clause *************************************************************************) -section\A conceptual introduction into DOF and its features:\ +chapter\A conceptual introduction into DOF and its features:\ theory Conceptual @@ -26,7 +26,7 @@ doc_class A = level :: "int option" x :: int -subsection\Excursion: On the semantic consequences of this definition: \ +section\Excursion: On the semantic consequences of this definition: \ text\This class definition leads an implicit Isabelle/HOL \<^theory_text>\record\ definition (cf. \<^url>\https://isabelle.in.tum.de/doc/isar-ref.pdf\, chapter 11.6.). @@ -77,7 +77,7 @@ A_make zero (SOME one) (add one one) \ -subsection\An independent class-tree root: \ +section\An independent class-tree root: \ doc_class B = @@ -90,7 +90,7 @@ text\We may even use type-synonyms for class synonyms ...\ type_synonym XX = B -subsection\Examples of inheritance \ +section\Examples of inheritance \ doc_class C = XX + z :: "A option" <= None (* A LINK, i.e. an attribute that has a type diff --git a/Isabelle_DOF-Ontologies/document_setup.thy b/Isabelle_DOF-Ontologies/document_setup.thy index 689192d..0c5867a 100644 --- a/Isabelle_DOF-Ontologies/document_setup.thy +++ b/Isabelle_DOF-Ontologies/document_setup.thy @@ -6,6 +6,11 @@ begin use_template "scrreprt-modern" use_ontology "technical_report" +(*>*) +title*[title::title] \Isabelle/DOF\ +subtitle*[subtitle::subtitle]\Ontologies\ + +(*<*) end (*>*) diff --git a/Isabelle_DOF-Ontologies/small_math/small_math.thy b/Isabelle_DOF-Ontologies/small_math/small_math.thy index 639d633..334aa4c 100644 --- a/Isabelle_DOF-Ontologies/small_math/small_math.thy +++ b/Isabelle_DOF-Ontologies/small_math/small_math.thy @@ -11,7 +11,7 @@ * SPDX-License-Identifier: BSD-2-Clause *************************************************************************) -section\An example ontology for a math paper\ +chapter\An example ontology for a math paper\ theory small_math imports