ISO/IEC 29128:2011

Information technology — Security techniques — Verification of cryptographic protocols

ISO/IEC 29128:2011 establishes a technical base for the security proof of the specification of cryptographic protocols. It specifies design evaluation criteria for these protocols, as well as methods to be applied in a verification process for such protocols. It also provides definitions of different protocol assurance levels consistent with evaluation assurance components in ISO/IEC 15408.

Technologies de l'information — Techniques de sécurité — Vérification des protocoles cryptographiques

General Information

• Status: Withdrawn
• Publication Date: 06-Dec-2011
• ICS: 35.030 - IT Security
• ICS: 35.040 - Information coding
• Technical Committee: ISO/IEC JTC 1/SC 27 - Information security, cybersecurity and privacy protection
• Drafting Committee: ISO/IEC JTC 1/SC 27/WG 3 - Security evaluation, testing and specification
• Current Stage: 9092 - International Standard to be revised
• Completion Date: 03-Jul-2019

Relations

• Revised: ISO/IEC 29128-1:2023 - Information security, cybersecurity and privacy protection — Verification of cryptographic protocols — Part 1: Framework
• Effective Date: 23-Apr-2020

Standards Content (Sample)

INTERNATIONAL ISO/IEC
STANDARD 29128
First edition
2011-12-15


Information technology — Security
techniques — Verification of
cryptographic protocols
Technologies de l'information — Techniques de sécurité — Vérification
des protocoles cryptographiques




Reference number
ISO/IEC 29128:2011(E)
©
ISO/IEC 2011

---------------------- Page: 1 ----------------------
ISO/IEC 29128:2011(E)

COPYRIGHT PROTECTED DOCUMENT


©  ISO/IEC 2011
All rights reserved. Unless otherwise specified, no part of this publication may be reproduced or utilized in any form or by any means,
electronic or mechanical, including photocopying and microfilm, without permission in writing from either ISO at the address below or
ISO's member body in the country of the requester.
ISO copyright office
Case postale 56  CH-1211 Geneva 20
Tel. + 41 22 749 01 11
Fax + 41 22 749 09 47
E-mail [e-mail]
Web www.iso.org
Published in Switzerland

ii © ISO/IEC 2011 – All rights reserved

---------------------- Page: 2 ----------------------
ISO/IEC 29128:2011(E)

Contents Page
Foreword . v
Introduction . vi
1 Scope . 1
2 Terms and definitions . 1
3 Symbols and notation. . 2
4 General . 3
5 Specifying cryptographic protocols . 5
5.1 Objectives . 5
5.2 The abstraction levels . 5
5.3 The specification of security protocols . 5
5.3.1 General . 5
5.3.2 The symbolic messages . 5
5.3.3 Observing messages . 6
5.3.4 Algebraic properties . 7
5.3.5 Protocol roles . 7
5.4 The specification of adversarial model . 8
5.4.1 Network specification . 8
5.4.2 The attacker . 8
5.4.3 The scenario . 9
5.5 The specification of security properties . 10
5.5.1 General . 10
5.5.2 Trace properties . 11
6 Cryptographic protocol assurance levels . 12
6.1 General . 12
6.2 Protocol Assurance Level 1 . 13
6.3 Protocol Assurance Level 2 . 13
6.4 Protocol Assurance Level 3 . 14
6.5 Protocol Assurance Level 4 . 14
6.6 Difference among Protocol Assurance Levels . 14
6.7 Corresponding assurance levels in ISO/IEC 15408 . 15
7 Security Assessment and Verification . 16
7.1 Protocol specification . 16
7.1.1 PPS_SEMIFORMAL . 16
7.1.2 PPS_FORMAL . 17
7.1.3 PPS_MECHANIZED . 17
7.2 Adversarial model . 18
7.2.1 PAM INFORMAL . 18
7.2.2 PAM_FORMAL . 18
7.2.3 PAM_MECHANIZED . 19
7.3 Security properties . 20
7.3.1 General . 20
7.3.2 PSP_INFORMAL . 21
7.3.3 PSP_FORMAL . 21
7.3.4 PSP_MECHANIZED . 22
7.4 Self-assessment evidence for verification. 23
7.4.1 General . 23
7.4.2 PEV_ARGUMENT . 23
7.4.3 PEV_HANDPROVEN . 23
7.4.4 PEV_BOUNDED . 24
7.4.5 PEV_UNBOUNDED .24
© ISO/IEC 2011 – All rights reserved iii

