Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Final version

This commit is contained in:
Pierre Derathe 2023-02-19 16:26:23 +01:00
parent 2f4307a907
commit ec81f7bbce
2 changed files with 0 additions and 224 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

99
src/ontologies/CC_2022_R1/Common_Criteria.thy
View File

@ -55,16 +55,11 @@ doc_class cc_spec_report = text_element +
doc_class PP_report = cc_spec_report +
cc_spec :: "cc_spec" <= "PP"
<<<<<<< HEAD
level :: "int option"
=======
level :: "int option" <= "Some 1"
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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 +
<<<<<<< HEAD
cc_spec_chapter :: "cc_spec_chapter" <= "Introduction"
invariant introduction_chapter :: \<open>cc_spec_chapter \<sigma> = Introduction\<close>
@ -78,50 +73,31 @@ doc_class PP_conformance_report = PP_report +
doc_class PP_conformance_title = PP_conformance_report +
level :: "int option" <= "Some 1"
=======
cc_spec_chapter :: "cc_spec_chapter" <= "Introduction"
invariant introduction_chapter :: \<open>cc_spec_chapter \<sigma> = Introduction\<close>
doc_class PP_Conformance_report = PP_report +
cc_spec_chapter :: "cc_spec_chapter" <= "Conformance"
invariant conformance_chapter :: \<open>cc_spec_chapter \<sigma> = Conformance\<close>
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
doc_class PP_SPD_report = PP_report +
cc_spec_chapter :: "cc_spec_chapter" <= "SPD"
invariant SPD_chapter :: \<open>cc_spec_chapter \<sigma> = SPD\<close>
<<<<<<< HEAD
doc_class PP_SPD_title = PP_SPD_report +
level :: "int option" <= "Some 1"
=======
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
doc_class PP_SO_report = PP_report +
cc_spec_chapter :: "cc_spec_chapter" <= "SO"
invariant SO_chapter :: \<open>cc_spec_chapter \<sigma> = SO\<close>
<<<<<<< HEAD
doc_class PP_SO_title = PP_SO_report +
level :: "int option" <= "Some 1"
=======
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
doc_class PP_ECD_report = PP_report +
cc_spec_chapter :: "cc_spec_chapter" <= "ECD"
invariant ECD_chapter :: \<open>cc_spec_chapter \<sigma> = ECD\<close>
<<<<<<< HEAD
doc_class PP_ECD_title = PP_ECD_report +
level :: "int option" <= "Some 1"
=======
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
doc_class PP_SR_report = PP_report +
cc_spec_chapter :: "cc_spec_chapter" <= "SR"
invariant SR_chapter :: \<open>cc_spec_chapter \<sigma> = SR\<close>
<<<<<<< HEAD
doc_class PP_SR_title = PP_SR_report +
level :: "int option" <= "Some 1"
@ -130,17 +106,8 @@ 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"
=======
(* Declaration of the sections in the PP introduction *)
doc_class PP_introduction = PP_introduction_report +
level :: "int option" <= "Some 0"
doc_class PP_reference = PP_introduction_report +
cc_spec_section :: "cc_spec_section" <= "PP_reference"
cc_title :: "title"
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
version :: "string" <= "''''"
sponsors :: "string list" <= "[]"
publication_date :: "string" <= "''''"
@ -152,26 +119,16 @@ doc_class PP_reference = PP_introduction_report +
term\<open>scholarly_paper.short_title (cc_title a) \<noteq> None \<and>
the(scholarly_paper.short_title (cc_title a)) \<noteq> ''''\<close>
<<<<<<< HEAD
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 +
=======
doc_class PP_overview = PP_introduction_report +
cc_spec_section :: "cc_spec_section" <= "PP_overview"
(* Declaration of the sections in the conformance *)
doc_class Conformance = PP_Conformance_report +
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
level :: "int option" <= "Some 0"
(* Declaration of the sections in the security problem definition *)
<<<<<<< HEAD
doc_class SPD = PP_SPD_title +
cc_definition :: "cc_term option" <= "Some @{cc-term \<open>SPD\<close>}"
level :: "int option" <= "Some 0"
@ -184,25 +141,10 @@ doc_class Assumptions = PP_SPD_title +
doc_class OSPs = PP_SPD_title +
cc_spec_section :: "cc_spec_section" <= "OSPs"
=======
doc_class SPD = PP_SPD_report +
cc_definition :: "cc_term option" <= "Some @{cc-term \<open>SPD\<close>}"
level :: "int option" <= "Some 0"
doc_class Threats = PP_SPD_report +
cc_spec_section :: "cc_spec_section" <= "Threats"
doc_class Assumptions = PP_SPD_report +
cc_spec_section :: "cc_spec_section" <= "Assumptions"
doc_class OSPs = PP_SPD_report +
cc_spec_section :: "cc_spec_section" <= "OSPs"
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
type_synonym organizational_security_policies = OSPs
(* Declaration of the sections in the security objectives *)
<<<<<<< HEAD
doc_class SO = PP_SO_title +
level :: "int option" <= "Some 0"
@ -216,43 +158,19 @@ doc_class SO_for_OE = PP_SO_title +
doc_class SOR = PP_SO_title +
cc_spec_section :: "cc_spec_section" <= "SOR"
=======
doc_class SO = PP_SO_report +
level :: "int option" <= "Some 0"
doc_class SO_for_TOE = PP_SO_report +
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_report +
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_report +
cc_spec_section :: "cc_spec_section" <= "SOR"
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
type_synonym security_objectives_rationale = SOR
(* Declaration of the sections in the extended components definition *)
<<<<<<< HEAD
doc_class ECD = PP_ECD_title +
level :: "int option" <= "Some 0"
doc_class ECD_section = PP_ECD_title +
level :: "int option" <= "Some 1"
=======
doc_class ECD = PP_ECD_report +
level :: "int option" <= "Some 0"
doc_class ECD_section = PP_ECD_report +
ECD_title :: "title"
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
type_synonym extended_component_definition = ECD_section
(* Declaration of the sections in the Security requirements *)
<<<<<<< HEAD
doc_class SR = PP_SR_title +
level :: "int option" <= "Some 0"
@ -261,16 +179,6 @@ doc_class SFR = PP_SR_title +
doc_class SAR = PP_SR_title +
cc_spec_section :: "cc_spec_section" <= "SARs"
=======
doc_class SR = PP_SR_report +
level :: "int option" <= "Some 0"
doc_class SFR = PP_SR_report +
cc_spec_section :: "cc_spec_section" <= "SFRs"
doc_class SAR = PP_SR_report +
cc_spec_section :: "cc_spec_section" <= "SARs"
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
(* Declaration of the monitor of each chapter of the PP specification *)
@ -280,11 +188,7 @@ doc_class PP_introduction_monitor =
doc_class Conformance_monitor =
cc_spec :: "cc_spec" <= "PP"
<<<<<<< HEAD
accepts "Conformance ~~ \<lbrace>PP_conformance_report\<rbrace>\<^sup>*"
=======
accepts "Conformance ~~ \<lbrace>PP_Conformance_report\<rbrace>\<^sup>*"
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
doc_class SPD_monitor =
cc_spec :: "cc_spec" <= "PP"
@ -306,13 +210,10 @@ doc_class Appendix = cc_spec_report +
level :: "int option" <= "Some 0"
letter :: "char"
<<<<<<< HEAD
=======
doc_class Annex = cc_spec_report +
level :: "int option" <= "Some 0"
letter :: "char"
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
(* Declaration of the monitor of the whole PP specification *)
doc_class monitor_cc_spec =
cc_spec :: "cc_spec"

125
src/tests/Common_Criteria_Tests.thy
View File

@ -10,55 +10,35 @@ begin
*)
open_monitor* [ex_PP_monitor1::monitor_PP_spec]
open_monitor* [ex_PP_monitor2::monitor_PP_control]
<<<<<<< HEAD
title*[ex_title:: title,
=======
text*[ex_title:: title,
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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]
<<<<<<< HEAD
chapter*[ex_intro::PP_introduction]\<open>
INTRODUCTION TO THE DBMS PP EXTENDED PACKAGE
\<close>
section*[title_identification::PP_reference,
=======
text*[ex_intro::PP_introduction]\<open>
INTRODUCTION TO THE DBMS PP EXTENDED PACKAGE
\<close>
text*[ex_identification::PP_reference,
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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
<<<<<<< HEAD
\<close>
text*[ex_identification::PP_introduction_report]\<open>
=======
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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>
<<<<<<< HEAD
section*[title_overview::PP_overview]\<open>
DBMS PP Extended Package Overview
\<close>
text*[ex_overview::PP_introduction_report]\<open>
=======
text*[ex_overview::PP_overview]\<open>
DBMS PP Extended Package Overview
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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>
<<<<<<< HEAD
section*[title_framework::PP_introduction_title]\<open>
DBMS PP Extended Package Framework
\<close>
@ -69,14 +49,6 @@ section*[title_structure::PP_introduction_title]\<open>
Structure of the Extended Package
\<close>
text*[ex_structure::PP_introduction_report]\<open>
=======
text*[ex_framework::PP_introduction_report]\<open>
DBMS PP Extended Package Framework
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>
text*[ex_structure::PP_introduction_report]\<open>
Structure of the Extended Package
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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.
@ -85,7 +57,6 @@ This document is structured as follows:
• 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>
<<<<<<< HEAD
section*[title_references::PP_introduction_title]\<open>
References
\<close>
@ -96,13 +67,6 @@ DBMS PP Protection Profile for Database Management Systems (Base Package) V 2.12
section*[title_conventions::PP_introduction_title]\<open>
References
\<close>
=======
text*[ex_references::PP_introduction_report]\<open>
References
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>
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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.
@ -110,7 +74,6 @@ The document convention explained in Chapter 1.4 of [DBMS PP] are applicable in
close_monitor*[ex_Intro_monitor]
open_monitor*[ex_Conformance_monitor::Conformance_monitor]
<<<<<<< HEAD
chapter*[title_Conf_claims::Conformance]\<open>
CONFORMANCE CLAIMS
\<close>
@ -127,18 +90,6 @@ section*[title_EPCR::PP_conformance_title]\<open>
Extended Package Conformance Rules
\<close>
text*[ex_EPCR::PP_conformance_report]\<open>
=======
text*[ex_Conf_claims::Conformance]\<open>
CONFORMANCE CLAIMS
The following sections describe the conformance claims of the Database Management System Protection Profile (DBMS PP).
\<close>
text*[ex_Conf_with_CC::PP_Conformance_report]\<open>
Conformance with CC
This extended package does not augment the conformance claim of the DBMS PP base specified in [DBMS PP] chapter 3.
\<close>
text*[ex_EPCR::PP_Conformance_report]\<open>
Extended Package Conformance Rules
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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.
@ -146,21 +97,15 @@ This extended package does not conflict with any other DBMS PP extended package
close_monitor*[ex_Conformance_monitor]
open_monitor*[ex_SPD_monitor::SPD_monitor]
<<<<<<< HEAD
chapter*[title_SPD::SPD]\<open>
SECURITY PROBLEM DEFINITION
\<close>
text*[ex_SPD::PP_SPD_report]\<open>
=======
text*[ex_SPD::SPD]\<open>
SECURITY PROBLEM DEFINITION
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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> *)
<<<<<<< HEAD
section*[title_threats::Threats]\<open>
Threats
\<close>
@ -177,24 +122,11 @@ section*[title_Assumptions::Assumptions]\<open>
Assumptions
\<close>
text*[ex_Assumptions::PP_SPD_report]\<open>
=======
text*[ex_treats::Threats]\<open>
Threats
This extended package neither adds to nor alters the threats given in [DBMS PP].
\<close>
text*[ex_OSPs::OSPs]\<open>
Organizational Security Policies
This extended package neither adds to nor alters any organizational security policies given in [DBMS PP].
\<close>
text*[ex_Assumptions::Assumptions]\<open>
Assumptions
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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]
<<<<<<< HEAD
chapter*[title_SO::SO]\<open>
SECURITY OBJECTIVES
\<close>
@ -218,23 +150,6 @@ section*[title_R_for_SO::SOR]\<open>
Rationale for Security Objectives
\<close>
text*[ex_R_for_SO::PP_SO_report]\<open>
=======
text*[ex_SO::SO]\<open>
SECURITY OBJECTIVES
This section identifies the additional security objectives of the TOE and its supporting environment met by this extended package.
These security objectives identify the responsibilities of the TOE and its environment in meeting the security problem definition (SPD).
\<close>
text*[ex_TOE_SO::SO_for_TOE]\<open>
TOE Security Objectives
This extended package specifies one additional security objective in addition to those given in [DBMS PP].
\<close>
text*[ex_OE_SO::SO_for_OE]\<open>
Operational Environment Security Objectives
This extended package neither adds to nor alters the operational environment security objectives given in [DBMS PP].
\<close>
text*[ex_R_for_SO::SOR]\<open>
Rationale for Security Objectives
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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
@ -243,7 +158,6 @@ The table below gives the rationale for the TOE security objectives. In this ext
close_monitor*[ex_SO_monitor]
open_monitor*[ex_ECD_monitor::ECD_monitor]
<<<<<<< HEAD
chapter*[title_ESFR::ECD]\<open>
EXTENDED SECURITY FUNCTIONAL REQUIREMENTS
\<close>
@ -254,14 +168,6 @@ 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>
=======
text*[ex_ESFR::ECD]\<open>
EXTENDED SECURITY FUNCTIONAL REQUIREMENTS
This extended package defines one extended SFR.
\<close>
text*[ex_ESFR_spe::PP_ECD_report]\<open>
Extended Security Functional Requirements Specified By This Extended Package
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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
@ -282,21 +188,15 @@ 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>
<<<<<<< HEAD
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>
=======
text*[ex_R_for_ESFR::PP_ECD_report]\<open>
Rationale For The Extended Security Functional Requirement
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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]
<<<<<<< HEAD
chapter*[title_SR::SR]\<open>
SECURITY REQUIREMENTS
\<close>
@ -304,13 +204,6 @@ section*[title_ASFR::SFR]\<open>
Additional Security Functional Requirements to The Base DBMS PP
\<close>
text*[ex_ASFR::PP_SR_report]\<open>
=======
text*[ex_SR::SR]\<open>
SECURITY REQUIREMENTS
\<close>
text*[ex_ASFR::SFR]\<open>
Additional Security Functional Requirements to The Base DBMS PP
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
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)
@ -324,7 +217,6 @@ 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>
<<<<<<< HEAD
section*[title_SFRR::SFR]\<open>
Security Functional Requirements Refined from The Base DBMS PP
\<close>
@ -348,23 +240,6 @@ text*[title_SAR::SAR]\<open>
Security Assurance Requirements
\<close>
text*[ex_SARD::PP_SR_report]\<open>
=======
text*[ex_SFRR::SFR]\<open>
Security Functional Requirements Refined from The Base DBMS PP
Security Audit (FAU)
FAU_GEN.1 Audit data generation
\<close>
text*[ex_R_for_ASFR::SFR]\<open>
Rationale For The Additional TOE Security Functional Requirements
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>
text*[ex_R_for_all_SFRD::SFR]\<open>
Rationale for Satisfying All Security Functional Requirement Dependencies
This extended package does not contain any additional or amended SFRs that have dependencies.
\<close>
text*[ex_::SAR]\<open>
Security Assurance Requirements
>>>>>>> a75c47d6b6635c292cb364bb32bb6cd4ed3c1cd6
This extended package neither adds to nor alters the security assurance requirements given in [DBMS PP].
\<close>
close_monitor*[ex_SR_monitor]