ISO IEC 29128:2011 pdf – Information technology一Security techniques – Verification of cryptographic protocols.
The developer shall provide information about language which is used for describe adversarial model of the target protocol.
7.2.3.3 Content and presentation elements
The statement of adversarial model shall describe all necessary items in Clause 5.4 such as network specification, ability ol attacker and scenario writlen In a formal tool-specific specification language. This formal adversarial model shall conform to PAM_INFORMAL
lntomatn about the tool-specific specification language shall include matenals such as reference manuals and papers.
7.2.3.4 Evaluator action elements
The evaluator shal confirm that the information provided meets all requirements for content and presentation.
NOTE 1 Adversanal model can be specified in looi-spechc specification language For efticiency reasons, most tools hard-wire’ this intruder model into thee tool, e.g., via speciazed calculi for constraint solving. If one uses a general- purpose model cbecker, one must explicitly represent the intruder as a process.
NOTE 2 Adversanal model can be specified In general predicate logic language as an inductively defined set as part of the proloool specification. The adversarial model can also be specified as an intruder icxmahzation integrated Mthin verification tools
7.3 Security properties
7.3.1 General
Properties p specify requirements on the behavior of the protocol, For the vast majority of Formal Methods. the model N constitutes a transition system, describing the system states and the transitions between states. In this setting, a property rp is typically either a state-properly, i.e., some invariant that should hold for all reachable system states or a temporal property descring valid sequences of states (or system events). Standard examples of security properties are secrecy properties or authentication properties. A secrecy (or confidentiality) property is generally a state invariant and says that some set S of data items (e.9.. keys and nonces) Is never obtained by the attacker In an unencrypted form. Authentication properties include both message-origin authentication (that a message supposedly sent by a party actually was sent by the party) and entity authentication (roughly. that a given principal is currently participating in the protocol in some stated role).
7.4 Self-assessment evidence for verification
7.4.1 General
Self-assessment evidence of vent Icatlon Is an evidence that the protocol designer solves the model-diecking problem of demonstrating that the model M has the property q’. i.e.. M satisfies p. There are a variety of different Formal Methods capable of establishing or refuting that M satisfies ‘p.
7.4.2 PEV_ARGUMENT
7.4.2.1 Objectives
The evidence for verification for PEV ARGUMENT consists of informal argument of why the protocol has the specified properties.
7.4.2.2 Developer action elements
The developer shall provide information how the protocol specification fulfills the security property in the adversarial model.
7.4.2.3 Content and presentation elements
The information shall describe the reason in a verifiable way why the protocol specification assures the security property in the adversarial model.
7.4.2.4 Evaluator action elements
The evaluator shal confirm that the Information provided meets all requirements for content and presentation.
7.4.3 PEV_HANDPROVEN
7.4.3.1 Objectives
The evidence for verification for PEV_HANDPROVEN consists of mathematically formal paper-and-pencil proof of why the protocol has the specified properties
7.4.3.2 Developer action elements
The developer shall provide information how the protocol specification fulfills the security property in the adversarial model.
7.4.3.3 Content and presentation elements
The information shall describe the reason In a verifiable way why the protocol specification assures the security property in the adversarial mOdel.
7.4.3.4 Evaluator action elements
The evaluator shal confirm that the information provided meets all requirements for content and presentation.
7.4.4 PEV_BOUNDED
7.4.4.1 Objectives
The evidence for verifcation for PEV_BOUNDED consists of the protocol specification and security properties and (it requwed) the adversarial model used by a verification tool such as model checkers along with additional parameters. The most important parameter is to provide a bound on the number of role instances. Dillerent model checkers provide different ways of doing this. The evidence is input to the tool, If a protocol satisfies declared properties, the toofs simply report this. If the protocol fails to satisfy the properties, the tools should provide informative output such as a trace or message sequence chart.