---------------------- Page: 3 ----------------------
ISO/IEC 29128:2011(E)
8 Common Methodology for Cryptographic Protocols Security Evaluation . 25
8.1 Introduction . 25
8.2 Protocol specification evaluation . 26
8.2.1 Evaluation of sub-activity (PPS_SEMIFORMAL) . 26
8.2.2 Evaluation of sub-activity (PPS_FORMAL) . 26
8.2.3 Evaluation of sub-activity (PPS_MECHANIZED) . 26
8.3 Adversarial model evaluation . 27
8.3.1 Evaluation of sub-activity (PAM INFORMAL) . 27
8.3.2 Evaluation of sub-activity (PAM_FORMAL) . 27
8.3.3 Evaluation of sub-activity (PAM_MECHANIZED) . 28
8.4 Security properties evaluation . 28
8.4.1 Evaluation of sub-activity (PSP_INFORMAL) . 28
8.4.2 Evaluation of sub-activity (PSP_FORMAL) . 28
8.4.3 Evaluation of sub-activity (PSP_MECHANIZED) . 29
8.5 Self-assessment evidence evaluation . 29
8.5.1 Evaluation of sub-activity (PEV_ARGUMENT) . 29
8.5.2 Evaluation of sub-activity (PEV_HANDPROVEN) . 30
8.5.3 Evaluation of sub-activity (PEV_BOUNDED) . 30
8.5.4 Evaluation of sub-activity (PEV_UNBOUNDED) . 30
Annex A (informative) Guidelines for Cryptographic Protocol Design . 32
Annex B (informative) Example of formal specification . 34
B.1 Symbolic specification of security protocols . 34
B.1.1 Abstraction level . 34
B.1.2 Protocol specifications . 35
B.2 State transitions . 37
B.2.1 Attacker model . 37
B.2.2 Configuration state . 37
B.2.3 Traces . 38
B.3 Trace properties . 38
B.3.1 Secrecy . 38
B.3.2 Authentication . 39
Annex C (informative) Verification examples . 41
C.1 Sample protocol . 41
C.2 Design artifacts . 41
C.2.1 Input to protocol verification tool . 42
C.2.2 Protocol Specification . 43
C.2.3 Operating Environment . 44
C.2.4 Security Properties . 44
C.2.5 Evidence . 44
C.3 Additional inputs for verification . 47
Bibliography . 49

iv © ISO/IEC 2011 – All rights reserved

---------------------- Page: 4 ----------------------
ISO/IEC 29128:2011(E)
Foreword
ISO (the International Organization for Standardization) and IEC (the International Electrotechnical
Commission) form the specialized system for worldwide standardization. National bodies that are members of
ISO or IEC participate in the development of International Standards through technical committees
established by the respective organization to deal with particular fields of technical activity. ISO and IEC
technical committees collaborate in fields of mutual interest. Other international organizations, governmental
and non-governmental, in liaison with ISO and IEC, also take part in the work. In the field of information
technology, ISO and IEC have established a joint technical committee, ISO/IEC JTC 1.
International Standards are drafted in accordance with the rules given in the ISO/IEC Directives, Part 2.
The main task of the joint technical committee is to prepare International Standards. Draft International
Standards adopted by the joint technical committee are circulated to national bodies for voting. Publication as
an International Standard requires approval by at least 75 % of the national bodies casting a vote.
Attention is drawn to the possibility that some of the elements of this document may be the subject of patent
rights. ISO and IEC shall not be held responsible for identifying any or all such patent rights.
ISO/IEC 29128 was prepared by -RLQWTechnical Committee ISO/IEC JTC 1, Information Wechnology,
Subcommittee SC 27, ,7Security Wechniques.
v
© ISO/IEC 2011 – All rights reserved

---------------------- Page: 5 ----------------------
ISO/IEC 29128:2011(E)
Introduction
The security of digital communications is dependHnt on a number of aspects, where cryptographic
mechanisms play an increasingly important role. When such mechanisms are being used, there are a number
of security concerns such as the strength of the cryptographic algorithms, the accuracy and correctness of the
implementation, the correct operation and use of cryptographic systems, and the security of the deployed
cryptographic protocols.
Standards already exist for the specification of cryptographic algorithms, and for the implementation and test
of cryptographic devices and modules. However, there are no standards or generally accepted processes for
the assessment of the specification of protocols used in such communication. The goal of this International
Standard is to establish means for verification of cryptographic protocol specifications to provide defined levels
of confidence concerning the security of the specification of cryptographic protocols.
vi
© ISO/IEC 2011 – All rights reserved

---------------------- Page: 6 ----------------------
INTERNATIONAL STANDARD     ISO/IEC 29128:2011(E)

