Change of cc and cc_test to be used to create a pdf
This commit is contained in:
Pierre Derathe
parent
5aaa5451f6
commit
d67e270b3d
|
|
@ -55,41 +55,59 @@ doc_class cc_spec_report = text_element +
|
|||
|
||||
doc_class PP_report = cc_spec_report +
|
||||
cc_spec :: "cc_spec" <= "PP"
|
||||
level :: "int option" <= "Some 1"
|
||||
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"
|
||||
cc_spec_chapter :: "cc_spec_chapter" <= "Introduction"
|
||||
invariant introduction_chapter :: \<open>cc_spec_chapter \<sigma> = Introduction\<close>
|
||||
|
||||
doc_class PP_Conformance_report = PP_report +
|
||||
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_report +
|
||||
doc_class PP_introduction = PP_introduction_title +
|
||||
level :: "int option" <= "Some 0"
|
||||
|
||||
doc_class PP_reference = PP_introduction_report +
|
||||
doc_class PP_reference = PP_introduction_title +
|
||||
cc_spec_section :: "cc_spec_section" <= "PP_reference"
|
||||
cc_title :: "title"
|
||||
cc_title :: "title"
|
||||
version :: "string" <= "''''"
|
||||
sponsors :: "string list" <= "[]"
|
||||
publication_date :: "string" <= "''''"
|
||||
|
|
@ -101,66 +119,66 @@ 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>
|
||||
|
||||
doc_class PP_overview = PP_introduction_report +
|
||||
cc_spec_section :: "cc_spec_section" <= "PP_overview"
|
||||
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_report +
|
||||
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_report +
|
||||
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_report +
|
||||
cc_spec_section :: "cc_spec_section" <= "Threats"
|
||||
doc_class Threats = PP_SPD_title +
|
||||
cc_spec_section :: "cc_spec_section" <= "Threats"
|
||||
|
||||
doc_class Assumptions = PP_SPD_report +
|
||||
cc_spec_section :: "cc_spec_section" <= "Assumptions"
|
||||
doc_class Assumptions = PP_SPD_title +
|
||||
cc_spec_section :: "cc_spec_section" <= "Assumptions"
|
||||
|
||||
doc_class OSPs = PP_SPD_report +
|
||||
cc_spec_section :: "cc_spec_section" <= "OSPs"
|
||||
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_report +
|
||||
doc_class SO = PP_SO_title +
|
||||
level :: "int option" <= "Some 0"
|
||||
|
||||
doc_class SO_for_TOE = PP_SO_report +
|
||||
cc_spec_section :: "cc_spec_section" <= "SO_for_TOE"
|
||||
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_report +
|
||||
cc_spec_section :: "cc_spec_section" <= "SO_for_OE"
|
||||
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_report +
|
||||
cc_spec_section :: "cc_spec_section" <= "SOR"
|
||||
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_report +
|
||||
doc_class ECD = PP_ECD_title +
|
||||
level :: "int option" <= "Some 0"
|
||||
|
||||
doc_class ECD_section = PP_ECD_report +
|
||||
ECD_title :: "title"
|
||||
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_report +
|
||||
doc_class SR = PP_SR_title +
|
||||
level :: "int option" <= "Some 0"
|
||||
|
||||
doc_class SFR = PP_SR_report +
|
||||
cc_spec_section :: "cc_spec_section" <= "SFRs"
|
||||
doc_class SFR = PP_SR_title +
|
||||
cc_spec_section :: "cc_spec_section" <= "SFRs"
|
||||
|
||||
doc_class SAR = PP_SR_report +
|
||||
cc_spec_section :: "cc_spec_section" <= "SARs"
|
||||
doc_class SAR = PP_SR_title +
|
||||
cc_spec_section :: "cc_spec_section" <= "SARs"
|
||||
|
||||
(* Declaration of the monitor of each chapter of the PP specification *)
|
||||
|
||||
|
|
@ -170,7 +188,7 @@ doc_class PP_introduction_monitor =
|
|||
|
||||
doc_class Conformance_monitor =
|
||||
cc_spec :: "cc_spec" <= "PP"
|
||||
accepts "Conformance ~~ \<lbrace>PP_Conformance_report\<rbrace>\<^sup>*"
|
||||
accepts "Conformance ~~ \<lbrace>PP_conformance_report\<rbrace>\<^sup>*"
|
||||
|
||||
doc_class SPD_monitor =
|
||||
cc_spec :: "cc_spec" <= "PP"
|
||||
|
|
@ -192,10 +210,6 @@ 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"
|
||||
|
|
|
|||
|
|
@ -10,37 +10,45 @@ begin
|
|||
*)
|
||||
open_monitor* [ex_PP_monitor1::monitor_PP_spec]
|
||||
open_monitor* [ex_PP_monitor2::monitor_PP_control]
|
||||
text*[ex_title:: title,
|
||||
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]
|
||||
text*[ex_intro::PP_introduction]\<open>
|
||||
chapter*[ex_intro::PP_introduction]\<open>
|
||||
INTRODUCTION TO THE DBMS PP EXTENDED PACKAGE
|
||||
\<close>
|
||||
text*[ex_identification::PP_reference,
|
||||
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>
|
||||
text*[ex_overview::PP_overview]\<open>
|
||||
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>
|
||||
text*[ex_framework::PP_introduction_report]\<open>
|
||||
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>
|
||||
text*[ex_structure::PP_introduction_report]\<open>
|
||||
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.
|
||||
|
|
@ -49,11 +57,16 @@ 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>
|
||||
text*[ex_references::PP_introduction_report]\<open>
|
||||
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.
|
||||
|
|
@ -61,16 +74,22 @@ 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]
|
||||
text*[ex_Conf_claims::Conformance]\<open>
|
||||
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>
|
||||
text*[ex_Conf_with_CC::PP_Conformance_report]\<open>
|
||||
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>
|
||||
text*[ex_EPCR::PP_Conformance_report]\<open>
|
||||
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.
|
||||
|
|
@ -78,43 +97,59 @@ 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]
|
||||
text*[ex_SPD::SPD]\<open>
|
||||
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> *)
|
||||
text*[ex_treats::Threats]\<open>
|
||||
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>
|
||||
text*[ex_OSPs::OSPs]\<open>
|
||||
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>
|
||||
text*[ex_Assumptions::Assumptions]\<open>
|
||||
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]
|
||||
text*[ex_SO::SO]\<open>
|
||||
chapter*[title_SO::SO]\<open>
|
||||
SECURITY OBJECTIVES
|
||||
\<close>
|
||||
text*[ex_SO::PP_SO_report]\<open>
|
||||
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>
|
||||
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>
|
||||
text*[ex_OE_SO::SO_for_OE]\<open>
|
||||
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>
|
||||
text*[ex_R_for_SO::SOR]\<open>
|
||||
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
|
||||
|
|
@ -123,12 +158,16 @@ 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]
|
||||
text*[ex_ESFR::ECD]\<open>
|
||||
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>
|
||||
text*[ex_ESFR_spe::PP_ECD_report]\<open>
|
||||
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
|
||||
|
|
@ -149,18 +188,22 @@ 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>
|
||||
text*[ex_R_for_ESFR::PP_ECD_report]\<open>
|
||||
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]
|
||||
text*[ex_SR::SR]\<open>
|
||||
chapter*[title_SR::SR]\<open>
|
||||
SECURITY REQUIREMENTS
|
||||
\<close>
|
||||
text*[ex_ASFR::SFR]\<open>
|
||||
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)
|
||||
|
|
@ -174,21 +217,29 @@ 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>
|
||||
text*[ex_SFRR::SFR]\<open>
|
||||
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>
|
||||
text*[ex_R_for_ASFR::SFR]\<open>
|
||||
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>
|
||||
text*[ex_R_for_all_SFRD::SFR]\<open>
|
||||
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*[ex_::SAR]\<open>
|
||||
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]
|
||||
|
|
|
|||
Loading…
Reference in New Issue