Merge branch 'main' into test-rebase2

All terms and definition are now in CC_terms

src/ROOT

@@ -11,6 +11,7 @@ session "Isabelle_DOF" = "Functional-Automata" +
     "ontologies/small_math"
     "ontologies/technical_report"
     "ontologies/CC_v3_1_R5"
+    "ontologies/CC_2022_R1"
   theories
     "DOF/Isa_DOF"
     "ontologies/ontologies"

src/ontologies/CC_2022_R1/Common_Criteria.thy

@@ -0,0 +1,235 @@
+chapter \<open>An Outline of a CENELEC Ontology\<close>
+
+text\<open> NOTE: An Ontology-Model of a certification standard such as CENELEC or Common Criteria 
+identifies:
+- notions (conceptual \<^emph>\<open>categories\<close>) having \<^emph>\<open>instances\<close>
+  (similar to classes and objects),
+- their \<^emph>\<open>subtype\<close> relation (eg., a "SRAC" is an "assumption"),
+- their syntactical structure 
+  (for the moment: defined by regular expressions describing the
+   order of category instances in the overall document as a regular language)
+ \<close> 
+
+(*<<*)  
+theory Common_Criteria
+  imports  "Isabelle_DOF.Common_Criteria_Terms"
+begin
+
+define_shortcut* csp      \<rightleftharpoons> \<open>CSP\<close>
+                 holcsp   \<rightleftharpoons> \<open>HOL-CSP\<close>
+                 hol      \<rightleftharpoons> \<open>HOL\<close>
+                 isabelle \<rightleftharpoons> \<open>Isabelle/HOL\<close>
+
+
+datatype cc_spec =
+      package             
+    | PP                  
+    | PP_module           
+    | PP_configuration    
+    | ST                  
+    | PP_PP_configuration 
+
+datatype cc_spec_chapter =
+      Introduction
+    | Conformance
+    | SPD \<comment> \<open>Security problem definition  \<^cc_term>\<open>SPD\<close>\<close>
+    | SO  \<comment> \<open>Security objectives  \<^cc_term>\<open>SO\<close>\<close>
+    | ECD \<comment> \<open>Extended components definition\<close>
+    | SR  \<comment> \<open>Security requirements  \<^cc_term>\<open>SR\<close>\<close>
+
+datatype cc_spec_section =
+      PP_reference
+    | PP_overview
+    | Threats
+    | Assumptions
+    | OSPs          \<comment> \<open>organizational security policies\<close>
+    | SO_for_TOE    \<comment> \<open>security objectives for the TOE\<close>
+    | SO_for_OE     \<comment> \<open>security objectives for the operational environment\<close>
+    | SOR           \<comment> \<open>security objectives rationale\<close>
+    | SFRs          \<comment> \<open>security functional requirements\<close>
+    | SARs          \<comment> \<open>security assurance requirements\<close>
+
+doc_class cc_spec_report = text_element +
+    cc_spec         ::    "cc_spec"
+    cc_definition   ::    "cc_term option" <= "None"
+
+doc_class PP_report = cc_spec_report +
+    cc_spec           ::    "cc_spec" <= "PP"
+    level             ::    "int option"
+    invariant PP_spec ::    \<open>cc_spec \<sigma> = PP\<close>
+
+(* Declaration of the superclass of each chapter of the specification of PP*)
+doc_class PP_introduction_report = PP_report +
+    cc_spec_chapter   ::    "cc_spec_chapter" <= "Introduction"
+    invariant introduction_chapter ::  \<open>cc_spec_chapter \<sigma> = Introduction\<close>
+
+doc_class PP_introduction_title = PP_introduction_report +
+    level             ::    "int option" <= "Some 1"
+
+doc_class PP_conformance_report = PP_report +
+    cc_spec_chapter     ::    "cc_spec_chapter" <= "Conformance"
+    invariant conformance_chapter ::  \<open>cc_spec_chapter \<sigma> = Conformance\<close>
+
+doc_class PP_conformance_title = PP_conformance_report +
+    level             ::    "int option" <= "Some 1"
+
+doc_class PP_SPD_report = PP_report +
+    cc_spec_chapter       ::    "cc_spec_chapter" <= "SPD"
+    invariant SPD_chapter ::  \<open>cc_spec_chapter \<sigma> = SPD\<close>
+
+doc_class PP_SPD_title = PP_SPD_report +
+    level             ::    "int option" <= "Some 1"
+
+doc_class PP_SO_report = PP_report +
+    cc_spec_chapter       ::    "cc_spec_chapter" <= "SO"
+    invariant SO_chapter  ::  \<open>cc_spec_chapter \<sigma> = SO\<close>
+
+doc_class PP_SO_title = PP_SO_report +
+    level             ::    "int option" <= "Some 1"
+
+doc_class PP_ECD_report = PP_report +
+    cc_spec_chapter       ::    "cc_spec_chapter" <= "ECD"
+    invariant ECD_chapter ::  \<open>cc_spec_chapter \<sigma> = ECD\<close>
+
+doc_class PP_ECD_title = PP_ECD_report +
+    level             ::    "int option" <= "Some 1"
+
+doc_class PP_SR_report = PP_report +
+cc_spec_chapter       ::    "cc_spec_chapter" <= "SR"
+    invariant SR_chapter  ::  \<open>cc_spec_chapter \<sigma> = SR\<close>
+
+doc_class PP_SR_title = PP_SR_report +
+    level             ::    "int option" <= "Some 1"
+
+(* Declaration of the sections in the PP introduction *)
+doc_class PP_introduction = PP_introduction_title +
+    level             ::    "int option" <= "Some 0"
+
+doc_class PP_reference = PP_introduction_title +
+    cc_spec_section   ::    "cc_spec_section" <= "PP_reference"
+    cc_title             ::    "title"
+    version           ::    "string" <= "''''"
+    sponsors          ::    "string list" <= "[]"
+    publication_date  ::    "string" <= "''''"
+    invariant null_title    ::    \<open>short_title (cc_title \<sigma>) \<noteq> None\<close> 
+    invariant null_version  ::    \<open>version \<sigma> \<noteq> ''''\<close>
+    invariant null_sponsors ::    \<open>sponsors \<sigma> \<noteq> []\<close>
+    invariant null_date     ::    \<open>publication_date \<sigma> \<noteq> ''''\<close>
+
+term\<open>scholarly_paper.short_title (cc_title a) \<noteq> None \<and> 
+     the(scholarly_paper.short_title (cc_title a)) \<noteq> ''''\<close>
+
+doc_class PP_overview = PP_introduction_title +
+    cc_spec_section   ::    "cc_spec_section" <= "PP_overview"
+
+(* Declaration of the sections in the conformance *)
+
+doc_class Conformance = PP_conformance_title +
+    level             ::    "int option" <= "Some 0"
+
+(* Declaration of the sections in the security problem definition *)
+
+doc_class SPD = PP_SPD_title +
+    cc_definition     ::    "cc_term option" <= "Some @{cc-term \<open>SPD\<close>}"
+    level             ::    "int option" <= "Some 0"
+
+doc_class Threats = PP_SPD_title +
+    cc_spec_section   ::    "cc_spec_section" <= "Threats"
+
+doc_class Assumptions = PP_SPD_title +
+    cc_spec_section   ::    "cc_spec_section" <= "Assumptions"
+
+doc_class OSPs = PP_SPD_title +
+    cc_spec_section   ::    "cc_spec_section" <= "OSPs"
+    type_synonym organizational_security_policies = OSPs
+
+(* Declaration of the sections in the security objectives *)
+
+doc_class SO = PP_SO_title +
+    level             ::    "int option" <= "Some 0"
+
+doc_class SO_for_TOE = PP_SO_title +
+    cc_spec_section   ::    "cc_spec_section" <= "SO_for_TOE"
+    type_synonym security_objectives_for_the_TOE = SO_for_TOE
+
+doc_class SO_for_OE = PP_SO_title +
+    cc_spec_section   ::    "cc_spec_section" <= "SO_for_OE"
+    type_synonym security_objectives_for_the_operational_environment = SO_for_TOE
+
+doc_class SOR = PP_SO_title +
+    cc_spec_section   ::    "cc_spec_section" <= "SOR"
+    type_synonym security_objectives_rationale = SOR
+
+(* Declaration of the sections in the extended components definition *)
+
+doc_class ECD = PP_ECD_title +
+    level             ::    "int option" <= "Some 0"
+
+doc_class ECD_section = PP_ECD_title +
+    level             ::    "int option" <= "Some 1"
+    type_synonym extended_component_definition = ECD_section
+
+(* Declaration of the sections in the Security requirements *)
+
+doc_class SR = PP_SR_title +
+    level             ::    "int option" <= "Some 0"
+
+doc_class SFR = PP_SR_title +
+    cc_spec_section   ::    "cc_spec_section" <= "SFRs"
+
+doc_class SAR = PP_SR_title +
+    cc_spec_section   ::    "cc_spec_section" <= "SARs"
+
+(* Declaration of the monitor of each chapter of the PP specification *)
+
+doc_class PP_introduction_monitor = 
+    cc_spec         ::    "cc_spec" <= "PP"
+    accepts "PP_introduction  ~~ PP_reference ~~ PP_overview"
+
+doc_class Conformance_monitor = 
+    cc_spec         ::    "cc_spec" <= "PP"
+    accepts "Conformance ~~ \<lbrace>PP_conformance_report\<rbrace>\<^sup>*"
+
+doc_class SPD_monitor = 
+    cc_spec         ::    "cc_spec" <= "PP"
+    accepts "Threats ~~ Assumptions ~~ \<lbrakk>OSPs\<rbrakk>"
+
+doc_class SO_monitor = 
+    cc_spec         ::    "cc_spec" <= "PP"
+    accepts "SO_for_TOE ~~ SO_for_OE ~~ \<lbrakk>SOR\<rbrakk>"
+
+doc_class ECD_monitor = 
+    cc_spec         ::    "cc_spec" <= "PP"
+    accepts "ECD ~~ \<lbrace>PP_ECD_report\<rbrace>\<^sup>+"
+
+doc_class SR_monitor = 
+    cc_spec         ::    "cc_spec" <= "PP"
+    accepts "SR ~~ \<lbrace>SFR\<rbrace>\<^sup>+ ~~ \<lbrace>SAR\<rbrace>\<^sup>+"
+
+doc_class Appendix = cc_spec_report +
+    level             ::    "int option" <= "Some 0"
+    letter          ::    "char"
+
+doc_class Annex = cc_spec_report +
+    level             ::    "int option" <= "Some 0"
+    letter          ::    "char"
+
+(* Declaration of the monitor of the whole PP specification *)
+doc_class monitor_cc_spec =
+    cc_spec         ::    "cc_spec"
+
+doc_class monitor_PP_spec =
+    cc_spec         ::    "cc_spec" <= "PP"
+    accepts "title ~~ PP_introduction_monitor ~~ Conformance_monitor ~~ 
+             SPD_monitor ~~ SO_monitor ~~ \<lbrakk>ECD_monitor\<rbrakk> ~~ SR_monitor ~~ \<lbrace>Appendix\<rbrace>\<^sup>*"
+    
+
+doc_class monitor_PP_control =
+    cc_spec         ::    "cc_spec" <= "PP"
+    rejects text_element
+    accepts "\<lbrace>PP_report\<rbrace>\<^sup>*"
+
+(* Put cc_term option in attribut
+   
+*)
+end

src/ontologies/CC_2022_R1/Common_Criteria_Terms.thy

@@ -0,0 +1,460 @@
+theory Common_Criteria_Terms
+  imports  "Isabelle_DOF.technical_report"
+begin
+
+text\<open>We re-use the class \<^typ>\<open>math_content\<close>, which provides also a framework for
+semi-formal "math-alike" terminology, which we re-use by this definition.\<close>
+
+doc_class semi_formal_content = math_content +
+      status        :: status <= "semiformal" 
+      mcc           :: math_content_class 
+
+
+
+type_synonym sfc = semi_formal_content  
+
+doc_class cc_term = semi_formal_content + 
+      mcc          :: math_content_class <= "terminology"
+      level        :: "int option" <= "Some 1"
+
+type_synonym common_criteria_term = cc_term 
+
+text\<open> in the following, all \<^theory_text>\<open>Definition*\<close> statements are interpreted as 
+     \<^doc_class>\<open>cc_term\<close>s, i.e. semi-formal teminological definitions.\<close>
+
+declare[[ Definition_default_class="cc_term"]]
+
+
+text\<open> Excerpt of the BE EN 50128:2011, page 22. \<close>
+
+section\<open>Terms and Definitions\<close>
+
+declare_reference*[evaluator::cc_term]
+declare_reference*[developer::cc_term]
+Definition*[action]
+\<open>documented activity of the @{cc_term (unchecked) \<open>evaluator\<close>}
+ or  @{cc_term (unchecked) \<open>developer\<close>}\<close>
+
+declare_reference*[entity::cc_term]
+declare_reference*[TSF::cc_term]
+Definition*[admministrator]
+\<open> @{cc_term (unchecked) \<open>entity\<close>} that has a level of trust with respect to 
+all policies implemented by the  @{cc_term (unchecked) \<open>TSF\<close>}\<close>
+
+Definition*[API, short_name="''application programming interface''"]
+\<open>\<close>
+
+declare_reference*[threat_agent::cc_term]
+declare_reference*[asset::cc_term]
+Definition*[adverse_action]
+\<open> \<^cc_term>\<open>action\<close> performed by a @{cc_term (unchecked) \<open>threat_agent\<close>} 
+on an @{cc_term (unchecked) \<open>asset\<close>}\<close>
+
+declare_reference*[TOE::cc_term]
+Definition*[asset]
+\<open>  @{cc_term (unchecked) \<open>entity\<close>}  that the owner of 
+the  @{cc_term (unchecked) \<open>TOE\<close>} presumably places value on\<close>
+
+Definition*[assignement]
+\<open>specification of an identified parameter in a functional or assurance component\<close>
+
+declare_reference*[SFR::cc_term]
+Definition*[assurance]
+\<open>grounds for confidence that a @{cc_term (unchecked) \<open>TOE\<close>} meets
+the security functional requirements @{cc_term (unchecked) \<open>SFR\<close>}s \<close>
+
+declare_reference*[SAR::cc_term]
+Definition*[AP, short_name="''assurance package''"]
+\<open>named set of  @{cc_term (unchecked) \<open>SAR\<close>}s\<close>
+
+Definition*[attack_potential]
+\<open>measure of the effort needed to exploit a vulnerability in a @{cc_term (unchecked) \<open>TOE\<close>} \<close>
+
+Definition*[attack_surface]
+\<open>set of logical or physical interfaces to a target, consisting of points
+ through which access to the target and its functions may be attempted\<close>
+
+Definition*[augmentation]
+\<open>addition of one or more requirements to a package\<close>
+
+Definition*[autorized_user]
+\<open> @{cc_term (unchecked) \<open>entity\<close>} who may, in accordance with the @{cc_term (unchecked) \<open>SFR\<close>}s,
+ perform an operation on the  @{cc_term (unchecked) \<open>TOE\<close>}\<close>
+
+declare_reference*[independent_entity::cc_term]
+declare_reference*[dependent_component::cc_term]
+Definition*[base_component]
+\<open> @{cc_term (unchecked) \<open>independent_entity\<close>} in a multi-component product that provides
+ services and resources to one or more  @{cc_term (unchecked) \<open>dependent_component\<close>}(s)\<close>
+
+declare_reference*[PP::cc_term]
+declare_reference*[PP_module::cc_term]
+declare_reference*[PP_module_base::cc_term]
+declare_reference*[PP_config::cc_term]
+Definition*[base_PP, short_name="''base Protection Profile''"]
+\<open> @{cc_term (unchecked) \<open>PP\<close>} specified in a  @{cc_term (unchecked) \<open>PP_module\<close>}, 
+as part of that @{cc_term (unchecked) \<open>PP_module\<close>}’s @{cc_term (unchecked) \<open>PP_module_base\<close>},
+used as a basis to build a @{cc_term (unchecked) \<open>PP_config\<close>}\<close>
+
+Definition*[base_PP_module, short_name="''base PP-Module''"]
+\<open>@{cc_term (unchecked) \<open>PP_module\<close>} specified in a different @{cc_term (unchecked) \<open>PP_module\<close>}, 
+as part of that @{cc_term (unchecked) \<open>PP_module\<close>}’s  @{cc_term (unchecked) \<open>PP_module_base\<close>}, 
+used as a basis to build a @{cc_term (unchecked) \<open>PP_config\<close>}\<close>
+
+Definition*[base_TOE, short_name="''base target of evaluation''"]
+\<open>@{cc_term (unchecked) \<open>base_component\<close>} which is itself the subject of an evaluation\<close>
+
+Definition*[class_cc, short_name="''class''"]
+\<open>〈taxonomy〉 set of families that share a common focus\<close>
+
+Definition*[CD, short_name="''compact disk''"]
+\<open>\<close>
+
+Definition*[component]
+\<open>〈taxonomy〉 smallest selectable set of elements on which requirements may be based OU
+  <composition> @{cc_term (unchecked) \<open>entity\<close>} which provides resources and services in a product\<close>
+
+declare_reference*[composed_TOE::cc_term]
+Definition*[component_TOE, short_name="''component target of evaluation''"]
+\<open>(evaluated) @{cc_term (unchecked) \<open>TOE\<close>}
+ that is a component of another @{cc_term (unchecked) \<open>composed_TOE\<close>}\<close>
+
+Definition*[CAP, short_name="''composition assurance package''"]
+\<open> \<^cc_term>\<open>AP\<close> consisting of components drawn predominately from the ACO \<^cc_term>\<open>class_cc\<close>,
+ representing a point on the pre-defined scale for composition assurance\<close>
+
+Definition*[composed_TOE, short_name="''composed target of evaluation''"]
+\<open>@{cc_term (unchecked) \<open>TOE\<close>} comprising solely two or more separately identified components
+ with a security relationship between their @{cc_term (unchecked) \<open>TSF\<close>}\<close>
+
+Definition*[composed_evaluation, short_name="''composed evaluation''"]
+\<open>evaluation of a \<^cc_term>\<open>composed_TOE\<close> using the specific evaluation technique applicable to \<^cc_term>\<open>composed_TOE\<close>s\<close>
+
+declare_reference*[composite_product::cc_term]
+declare_reference*[composite_TOE::cc_term]
+Definition*[composite_evaluation, short_name="''composite evaluation''"]
+\<open>evaluation of a @{cc_term (unchecked) \<open>composite_TOE\<close>}/@{cc_term (unchecked) \<open>composite_product\<close>}
+ using the specific composite evaluation technique\<close>
+
+Definition*[composite_product, short_name="''composite product''"]
+\<open>product comprised of two or more components which can be organized in two layers:
+ a layer of one already evaluated \<^cc_term>\<open>base_component\<close> (\<^cc_term>\<open>base_TOE\<close>)
+ and a layer of one @{cc_term (unchecked) \<open>dependent_component\<close>}\<close>
+
+Definition*[COMP, short_name="''composite product assurance package''"]
+\<open>\<close>
+
+Definition*[composite_TOE, short_name="''composite target of evaluation''"]
+\<open>part of a \<^cc_term>\<open>composite_product\<close> including the \<^cc_term>\<open>base_TOE\<close>
+ and the @{cc_term (unchecked) \<open>dependent_component\<close>}\<close>
+
+Definition*[CM, short_name="''configuration management''"]
+\<open>discipline applying technical and administrative direction and surveillance to:
+ identify and document the functional and physical characteristics of a configuration item,
+ control changes to those characteristics, record and report change processing
+ and implementation status, and verify compliance with specified requirements\<close>
+
+Definition*[CMS, short_name="''configuration management system''"]
+\<open>set of procedures and tools (including their documentation) used by a @{cc_term (unchecked) \<open>developer\<close>}
+ to develop and maintain configurations of their products during their life-cycles\<close>
+
+Definition*[counter]
+\<open>act on or respond to a particular threat so that the threat is eradicated or mitigated\<close>
+
+declare_reference*[ST::cc_term]
+declare_reference*[PP_configuration::cc_term]
+Definition*[DC, short_name="''demonstrable conformance''"]
+\<open>relation between a @{cc_term (unchecked) \<open>PP\<close>}/@{cc_term (unchecked) \<open>ST\<close>} (PP/ST)
+ and a @{cc_term (unchecked) \<open>PP\<close>}, or an @{cc_term (unchecked) \<open>ST\<close>} and
+ a @{cc_term (unchecked) \<open>PP_configuration\<close>}, where the PP/ST provides an equivalent or
+ more restrictive solution that solves the generic security problem in the PP/PP-Configuration\<close>
+
+declare_reference*[FP::cc_term]
+Definition*[dependency]
+\<open>relationship between components such that a @{cc_term (unchecked) \<open>PP\<close>}, @{cc_term (unchecked) \<open>ST\<close>},
+ @{cc_term (unchecked) \<open>FP\<close>} or \<^cc_term>\<open>AP\<close>} including a component
+ also includes any other \<^cc_term>\<open>component\<close>s that are identified as being depended upon
+ or include a rationale as to why they are not\<close>
+
+declare_reference*[dependent_entity::cc_term]
+Definition*[dependent_component, short_name="''dependent component''"]
+\<open>@{cc_term (unchecked)\<open>dependent_entity\<close>} in a multi-component product that relies on
+ the provision of services and resources by one or more \<^cc_term>\<open>base_component\<close>s\<close>
+
+Definition*[dependent_TOE, short_name="''dependent target of evaluation''"]
+\<open>\<^cc_term>\<open>dependent_component\<close> which is itself the subject of an evaluation\<close>
+
+Definition*[developper]
+\<open>organization responsible for the development of the @{cc_term (unchecked)\<open>TOE\<close>}\<close>
+
+declare_reference*[SPD::cc_term]
+declare_reference*[SO::cc_term]
+declare_reference*[operational_environment::cc_term]
+Definition*[direct_rationale, short_name="''direct rationale''"]
+\<open>type of @{cc_term (unchecked)\<open>PP\<close>}, @{cc_term (unchecked)\<open>PP_module\<close>} or @{cc_term (unchecked)\<open>ST\<close>}
+ in which the @{cc_term (unchecked)\<open>SPD\<close>} elements are mapped directly to
+ the @{cc_term (unchecked)\<open>SFR\<close>}) and possibly to the @{cc_term (unchecked)\<open>SO\<close>}s
+ for the @{cc_term (unchecked)\<open>operational_environment\<close>}\<close>
+
+Definition*[DAC, short_name="''discretionary access control''"]
+\<open>\<close>
+
+Definition*[element]
+\<open>〈taxonomy〉 self-contained description of a security need assigned to @{cc_term (unchecked)\<open>SAR\<close>}
+ or @{cc_term (unchecked)\<open>SFR\<close>}\<close>
+
+Definition*[entity]
+\<open>identifiable item that is described by a set or collection of properties\<close>
+
+Definition*[evaluation]
+\<open>assessment of a @{cc_term (unchecked)\<open>PP_configuration\<close>}, @{cc_term (unchecked)\<open>PP\<close>},
+ a @{cc_term (unchecked)\<open>ST\<close>}, or a @{cc_term (unchecked)\<open>TOE\<close>}, against defined criteria
+\<close>
+
+Definition*[EA, short_name="''evaluation activity''"]
+\<open>activity derived from one or more work units\<close>
+
+Definition*[EAL, short_name="''evaluation assurance level''"]
+\<open>well-formed package of @{cc_term (unchecked)\<open>SAR\<close>} representing a point on the pre- defined assurance scale\<close>
+
+declare_reference*[evaluation_scheme::cc_term]
+Definition*[evaluation_authority, short_name="''evaluation authority''"]
+\<open>body operating an @{cc_term (unchecked)\<open>evaluation_scheme\<close>}\<close>
+
+Definition*[EM, short_name="''evaluation method''"]
+\<open>set of one or more \<^cc_term>\<open>EA\<close> for application in a specific context\<close>
+
+Definition*[evaluation_scheme, short_name="''evaluation scheme''"]
+\<open>rules, procedures and management to carrying evaluations of IT product security\<close>
+
+declare_reference*[overall_verdict::cc_term]
+Definition*[ETR, short_name="''evaluation technical report''"]
+\<open>documentation of the @{cc_term (unchecked)\<open>overall_verdict\<close>} and its justification, produced
+ by the @{cc_term (unchecked)\<open>evaluator\<close>}, and submitted to an \<^cc_term>\<open>evaluation_authority\<close>\<close>
+
+Definition*[ETR_COMP, short_name="''evaluation technical report for composite evaluation''"]
+\<open>documentation intended to be used within the \<^cc_term>\<open>composite_evaluation\<close> approach and derived
+ by the \<^cc_term>\<open>base_component\<close> @{cc_term (unchecked)\<open>evaluator\<close>} from the full \<^cc_term>\<open>ETR\<close> 
+for the evaluated \<^cc_term>\<open>base_component\<close>\<close>
+
+Definition*[evaluator]
+\<open>individual assigned to perform evaluations in accordance with a given evaluation standard and
+ associated evaluation methodology\<close>
+
+Definition*[EC, short_name="''exact conformance''"]
+\<open>hierarchical relationship between a @{cc_term (unchecked)\<open>PP\<close>} or @{cc_term (unchecked)\<open>PP_configuration\<close>}
+ and a @{cc_term (unchecked)\<open>ST\<close>} where all the requirements in the ST are drawn only from the PP/PP- Configuration\<close>
+
+Definition*[exploitable_vulnerability, short_name="''exploitable vulnerability''"]
+\<open>weakness in the @{cc_term (unchecked)\<open>TOE\<close>} that can be used to violate the @{cc_term (unchecked)\<open>SFR\<close>}s
+ in the @{cc_term (unchecked)\<open>operational_environment\<close>} for the  @{cc_term (unchecked)\<open>TOE\<close>}\<close>
+
+Definition*[extended_security_requirement, short_name="''extended security requirement''"]
+\<open>security requirement developed according to the rules in this document,
+ but which are not listed in any part of the CC\<close>
+
+Definition*[user, short_name="''external entity''"]
+\<open>human technical system or one of its components interacting with the @{cc_term (unchecked)\<open>TOE\<close>}
+ from outside of the TOE boundary\<close>
+
+Definition*[family]
+\<open>〈taxonomy〉 set of components that shares a similar goal but differs in emphasis or rigour\<close>
+
+Definition*[FP, short_name="''functional package''"]
+\<open>named set of @{cc_term (unchecked)\<open>SFR\<close>}s that may be accompanied by a @{cc_term (unchecked)\<open>SPD\<close>}
+ and @{cc_term (unchecked)\<open>SO\<close>}s derived from that SPD
+\<close>
+
+declare_reference*[multi_assurance_evaluation::cc_term]
+Definition*[global_AP, short_name="''global assurance package''"]
+\<open>\<^cc_term>\<open>AP\<close> that applies to the entire  @{cc_term (unchecked)\<open>TOE\<close>} in a
+  @{cc_term (unchecked)\<open>multi_assurance_evaluation\<close>}\<close>
+
+Definition*[guidance_documentation, short_name="''guidance documentation''"]
+\<open>documentation that describes the delivery, preparation, operation, management and/or use of the @{cc_term (unchecked)\<open>TOE\<close>}\<close>
+
+declare_reference*[refinement::cc_term]
+Definition*[implementation_representation, short_name="''implementation representation''"]
+\<open>least abstract representation of the @{cc_term (unchecked)\<open>TSF\<close>}, specifically the one
+ that is used to create the TSF itself without further design @{cc_term (unchecked)\<open>refinement\<close>}\<close>
+
+Definition*[internally_consistent, short_name="''internally consistent''"]
+\<open>no apparent contradictions exist between any aspects of an \<^cc_term>\<open>entity\<close>\<close>
+
+Definition*[interpretation_cc, short_name="''interpretation''"]
+\<open>clarification or amplification of a standard or an \<^cc_term>\<open>evaluation_scheme\<close> requirement\<close>
+
+Definition*[iteration]
+\<open>use of the same \<^cc_term>\<open>component\<close> to express two or more distinct requirements\<close>
+
+Definition*[layering]
+\<open>design technique where separate groups of components are hierarchically organized to have separate
+ responsibilities such that a group of components depends on groups of components below it in
+ the hierarchy for services, and provides its services to the groups of components above it\<close>
+
+Definition*[module_cc, short_name="''module''"]
+\<open>architectural unit specified at a level suitable for implementation of the unit\<close>
+
+Definition*[multi_assurance_evaluation, short_name="''multi-assurance evaluation''"]
+\<open>evaluation of a @{cc_term (unchecked)\<open>TOE\<close>} using a @{cc_term (unchecked)\<open>PP_configuration\<close>}
+ where each PP- Configuration component is associated with its own set of assurance requirements\<close>
+
+Definition*[object]
+\<open>\<^cc_term>\<open>entity\<close>in the @{cc_term (unchecked)\<open>TOE\<close>} that contains or receives information, and
+ upon which subjects perform operations\<close>
+
+Definition*[operation]
+\<open>〈on an \<^cc_term>\<open>object\<close>〉 specific type of \<^cc_term>\<open>action\<close> performed by a subject on an object
+\<close>
+
+Definition*[operational_environment, short_name="''operational environment''"]
+\<open>environment in which the @{cc_term (unchecked)\<open>TOE\<close>} is operated, consisting of everything
+ that is outside the TOE boundary\<close>
+
+Definition*[optional_SFR, short_name="''optional Security Functional Requirement''"]
+\<open>@{cc_term (unchecked)\<open>SFR\<close>} in a @{cc_term (unchecked)\<open>PP\<close>}, @{cc_term (unchecked)\<open>FP\<close>}, or
+ @{cc_term (unchecked)\<open>PP_module\<close>} that contributes to a stated aspect of the PP’s security problem
+ description but whose inclusion in a conformant PP’s or @{cc_term (unchecked)\<open>ST\<close>} list of
+ SFRs is not mandatory\<close>
+
+Definition*[OSP, short_name="''organizational security policy''"]
+\<open>set of security rules, procedures, or guidelines for an organization\<close>
+
+Definition*[overall_verdict, short_name="''overall verdict''"]
+\<open>statement issued by an \<^cc_term>\<open>evaluator\<close> with respect to the result of an \<^cc_term>\<open>evaluation\<close>\<close>
+
+Definition*[potential_vulnerability, short_name="''potential vulnerability''"]
+\<open>suspected, but not confirmed, weakness
+\<close>
+
+Definition*[PP, short_name="''Protection Profile''"]
+\<open>implementation-independent statement of security needs for a @{cc_term (unchecked)\<open>TOE\<close>} type\<close>
+
+Definition*[PP_configuration, short_name="''Protection Profile Configuration''"]
+\<open>implementation-independent statement of security needs for a @{cc_term (unchecked)\<open>TOE\<close>} type
+ containing at least one \<^cc_term>\<open>PP\<close> and an additional non-empty set of @{cc_term (unchecked)\<open>PP_module\<close>}
+ (with the associated PP-Modules Bases)\<close>
+
+Definition*[PP_configuration_component, short_name="''Protection Profile Configuration component''"]
+\<open>\<^cc_term>\<open>PP\<close> or @{cc_term (unchecked)\<open>PP_module\<close>} included in a \<^cc_term>\<open>PP_configuration\<close>\<close>
+
+Definition*[PP_module, short_name="''Protection Profile module''"]
+\<open>implementation-independent statement of security needs for a @{cc_term (unchecked)\<open>TOE\<close>} type
+ complementary to one or more base \<^cc_term>\<open>PP\<close> and possibly some \<^cc_term>\<open>base_PP_module\<close>\<close>
+
+Definition*[PP_module_base, short_name="''Protection Profile Module Base''"]
+\<open>set of either \<^cc_term>\<open>PP_module\<close> or \<^cc_term>\<open>PP\<close> or both, specified by a PP- Module as a basis
+ for building a \<^cc_term>\<open>PP_configuration\<close>\<close>
+
+Definition*[refinement]
+\<open>addition of details to a security component\<close>
+
+Definition*[residual_vulnerability, short_name="''residual vulnerability''"]
+\<open>weakness that cannot be exploited in the \<^cc_term>\<open>operational_environment\<close> for the
+ @{cc_term (unchecked)\<open>TOE\<close>}, but that can be used to violate the @{cc_term (unchecked)\<open>SFR\<close>}s by
+ an attacker with greater \<^cc_term>\<open>attack_potential\<close> than is anticipated in the operational
+ environment for the TOE\<close>
+
+Definition*[role]
+\<open>pre-defined set of rules establishing the allowed interactions between a user and the @{cc_term (unchecked)\<open>TOE\<close>}\<close>
+
+Definition*[SAR, short_name="''security assurance requirement''"]
+\<open>security requirement that refers to the conditions and processes for the development and delivery
+ of the @{cc_term (unchecked)\<open>TOE\<close>}, and the \<^cc_term>\<open>action\<close>s required of \<^cc_term>\<open>evaluator\<close>s
+ with respect to evidence produced from these conditions and processes
+\<close>
+
+Definition*[security_attribute, short_name="''security attribute''"]
+\<open>property of subjects, users, objects, information, sessions and/or resources that is used in
+ defining the @{cc_term (unchecked)\<open>SFR\<close>}s and whose values are used in enforcing the SFRs
+\<close>
+
+Definition*[SFR, short_name="''security functional requirement''"]
+\<open>security requirement, which contributes to fulfil the @{cc_term (unchecked)\<open>TOE\<close>}
+ @{cc_term (unchecked)\<open>SPD\<close>} as defined in a specific @{cc_term (unchecked)\<open>ST\<close>} or in a \<^cc_term>\<open>PP\<close>\<close>
+
+Definition*[SO, short_name="''security objective''"]
+\<open>statement of an intent to \<^cc_term>\<open>counter\<close> identified threats and/or satisfy identified
+ organization security policies and/or assumptions\<close>
+
+Definition*[SPD, short_name="''security problem definition''"]
+\<open>statement, which in a formal manner defines the nature and scope of the security that the
+ @{cc_term (unchecked)\<open>TOE\<close>} is intended to address\<close>
+
+Definition*[SR, short_name="''security requirement''"]
+\<open>requirement, which is part of a @{cc_term (unchecked)\<open>TOE\<close>} security specification as defined
+ in a specific @{cc_term (unchecked)\<open>ST\<close>} or in a \<^cc_term>\<open>PP\<close>\<close>
+
+Definition*[ST, short_name="''Security Target''"]
+\<open>implementation-dependent statement of security requirements for a @{cc_term (unchecked)\<open>TOE\<close>}
+ based on a \<^cc_term>\<open>SPD\<close>\<close>
+
+Definition*[selection]
+\<open>specification of one or more items from a list in a component\<close>
+
+Definition*[selection_based_SFR, short_name="''selection-based security functional requirement''"]
+\<open>\<^cc_term>\<open>SFR\<close>s in a \<^cc_term>\<open>PP\<close>, \<^cc_term>\<open>PP_module\<close>, or \<^cc_term>\<open>FP\<close> that contributes to a state
+ aspect of the PP’s, PP-Module’s or functional package’s \<^cc_term>\<open>SPD\<close> that is to be included
+ in a conformant PP or ST if a selection choice identified in the PP/PP-Module/functional package
+ indicates that it has an associated selection-based SFR\<close>
+
+Definition*[single_assurance_evaluation, short_name="''single-assurance evaluation''"]
+\<open>evaluation of a @{cc_term (unchecked)\<open>TOE\<close>} using one set of assurance requirements\<close>
+
+Definition*[SC, short_name="''strict conformance''"]
+\<open>hierarchical relationship between a \<^cc_term>\<open>PP\<close> and a PP/\<^cc_term>\<open>PP\<close> where all the requirements
+ in the PP also exist in the PP/ST\<close>
+
+Definition*[sub_TSF, short_name="''sub-TOE security functionality''"]
+\<open>combined functionality of all hardware, software, and firmware of a @{cc_term (unchecked)\<open>TOE\<close>}
+ that is relied upon for the correct enforcement of the \<^cc_term>\<open>SFR\<close>s defined in one
+ \<^cc_term>\<open>PP_configuration\<close> component\<close>
+
+Definition*[subject]
+\<open>\<^cc_term>\<open>entity\<close> in the @{cc_term (unchecked)\<open>TOE\<close>} that performs operations on objects\<close>
+
+Definition*[tailoring]
+\<open>addition of one or more functional requirements to a \<^cc_term>\<open>FP\<close>, and/or the addition of one or
+ more selections to a \<^cc_term>\<open>SFR\<close> in a functional package\<close>
+
+Definition*[TOE, short_name="''target of evaluation''"]
+\<open>set of software, firmware and/or hardware possibly accompanied by guidance, which is the subject of an evaluation\<close>
+
+Definition*[threat_agent, short_name="''threat agent''"]
+\<open>\<^cc_term>\<open>entity\<close> that has potential to exercise \<^cc_term>\<open>adverse_action\<close> on \<^cc_term>\<open>asset\<close>s
+ protected by the \<^cc_term>\<open>TOE\<close>\<close>
+
+Definition*[TSF, short_name="''TOE security functionality''"]
+\<open>combined functionality of all hardware, software, and firmware of a \<^cc_term>\<open>TOE\<close> that is relied
+ upon for the correct enforcement of the \<^cc_term>\<open>SFR\<close>s\<close>
+
+Definition*[TOE_type, short_name="''TOE type''"]
+\<open>set of characteristics common to a group of \<^cc_term>\<open>TOE\<close>\<close>
+
+Definition*[translation]
+\<open>process of describing security requirements in a standardized language\<close>
+
+Definition*[vulnerability]
+\<open>weakness in the \<^cc_term>\<open>TOE\<close> that can be used to violate the \<^cc_term>\<open>SFR\<close>s in some environment\<close>
+
+Definition*[DPA, short_name="''differential power analysis''"]
+\<open>\<close>
+
+Definition*[DRBG, short_name="''deterministic random bit generator''"]
+\<open>\<close>
+
+Definition*[ES, short_name="''electromagnetic spectrum''"]
+\<open>\<close>
+
+Definition*[GAP, short_name="''global assurance package''"]
+\<open>\<close>
+
+Definition*[GB, short_name="''gygabyte''"]
+\<open>\<close>
+
+Definition*[GHz, short_name="''gigahertz''"]
+\<open>\<close>
+
+Definition*[GUI, short_name="''graphical user interface''"]
+\<open>\<close>
+end

src/ontologies/ontologies.thy

@@ -19,6 +19,7 @@ imports
   "scholarly_paper/scholarly_paper"
   "small_math/small_math"
   "technical_report/technical_report"
+  "CC_2022_R1/Common_Criteria"
   (* "CC_v3_1_R5/CC_v3_1_R5" *)
 begin
 end

src/tests/Common_Criteria_Tests.thy

@@ -0,0 +1,251 @@
+theory Common_Criteria_Tests
+  imports  "Isabelle_DOF.Common_Criteria"
+begin
+(*Example for the verification of a Protection Profile
+  from the Common Criteria certification :
+
+  Adress of the example :
+  https://www.commoncriteriaportal.org/files/ppfiles/pp0088V2b_EP_AH_pdf.pdf
+
+*)
+open_monitor* [ex_PP_monitor1::monitor_PP_spec]
+open_monitor* [ex_PP_monitor2::monitor_PP_control]
+title*[ex_title:: title, 
+    short_title = "Some ''DBMS PP Extended Package  Access History''"]\<open>
+DBMS PP Extended Package – Access History\<close>
+
+open_monitor* [ex_Intro_monitor::PP_introduction_monitor]
+chapter*[ex_intro::PP_introduction]\<open>)
+INTRODUCTION TO THE DBMS PP EXTENDED PACKAGE
+\<close>
+section*[title_identification::PP_reference, 
+version = "''1.02''", 
+sponsors = "[''DBMS Working Group / Technical Community'']", 
+publication_date = "''23rd March, 2017''",
+cc_title = "@{title \<open>ex_title\<close>}"]\<open>
+DBMS PP Extended Package Identification
+\<close>
+text*[ex_identification::PP_introduction_report]\<open>
+Title: DBMS PP Extended Package – Access History DBMS PP Extended Package Abbreviation: AH Sponsor: DBMS Working Group / Technical Community CC Version: Common Criteria (CC) Version 3.1 R4
+EP Version: 1.02
+Publication Date: 23rd March, 2017
+Keywords: database management system, DBMS PP, DBMS, COTS, access history
+\<close>
+section*[title_overview::PP_overview]\<open>
+DBMS PP Extended Package Overview
+\<close>
+text*[ex_overview::PP_introduction_report]\<open>
+The base DBMS PP Security Problem Definition does not include a security objective relating to access history.
+While many organizations do not specify this objective as part of their security problem definition, this additional security objective may need to be included in the security problem definition by some organizations in order to support further mitigation of the threats of T.ACCESS_TSFDATA, T.IA_MASQUERADE and T.TSF_COMPROMISE. This is achieved by allowing trained users to review their access history in order to help identify unauthorized access attempts.
+This extended package supplements the DBMS PP by adding the TOE Security Objective O.ACCESS-HISTORY and the security functional requirement supporting that objective.
+\<close>
+section*[title_framework::PP_introduction_title]\<open>
+DBMS PP Extended Package Framework
+\<close>
+text*[ex_framework::PP_introduction_report]\<open>
+The DBMS PP Extended Package – Access History is part of the Database Management System Protection Profile framework defined in [DBMS PP] chapter 1.3. An ST author may optionally use this document specifying an extended package in addition to the DBMS base protection profile defined with [DBMS PP] chapters 3ff.
+\<close>
+section*[title_structure::PP_introduction_title]\<open>
+Structure of the Extended Package
+\<close>
+text*[ex_structure::PP_introduction_report]\<open>
+This document is structured as follows:
+• Chapter 1 provides the introduction into the DBMS PP extended package.
+• Chapter 2 specifies the conformance claims for the DBMS PP extended package.
+• Chapter 3 contains the security problem definition applicable to this DBMS PP extended package.
+• Chapter 4 defines the objectives to be covered by \<^cc_term>\<open>TOE\<close>s that are conformant to this DBMS 
+            \<^cc_term>\<open>PP\<close>  extended package.
+• Chapter 5 contains the definition of extended components used in this DBMS PP extended package.
+• Chapter 6 holds the security requirements definition for this DBMS PP extended package. database management system.
+\<close>
+section*[title_references::PP_introduction_title]\<open>
+References
+\<close>
+text*[ex_references::PP_introduction_report]\<open>
+The references given in the [DBMS PP] are also applicable to this document. The following references are also applicable to this document:
+DBMS PP Protection Profile for Database Management Systems (Base Package) V 2.12
+\<close>
+section*[title_conventions::PP_introduction_title]\<open>
+References
+\<close>
+text*[ex_documents_conventions::PP_introduction_report]\<open>
+Document Conventions
+The document convention explained in Chapter 1.4 of [DBMS PP] are applicable in this document.
+\<close>
+close_monitor*[ex_Intro_monitor]
+
+open_monitor*[ex_Conformance_monitor::Conformance_monitor]
+chapter*[title_Conf_claims::Conformance]\<open>
+CONFORMANCE CLAIMS
+\<close>
+text*[ex_Conf_claims::PP_conformance_report]\<open>
+The following sections describe the conformance claims of the Database Management System Protection Profile (DBMS PP).
+\<close>
+section*[title_Conf_with_CC::PP_conformance_title]\<open>
+Conformance with CC
+\<close>
+text*[ex_Conf_with_CC::PP_conformance_report]\<open>
+This extended package does not augment the conformance claim of the DBMS PP base specified in [DBMS PP] chapter 3.
+\<close>
+section*[title_EPCR::PP_conformance_title]\<open>
+Extended Package Conformance Rules
+\<close>
+text*[ex_EPCR::PP_conformance_report]\<open>
+This extended package does not depend on other DBMS PP extended packages.
+This package can only be claimed together with the DBMS PP base package, in the version defined in [DBMS PP].
+This extended package does not conflict with any other DBMS PP extended package at the time of publication.
+\<close>
+close_monitor*[ex_Conformance_monitor]
+
+open_monitor*[ex_SPD_monitor::SPD_monitor]
+chapter*[title_SPD::SPD]\<open>)
+SECURITY PROBLEM DEFINITION
+\<close>
+text*[ex_SPD::PP_SPD_report]\<open>
+The security problem definition of the DBMS PP Extended Package – Access History does not change the security problem definition of the DBMS PP base.
+\<close>
+(* text*[ex_error::text_element]\<open>
+This instance is an example of the use of the reject clause by   \<^monitor_PP_control>\<open>PP_monitor2\<close>
+\<close> *)
+section*[title_threats::Threats]\<open>
+Threats
+\<close>
+text*[ex_threats::PP_SPD_report]\<open>
+This extended package neither adds to nor alters the threats given in [DBMS PP].
+\<close>
+section*[title_OSPs::OSPs]\<open>
+Organizational Security Policies
+\<close>
+text*[ex_OSPs::PP_SPD_report]\<open>
+This extended package neither adds to nor alters any organizational security policies given in [DBMS PP].
+\<close>
+section*[title_Assumptions::Assumptions]\<open>Assumptions\<close>
+
+text*[ex_Assumptions::PP_SPD_report]\<open>
+This extended package neither adds to nor alters the assumptions given in [DBMS PP].
+\<close>
+close_monitor*[ex_SPD_monitor]
+
+open_monitor*[ex_SO_monitor::SO_monitor]
+chapter*[title_SO::SO]\<open>
+SECURITY OBJECTIVES
+\<close>
+text*[ex_SO::PP_SO_report]\<open>
+This section identifies the additional security objectives of the \<^cc_term>\<open>TOE\<close> and its supporting environment met by this extended package.
+These security objectives identify the responsibilities of the cc_term>\<open>TOE\<close> and its environment in meeting the security problem definition (SPD).
+\<close>
+section*[title_TOE_SO::SO_for_TOE]\<open>
+TOE Security Objectives
+\<close>
+text*[ex_TOE_SO::PP_SO_report]\<open>
+This extended package specifies one additional security objective in addition to those given in [DBMS PP].
+\<close>
+section*[title_OE_SO::SO_for_OE]\<open>
+Operational Environment Security Objectives
+\<close>
+text*[ex_OE_SO::PP_SO_report]\<open>
+This extended package neither adds to nor alters the operational environment security objectives 
+given in [DBMS PP].
+\<close>
+section*[title_R_for_SO::SOR]\<open>Rationale for Security Objectives\<close>
+
+text*[ex_R_for_SO::PP_SO_report]\<open>
+The table below gives a summary of the policies, and threats relating to the TOE security objectives.
+Security objectives coverage
+Rationale for the Security objectives sufficiency
+The table below gives the rationale for the TOE security objectives. In this extended package security objective O.ACCESS_HISTORY is supportive in reducing the threats T.ACCESS_TSFDATA, T.IA_MASQUERADE and T.TSF_COMPROMISE given in the base DBMS PP.
+\<close>
+close_monitor*[ex_SO_monitor]
+
+open_monitor*[ex_ECD_monitor::ECD_monitor]
+chapter*[title_ESFR::ECD]\<open>
+EXTENDED SECURITY FUNCTIONAL REQUIREMENTS
+\<close>
+text*[ex_ESFR::PP_ECD_report]\<open>
+This extended package defines one extended SFR.
+\<close>
+section*[title_ESFR_spe::PP_ECD_title]\<open>
+Extended Security Functional Requirements Specified By This Extended Package
+\<close>
+text*[ex_ESFR_spe::PP_ECD_report]\<open>
+FTA_TAH_(EXT).1 TOE access information
+FTA_TAH_(EXT).1 TOE access information provides the requirement for a TOE to make available information related to attempts to establish a session.
+Component levelling
+FTA_TAH_(EXT).1 is not hierarchical to any other components. Management: FTA_TAH_(EXT).1
+There are no management activities foreseen.
+Audit: FTA_TAH_(EXT).1
+There are no auditable events foreseen.
+FTA_TAH_(EXT).1 TOE access information
+Hierarchical to: No other components.
+Dependencies: No dependencies.
+FTA_TAH_(EXT).1.1
+Upon a session establishment attempt, the TSF shall store
+a. the [date and time] of the session establishment attempt of the user.
+b. the incremental count of successive unsuccessful session establishment attempt(s).
+FTA_TAH_(EXT).1.2
+Upon successful session establishment, the TSF shall allow the [date and time] of
+a. the previous last successful session establishment, and
+b. the last unsuccessful attempt to session establishment and the number of unsuccessful attempts since the previous last successful session establishment
+to be retrieved by the user.
+\<close>
+section*[title_R_for_ESFR::PP_ECD_title]\<open>
+Rationale For The Extended Security Functional Requirement
+\<close>
+text*[ex_R_for_ESFR::PP_ECD_report]\<open>
+The table below presents a rationale for the inclusion of the extended functional security requirements found in this extended package.
+\<close>
+close_monitor*[ex_ECD_monitor]
+
+open_monitor*[ex_SR_monitor::SR_monitor]
+chapter*[title_SR::SR]\<open>
+SECURITY REQUIREMENTS
+\<close>
+section*[title_ASFR::SFR]\<open>
+Additional Security Functional Requirements to The Base DBMS PP
+\<close>
+text*[ex_ASFR::PP_SR_report]\<open>)
+This section defines the functional requirements for the TOE that are amended or specified by this extended package.
+Functional requirements in this extended package were drawn directly from Part 2 of the CC [1b], or were based on Part 2 of the CC, including the use of extended components. These requirements are relevant to supporting the secure operation of the TOE.
+TOE Access (FTA)
+FTA_TAH_(EXT).1 TOE access information FTA_TAH_(EXT).1.1
+Upon a session establishment attempt, the TSF shall store
+a. the [date and time] of the session establishment attempt of the user.
+b. the incremental count of successive unsuccessful session establishment attempt(s).
+FTA_TAH_(EXT).1.2
+Upon successful session establishment, the TSF shall allow the [date and time] of
+a. the previous last successful session establishment, and
+b. the last unsuccessful attempt to session establishment and the number of unsuccessful attempts since the previous last successful session establishment
+to be retrieved by the user.
+\<close>
+section*[title_SFRR::SFR]\<open>
+Security Functional Requirements Refined from The Base DBMS PP
+\<close>
+text*[ex_SFRR::PP_SR_report]\<open>
+Security Audit (FAU)
+FAU_GEN.1 Audit data generation
+\<close>
+section*[title_R_for_ASFR::SFR]\<open>
+Rationale For The Additional TOE Security Functional Requirements
+\<close>
+text*[ex_R_for_ASFR::PP_SR_report]\<open>
+The following table provides the rationale for the selection of the security functional requirements. It traces each TOE security objective to the identified security functional requirements.
+\<close>
+section*[title_R_for_all_SFRD::SFR]\<open>
+Rationale for Satisfying All Security Functional Requirement Dependencies
+\<close>
+text*[ex_R_for_all_SFRD::PP_SR_report]\<open>
+This extended package does not contain any additional or amended SFRs that have dependencies.
+\<close>
+text*[title_SAR::SAR]\<open>
+Security Assurance Requirements
+\<close>
+text*[ex_SARD::PP_SR_report]\<open>
+This extended package neither adds to nor alters the security assurance requirements given in [DBMS PP].
+\<close>
+close_monitor*[ex_SR_monitor]
+
+close_monitor*[ex_PP_monitor2]
+close_monitor*[ex_PP_monitor1]
+
+
+end

src/tests/ROOT

@@ -9,5 +9,6 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" +
     "Evaluation"
     "High_Level_Syntax_Invariants"
     "Ontology_Matching_Example"
+    "Common_Criteria_Tests"
   theories [condition = ISABELLE_DOF_HOME]
     "Isabelle2022"