Information technology — Security techniques — Verification of
cryptographic protocols
1 Scope
This International Standard establishes a technical base for the security proof of the specification of
cryptographic protocols. This International Standard specifies design evaluation criteria for these protocols, as
well as methods to be applied in a verification process for such protocols. This International Standard also
provides definitions of different protocol assurance levels consistent with evaluation assurance components in
ISO/IEC 15408.
2 Terms and definitions
For the purposes of this document, the following terms and definitions apply.
2.1
arity
number of arguments
2.2
cryptographic protocol
protocol which performs a security-related function using cryptography
2.3
formal methods
techniques based on well-established mathematical concepts for modelling, calculation, and predication used
in the specification, design, analysis, construction, and assurance of hardware and software systems
2.4
formal description
description whose syntax and semantics are defined on the basis of well-established mathematical concepts
2.5
formal language
language for modelling, calculation, and predication in the specification, design, analysis, construction, and
assurance of hardware and software systems whose syntax and semantics are defined on the basis of well-
established mathematical concepts
1
© ISO/IEC 2011 – All rights reserved

---------------------- Page: 7 ----------------------
ISO/IEC 29128:2011(E)
2.6
adversarial model
description of the powers of adversaries who can try to defeat the protocol
NOTE It includes restriction on available resources, ability of adversaries, etc.
2.7
security property
formally or informally defined property which a cryptographic protocol is designed to assure such as secrecy,
authenticity, or anonymity
2.8
self-assessment evidence
evidence that the developer uses to verify whether a specified protocol fulfils its designated security properties
NOTE It includes cryptographic protocol specification, adversarial model and output (transcripts) of formal verification
tool.
2.9
protocol model
specification of a protocol and its behaviour with respect to an adversarial model
2.10
protocol specification
all formal and informal descriptions of a specified protocol
NOTE It includes all processes by each protocol participant, all communications between them and their order
2.11
secrecy
security property for a cryptographic protocol stating that a message or data should not be learned by
unauthorized entities
2.12
variadic
property of a function whose arity is variable
3 Symbols and QRWDWLRQ
For the purposes of this document, the following symbols and notation apply.
 security property of a protocol model
2
© ISO/IEC 2011 – All rights reserved

---------------------- Page: 8 ----------------------
ISO/IEC 29128:2011(E)
A,B role names
m message
r random nonce
k key
c communication channel
enc encryption function
dec decryption function
<.,…> paring operator
Send sending process
Receive receiving process
4 General
Verification of a cryptographic protocol involves checking the following artifacts:
a) specification of the cryptographic protocol;
b) specification of the adversarial model;
c) specification of the security objectives and properties;
d) self-assessment evidence that the specification of the cryptographic protocol in its adversarial model
achieves and satisfies its objectives and properties.
The artifacts shall clearly state parameters or properties relevant for the verification. Examples include the
bound used in bounded verification as later descibed in Clause7.4.4.1 or assumed algebraic properties of
cryptographic operators used in the protocol as described in Clause7.1.2.3 and Clause5.3.4.
The different Protocol Assurance Levels will lead to different requirements for these four artifacts. The stated
requirements are only for design verification not implementation verification.
NOTE 1 For verifying an implementation, additional assurance requirements should be supplied and satisfied.
This International Standard does not specify precisely what proof methods or tools shall be used, but instead
only specifes their properties. This encourages protocol designers to use the state-of-the-art for protocol
verification in terms of models, methods, and tools.
3
© ISO/IEC 2011 – All rights reserved

---------------------- Page: 9 ----------------------
ISO/IEC 29128:2011(E)
Verification tools shall fulfil the following conditions.
a) The verification tools are sound.
The protocol designer or possibly an independent third party shall provide evidence of the correctness of the
verification tool used. This may, for example, be in terms of a pencil-and-paper proof of the soundness of the
calculus used or, in some cases, in terms of code inspection to see that the tool properly implements the
calculus.
NOTE 2 This step is nontrivial, yet it is essential if machine checked proofs are to provide greater confidence than hand
proofs. In theory, this can be done once and for all for a verification tool, although in practice, tools evolve over time.
b) The results of verification tools are documented in such a way that they are repeatable.
The protocol designer shall provide adequate documentation, including all inputs needed for the tool to
construct a proof or (in the case of decision procedures) determine provability.
c) The verification tools are available for outside evaluation and use.
The protocol designer shall indicate all necessary tools to independently check the proofs.
NOTE 3 At least in theory, protocol verification canbe carried out by hand proofs, using paper and pencil. However, given
the substantial amount of detail typically involved in security protocol verification, especially for the high Protocol
Assurance Levels, confidence in the results is substantially increased by using mechanized tools such as model checkers
and theorem provers. Thus, proofs only with paper-and-pencil are treated as lower assurance level (i.e. PAL2) than
mechanized proof in this International Standard.
4
© ISO/IEC 2011 – All rights reserved

---------------------- Page: 10 ----------------------
ISO/IEC 29128:2011(E)
5 Specifying cryptographic protocols
5.1 Objectives
The goal of this part is to provide guidelines and minimal requirements for specifying cryptographic protocols.
5.2 The abstraction levels
The protocols can be specified at several levels of abstraction, each corresponding to a computation model.
At the most abstract level, messages are terms constructed from symbols and the attacker is also modelled as
a formal process. We will call this abstraction the symbolic level. In such a model, the resources (both time
and space resources) are not considered.
Any other model can be defined as a refinement of a symbolic model. For instance we can interpret the
symbols used in the symbolic model as functions on bitstrings, that can be computed in polynomial time.
Therefore, any cryptographic protocol consists in a symbolic specification and an interpretation in a given
domain (e.g. bitstrings or structured data, or even material-dependent formats) of all the symbols, together
with assumptions on their interpretation. Such hypotheses can ensure some correspondence between the
properties at various abstraction levels.
NOTE In this International Standard, we only consider the symbolic specification of security protocols.
Further documents are required for the specification of other (lower) abstraction levels. Typically, it will be
necessary to explain how to specify the interpretation domain and how to carry security guarantees across
levels of abstraction.
5.3 The specification of security protocols
5.3.1 General
As explained, a symbolic specification is the necessary first part towards the full specification of a protocol.
We list below the minimal mandatory parts in a symbolic protocol specification.
5.3.2 The symbolic messages
The first part consists in specifying what are the possible (valid) messages.
In this clause, the cryptographic primitives used in the protocol must be listed. Since we are talking about a
symbolic specification, this part consists of providing with
1. a set of function symbols 𝓕
Each function symbol has either a fixed arity, that has to be specified, or it is variadic (in which case it
has also to be specified).
© ISO/IEC 2011 – All rights reserved
5

---------------------- Page: 11 ----------------------
ISO/IEC 29128:2011(E)
2. a set of name symbols 𝓝 that may be split into various syntactic categories that have to be specified.
3. a set of variable symbols 𝓧.
4. a formal description of valid rules allowing to build messages using the function symbols.
A (non exhaustive) list of possible ways to specify such a language is:
 Nothing: all terms that are built with the function symbols and following the arity restrictions are valid
messages
 Some arguments are restricted to names: some of the arguments of function symbols are restricted
to belong to some name categories
 Sorts: a type discipline is defined and only well-typed terms correspond to messages.
The set of valid terms (or messages) is written (𝓕, 𝓝) (or (𝓕, 𝓝, 𝓧) when variables are involved)
EXAMPLE A typical example is encryption, that can be modeled by a symbol enc, whose arity is 2 or 3 (or 4),
depending on whether the random seed is explicit or not (and whether the encryption algorithm is explicit or not). A
specification has to make precise what is the arity of enc and what are the assumed types of its arguments. Typically, enc
has an arity 3. As possible name categories there are the random seeds, whose symbols will start with 𝑟, the keys, whose
symbols will start with 𝑘, the algorithms, whose symbols will start with  , and so on. If enc has been specified as being an
arity 3 symbol, we can additionally restrict its arguments, specifying for instance that the first argument must be a key and
the last one must be a random. In that case, enc(𝑘, 𝑘, 𝑟), enc(𝑘, enc(𝑘, 𝑟 , 𝑟 ), 𝑟 ), are valid terms while enc(enc(𝑘, 𝑘 ,
1 2 1
𝑟), 𝑘 , 𝑟 ) and enc(𝑟, 𝑘, 𝑟 )are not valid terms. Examples of symbols that can be considered as variadicinclude the
exclusive or ⊕, the arithmetic multiplication × or the concatenation ‖.
5.3.3 Observing messages
This part consists of specifying some comparison predicates between messages.
Only the equality predicate is mandatory, since other predicates could be seen as Boolean functions and
specified within the equality definition. It might however be useful to distinguish later between the computation
abilities and the observation abilities. Moreover, in many current specification languages, properties of the
function symbols are specified equationally (see clause 5.3.4), while it might be impossible to specify
equationally the observation abilities.
This part consists in listing predicate symbols, together with their arity. Typical examples include typing
predicates, equality, and same_length (that checks that its two arguments have the same length),
same_key (that checks whether two ciphertexts are encrypted with the same key).
6
© ISO/IEC 2011 – All rights reserved

---------------------- Page: 12 ----------------------
ISO/IEC 29128:2011(E)
5.3.4 Algebraic properties
This part specifies when two valid terms represent the same message and, more generally, what are the
interpretations of the predicate symbols listed in the previous clause.
For instance, when function symbols include both (symmetric) encryption and decryption, we might wish to
state that dec(𝑘, enc(𝑘, 𝑥, 𝑟))= 𝑥 where 𝑟 is a symbol for a random seed to express probabilistic encryption:
these are two term representations of the same message. We might also wish to state that, 𝑥 ⨁ 𝑥 = 0 if we are
using a symbol ⨁ meant to represent exclusive or.
As usual, we assume that any two terms that are not specified to be equal are different. The same rule applies
to the predicates: everything that has not been specified to be true is, by default, false.

5.3.5 Protocol roles
...