ISO/IEC 29128-1:2023
(Main)Information security, cybersecurity and privacy protection — Verification of cryptographic protocols — Part 1: Framework
Information security, cybersecurity and privacy protection — Verification of cryptographic protocols — Part 1: Framework
This document establishes a framework for the verification of cryptographic protocol specifications according to academic and industry best practices.
Titre manque — Partie 1: Titre manque
General Information
Relations
Buy Standard
Standards Content (Sample)
INTERNATIONAL ISO/IEC
STANDARD 29128-1
Second edition
2023-03
Information security, cybersecurity
and privacy protection — Verification
of cryptographic protocols —
Part 1:
Framework
Reference number
ISO/IEC 29128-1:2023(E)
© ISO/IEC 2023
---------------------- Page: 1 ----------------------
ISO/IEC 29128-1:2023(E)
COPYRIGHT PROTECTED DOCUMENT
© ISO/IEC 2023
All rights reserved. Unless otherwise specified, or required in the context of its implementation, no part of this publication may
be reproduced or utilized otherwise in any form or by any means, electronic or mechanical, including photocopying, or posting on
the internet or an intranet, without prior written permission. Permission can be requested from either ISO at the address below
or ISO’s member body in the country of the requester.
ISO copyright office
CP 401 • Ch. de Blandonnet 8
CH-1214 Vernier, Geneva
Phone: +41 22 749 01 11
Email: copyright@iso.org
Website: www.iso.org
Published in Switzerland
ii
© ISO/IEC 2023 – All rights reserved
---------------------- Page: 2 ----------------------
ISO/IEC 29128-1:2023(E)
Contents Page
Foreword .iv
Introduction .v
1 Scope . 1
2 Normative references . 1
3 Terms and definitions . 1
4 Formal verification of cryptographic protocols . 2
4.1 Methods for modelling cryptographic protocols . 2
4.2 Verification requirements . 3
4.2.1 Methods of verification . 3
4.2.2 Verification tools . 3
4.2.3 Bounded vs unbounded verification . 3
4.3 Cryptographic protocol model . 4
4.3.1 Description of a model . . 4
4.3.2 Formal specification . 4
4.3.3 Adversarial model . 5
4.3.4 Submitting a model . 5
4.3.5 Security properties . 5
4.3.6 Self-assessment evidence . . . 6
5 Verification process .6
5.1 General . 6
5.2 Duties of the submitter . 6
5.3 Duties of the evaluator . 6
5.3.1 Main duties . 6
5.3.2 Evaluating the prover . 6
5.3.3 Evaluating the model . 6
5.3.4 Evaluating the evidence . 7
5.3.5 Example evaluation . 7
Annex A (informative) The Needham-Schroeder-Lowe public key protocol .8
Annex B (informative) Example submission . 9
Annex C (informative) Example evaluation .10
Annex D (informative) Dolev-Yao model .11
Annex E (informative) Security properties .12
Bibliography .14
iii
© ISO/IEC 2023 – All rights reserved
---------------------- Page: 3 ----------------------
ISO/IEC 29128-1:2023(E)
Foreword
ISO (the International Organization for Standardization) is a worldwide federation of national standards
bodies (ISO member bodies). The work of preparing International Standards is normally carried out
through ISO technical committees. Each member body interested in a subject for which a technical
committee has been established has the right to be represented on that committee. International
organizations, governmental and non-governmental, in liaison with ISO, also take part in the work.
ISO collaborates closely with the International Electrotechnical Commission (IEC) on all matters of
electrotechnical standardization.
The procedures used to develop this document and those intended for its further maintenance
are described in the ISO/IEC Directives, Part 1. In particular, the different approval criteria
needed for the different types of ISO documents should be noted. This document was drafted in
accordance with the editorial rules of the ISO/IEC Directives, Part 2 (see www.iso.org/directives or
www.iec.ch/members_experts/refdocs).
Attention is drawn to the possibility that some of the elements of this document may be the subject of
patent rights. ISO shall not be held responsible for identifying any or all such patent rights. Details of
any patent rights identified during the development of the document will be in the Introduction and/
or on the ISO list of patent declarations received (see www.iso.org/patents) or the IEC list of patent
declarations received (see patents.iec.ch).
Any trade name used in this document is information given for the convenience of users and does not
constitute an endorsement.
For an explanation of the voluntary nature of standards, the meaning of ISO specific terms and
expressions related to conformity assessment, as well as information about ISO's adherence to
the World Trade Organization (WTO) principles in the Technical Barriers to Trade (TBT), see
www.iso.org/iso/foreword.html. In the IEC, see www.iec.ch/understanding-standards.
This document was prepared by Joint Technical Committee ISO/IEC JTC 1, Information Technology,
Subcommittee SC 27, Information security, cybersecurity and privacy protection.
This second edition cancels and replaces the first edition (ISO/IEC 29128:2011), which has been
technically revised.
The main changes are as follows:
— removal of informal and paper-and-pencil proofs;
— deprecation of PAL levels;
— streamlining of technical requirements and explanations;
— minor editorial changes to bring the document in line with the ISO/IEC Directives Part 2, 2021.
A list of all parts in the ISO/IEC 29128 series can be found on the ISO and IEC websites.
Any feedback or questions on this document should be directed to the user’s national standards
body. A complete listing of these bodies can be found at www.iso.org/members.html and
www.iec.ch/national-committees.
iv
© ISO/IEC 2023 – All rights reserved
---------------------- Page: 4 ----------------------
ISO/IEC 29128-1:2023(E)
Introduction
Many cryptographic protocols have failed to achieve their stated security goals because they are
complicated and difficult to design correctly in order to achieve the desired functional and security
requirements. This inherent difficulty means that protocols need to be rigorously analysed in order to
find errors in their design. The goal of this document is to standardize a method for analysing protocols
by proposing a clearly defined verification framework based on well-founded scientific methods.
This document proposes a standardization procedure analogous to what exists for cryptographic
algorithms. National and international bodies have evaluation processes that instil a high degree of
confidence that a standardized cryptographic algorithm meets the specific security requirements
it was designed for. A similar process for cryptographic protocols would provide confidence that a
verified protocol meets its stated security properties and can be used in security-critical systems.
The proposed verification process is based on state-of-the-art protocol modelling techniques using
rigorous logic, mathematics, and computer science. It is designed to provide objective evidence that
a protocol satisfies its stated security goals. Verification is not a guarantee of security; as with any
modelling, the results are constrained by the scope and quality of the model and tools used.
v
© ISO/IEC 2023 – All rights reserved
---------------------- Page: 5 ----------------------
INTERNATIONAL STANDARD ISO/IEC 29128-1:2023(E)
Information security, cybersecurity and privacy
protection — Verification of cryptographic protocols —
Part 1:
Framework
1 Scope
This document establishes a framework for the verification of cryptographic protocol specifications
according to academic and industry best practices.
2 Normative references
There are no normative references in this document.
3 Terms and definitions
For the purposes of this document, the following terms and definitions apply.
ISO and IEC maintain terminology databases for use in standardization at the following addresses:
— ISO Online browsing platform: available at https:// www .iso .org/ obp
— IEC Electropedia: available at https:// www .electropedia .org/
3.1
adversarial model
capabilities an adversary (3.2) has when attempting to attack a cryptographic protocol (3.4)
3.2
adversary
party attempting to disrupt the secure operation of a cryptographic protocol (3.4), with abilities defined
by the adversarial model (3.1)
3.3
automated prover
tool used for evaluating the security properties (3.9) of a cryptographic protocol model (3.5)
3.4
cryptographic protocol
communication protocol which uses cryptography to perform security-related functions
3.5
cryptographic protocol model
formal cryptographic protocol specification (3.8) combined with an adversarial model (3.1) and a set of
security properties (3.9)
3.6
cryptographic protocol specification
human-readable document which defines the functionality of a cryptographic protocol (3.4)
1
© ISO/IEC 2023 – All rights reserved
---------------------- Page: 6 ----------------------
ISO/IEC 29128-1:2023(E)
3.7
evaluator
party in the verification process defined by this document who evaluates a submitted protocol
3.8
formal cryptographic protocol specification
model of a cryptographic protocol specification (3.6) written in a machine-readable language
3.9
security property
security goal which a cryptographic protocol (3.4) is designed to guarantee, transcribed into a machine-
readable language
3.10
soundness
property of a mathematical system in which every statement that can be proved is true
3.11
self-assessment evidence
proofs of security properties (3.9) produced by an automated prover run on a cryptographic protocol
model (3.5)
3.12
submitter
party in the verification process defined by this document who submits a protocol for evaluation
4 Formal verification of cryptographic protocols
4.1 Methods for modelling cryptographic protocols
The goal of the formal verification of a cryptographic protocol is to obtain a formal proof that the
protocol, as defined in a protocol specification, meets its security properties and objectives within a
specified adversarial framework. Achieving this goal requires the construction of a protocol model.
There are two common paradigms for defining a protocol model - the symbolic model and the
[11]
computational model. The standardization process in this document considers only the symbolic
model, however both models are reviewed here for completeness.
In the symbolic model, aspects of cryptography are abstracted out of the model, so cryptographic
primitives are represented as black box functions and cryptography is assumed to be perfect. The
adversary is restricted to computations and algebraic operations that are part of the given primitives,
such as encrypting a message using a key, verifying a signature on a message, or computing the
Diffie-Hellman public value from a known private value. In particular, this means that if an adversary
knows some encrypted text, the only way they can learn the plain text from it is if they also possess
the relevant key. Abstracting away from purely cryptographic attacks allows for the construction of
a simple protocol model which is focused on the security of the protocol rather than the underlying
cryptography.
In the computational model, the cryptographic aspects are an integral part of the model. The method of
showing security in the protocol is to prove that attacking the protocol is at least as difficult as breaking
one of the hard problems that the cryptographic primitives are based on. The adversary may do any
computations on values they know, provided the computations run in polynomial time.
Automated tools for the computational model are limited and much less mature than for the symbolic
model. As such, proofs in the computational model are generally hand-written rather than automated.
Once tooling for computational models evolves, verification of protocols using those proofs can be
incorporated into this document.
Another paradigm for proving protocol security, known as composition, involves proving statements
about small parts of protocols and then combining those pieces together to prove statements about
2
© ISO/IEC 2023 – All rights reserved
---------------------- Page: 7 ----------------------
ISO/IEC 29128-1:2023(E)
the whole protocol. Universal composability is one major type of composability that has recently
been used to prove security properties of protocols that are used in practice. Automated provers for
composability are still in their infancy, but as they mature, verification of protocols using those proofs
can be incorporated into this document.
4.2 Verification requirements
4.2.1 Methods of verification
The state-of-the-art methodology for verifying the security properties of cryptographic protocols is
through the use of tools called automated provers. An automated prover takes in a description of a
protocol along with descriptions of security properties for that protocol. The prover then attempts
to either prove that, under certain assumptions, each security property holds or finds a sequence
of messages which allows an adversary to violate the security property. These inputs are part of a
cryptographic protocol model, which is defined fully in 5.3.
An automated prover may take advantage of computational power to verify complex security properties
by checking many cases and sub-cases without human intervention. It also produces repeatable
results which can be reviewed and verified by other parties. Automated provers require the protocol
specification to be written in a language that the tool is able to parse; in this document, this is termed a
formal specification.
4.2.2 Verification tools
Many automated provers currently exist for verifying security properties. In the future, new tools will
surely be developed, and it is always possible for errors and bugs to be found in tools. As such, this
document does not specify a list of eligible tools which can be used and instead specifies the properties
that a tool shall have.
The only tools which are eligible to be used for this standardization process are automated provers,
including model checkers, which are capable of accepting as input a cryptographic protocol model as
described in 4.3.
Automated provers are based on an underlying mathematical framework, which is the foundation on
which the proofs produced by the prover are based. In order to have confidence in the proof results, the
soundness of the framework shall be verified. Many provers have papers claiming to prove soundness,
which provide an excellent starting point for this verification.
Automated provers are software, and like all software the possibility of errors in the code exists. The
tool shall be auditable, such that anybody is able to review the code for the tool and its dependencies.
Lastly, the tool shall produce results which are repeatable. This means that anyone possessing the
inputs and a copy of the tool may reconstruct the results.
4.2.3 Bounded vs unbounded verification
Proofs taking advantage of automated tools can provide a particularly effective way to simplify the
formal verification process. Automatic provers obtain predictable results since their soundness and
completeness are already proven. Another important advantage of an automatic prover is the fact
that they can use available computational power to solve particularly complex security properties;
properties that would be out of reach of manual verification.
Tool-aided proofs require the specification of the cryptographic protocol to be written in a language
that the tool can execute; in this document this is termed a formal cryptographic protocol specification.
Two types of verification tools are recognized by this document: model checkers and theorem provers.
Confidence in a tool is not determined by its type but by whether it can handle unbounded sessions or
not.
3
© ISO/IEC 2023 – All rights reserved
---------------------- Page: 8 ----------------------
ISO/IEC 29128-1:2023(E)
Finally, verification tools can be fully automated (automatic) or require guidance from the developer
(semi-automatic).
4.3 Cryptographic protocol model
4.3.1 Description of a model
In order to create formal proofs of security properties, the construction of a cryptographic protocol
model is required. For the purposes of this document, such a model consists of:
— a formal cryptographic protocol specification based on the protocol specification;
— an adversarial model defining the adversary’s capabilities;
— a model of the desired security properties.
Annex A provides an example of a cryptographic protocol model.
Verification techniques are applied to the protocol model in an attempt to prove the correctness of
the security properties. For each desired security property, these techniques can result in a proof of
correctness for that security property, an attack that shows the protocol does not satisfy the desired
security property, or they can fail to find either a proof or an attack. Such proofs of correctness of
security properties will be referred to as self-assessment evidence.
4.3.2 Formal specification
Cryptographic protocol specifications are written in a way that humans can read and implement
them. In order to use such a specification for modelling, it shall be re-written in a computer-readable
language which can be interpreted by an automated prover. This new specification is called a formal
cryptographic protocol specification and shall encapsulate all relevant aspects of the protocol.
The formal specification shall model all the messages which can be sent by the parties involved in the
protocol. Typically, this is done by modelling the set of messages for each party as a separate role in the
protocol, or by modelling messages individually.
The formal specification shall model all of the functions which are used in constructing the messages
defined above. Common functions are often built into the automated prover, and any which are not
shall be included in the formal specification. These functions include cryptographic functions such
as encryption, signing and hashing, as well as non-cryptographic functions such as concatenation.
If the modelled protocols make use of Diffie-Hellman, this should include, for example, functions for
exponentiation and multiplication.
The formal specification shall model variables. Variables are used as inputs to and outputs of functions
and also as components of messages sent over the network.
The formal specification shall contain an algebraic structure which defines the mathematical rules
governing functions and variables. The structure defines the behaviour about how functions and
variables interact with each other, in order to model the way cryptographic operations interact with
each other.
EXAMPLE The functions for encrypting and decrypting a message m with a key k can be written as
enc(m,k) and dec(m,k)
with the relationship
dec(enc(m,k),k) = m
Typically, most or all of the algebraic structure is built into the automated prover. Any algebraic relations
which are needed for the protocol but not built into the prover shall be included as part of the model.
4
© ISO/IEC 2023 – All rights reserved
---------------------- Page: 9 ----------------------
ISO/IEC 29128-1:2023(E)
4.3.3 Adversarial model
4.3.3.1 General
The adversarial model constitutes the powers and abilities used by a hypothetical adversary to
compromise the system. It defines what information the adversary has access to and what actions they
are capable of taking. The starting point for most symbolic adversarial models is the Dolev-Yao model,
and using this model is required for protocol verification in this document. As this is the most common
model, it is also the model used by most automated provers. A brief description is provided in 4.3.3.3,
and a more detailed explanation can be found in Annex E.
4.3.3.2 Network specification
The network specification explains the network operating environment of the protocol. Typically, this
consists of a single public communication channel which is shared by all parties and which an adversary
has full control over. However, additional channels where the adversary has less control are also part of
some protocols and can be modelled by many tools.
4.3.3.3 Dolev-Yao model
The Dolev-Yao adversarial model defines three main types of abilities of an adversary.
The adversary has full control of the public portions of the network. They are able to read all messages
sent over the network, send their own messages over the network and delete messages preventing them
from being seen by others on the network. Messages sent over the network by the adversary will be of
a type defined in the formal specification. Full network control is, in many cases, an unrealistically
strong threat model, however all modern protocols are designed to withstand attack from adversaries
with this capability.
The adversary can know and retain information. Any values they see on the network and any values
they are able to compute can be stored indefinitely for later use.
The adversary can perform computations. The formal specification defines algebraic operations and
functions which are part of the protocol being studied. An adversary may use all of these operations
and functions with any of the information it has. This allows the adversary to learn new information
derived from existing information.
EXAMPLE If an adversary is in possession of an encrypted message and the key that is needed to decrypt the
message, then the adversary can learn the message.
Annex D provides more information on the Dolev-Yao model.
4.3.4 Submitting a model
If the automated prover does not have an embedded Dolev-Yao model, then a specification for the
adversarial model shall be included as part of the protocol specification. If no adversarial model is
submitted, it is assumed that the embedded Dolev-Yao adversarial model is being used.
It is possible to grant additional powers to an adversary to obtain a stronger proof of security. Granting
additional powers is permitted in this document and such powers are defined as part of the adversarial
model. Any such powers defined include a plain language description of the powers.
4.3.5 Security properties
Security properties define the security goals of a cryptographic protocol, such as authentication of a
party or secrecy of a transmitted message. In the protocol model, security properties are statements
about the formal specification, written in the same language, which the automated prover will attempt
to verify.
5
© ISO/IEC 2023 – All rights reserved
---------------------- Page: 10 ----------------------
ISO/IEC 29128-1:2023(E)
4.3.6 Self-assessment evidence
After constructing the cryptographic protocol model, the model is run through the automated prover.
The self-assessment evidence is the collection of proofs of security properties this process generates.
5 Verification process
5.1 General
This clause defines the process that shall be undertaken to complete a verification of a candidate
protocol. There are two separate parties involved in the process: the submitter and the evaluator. The
submitter is the party who creates a cryptographic protocol model for the protocol they wish to verify.
The submitter would likely be a protocol designer or someone who wishes to use a protocol, but anybody
can be a submitter. The evaluator is the party that verifies the self-assessment evidence produced from
the cryptographic protocol. The evaluator shall be someone with the technical expertise to conduct the
verification process defined in 5.3 and shall be independent from the submitter.
5.2 Duties of the submitter
The submitter shall provide the following to the evaluator:
— the cryptographic protocol specification which defines the protocol to be evaluated;
— the cryptographic protocol model produced based on the specification (as defined in 4.3);
— the self-assessment evidence produced by the automated prover (as defined in 4.3.6);
— the name and version number of the automated prover used to produce the self-assessment evidence;
— a copy of, or access to, the automated prover, if it is not readily available to the evaluator;
— a list of the claimed security properties written in plain language;
— a list of additional powers granted to the adversary written in plain language, if applicable.
Annex B provides an example of a protocol submission for evaluation.
5.3 Duties of the evaluator
5.3.1 Main duties
The evaluator is responsible for evaluating all material provided by the submitter. This consists of:
— evaluating the automated prover used to produce the self-assessment evidence;
— evaluating the cryptographic protocol model created by the submitter;
— evaluating the self-assessment evidence provided by the submitter.
5.3.2 Evaluating the prover
The evaluator shall evaluate the suitability of the prover being used. The evaluator shall examine the
prover and verify that it meets all of the criteria defined in 4.2.2.
5.3.3 Evaluating the model
The evaluator shall verify that all aspects of the submitted model as defined in 4.3.2 are correct.
6
© ISO/IEC 2023 – Al
...
ISO/IEC 29128-1:20222023(E)
2022-07-20
2023-01-10
ISO/IEC JTC 1/SC 27/WG 3
Secretariat: XXXXDIN
Information security, cybersecurity and privacy protection — Verification of
cryptographic protocols — Part 1: Framework
---------------------- Page: 1 ----------------------
© ISO 2022 – All rights reserved
© ISO 2022 2023
All rights reserved. Unless otherwise specified, or required in the context of its implementation,
no part of this publication may be reproduced or utilized otherwise in any form or by any means,
electronic or mechanical, including photocopying, or posting on the internet or an intranet,
without prior written permission. Permission can be requested from either ISO at the address
below or ISO's member body in the country of the requester.
ISO Copyright Office
CP 401 • CH-1214 Vernier, Geneva
Phone: + 41 22 749 01 11
Email: copyright@iso.org
Website: www.iso.org
Published in Switzerland.
© ISO/IEC 2021 – All rights reserved ii-3
---------------------- Page: 2 ----------------------
ISO/IEC 29128-1:20212023(E)
Contents
Foreword . v
Introduction . vi
1 Scope . 2
2 Normative references . 2
3 Terms and definitions . 2
4 Formal Verification of Cryptographic Protocols . 3
4.1 Methods for Modelling Cryptographic Protocols . 3
4.2 Verification Requirements . 4
4.2.1 Methods of Verification . 4
4.2.2 Verification Tools . 4
4.2.3 Bounded vs Unbounded Verification . 4
4.3 Cryptographic Protocol Model . 5
4.3.1 Description of a Model. 5
4.3.2 Formal Specification . 5
4.3.3 Adversarial Model . 6
4.3.4 Security Properties . 6
4.3.5 Self-Assessment Evidence . 7
5 Verification Process . 7
5.1 General . 7
5.2 Duties of the Submitter . 7
5.3 Duties of the Evaluator . 7
5.3.1 Main Duties . 7
5.3.2 Evaluating the Prover . 7
5.3.3 Evaluating the Model . 7
5.3.4 Evaluating the Evidence . 8
5.3.5 Example Evaluation . 8
Annex A (informative) The Needham-Schroeder-Lowe public key protocol . 9
A.1 Protocol Specification . 9
A.2 Protocol Model . 9
Annex B (informative) Example Submission . 13
B.1 General . 13
B.2 Protocol Specification . 13
B.3 Protocol Model . 13
B.4 Self-Assessment Evidence . 13
B.5 Automated Prover . 13
B.6 Security Properties . 13
© ISO/IEC 2022 – All rights reservediv iv© ISO/IEC 2023 – All rights reserved
---------------------- Page: 3 ----------------------
ISO/IEC 29128-1:20222023(E)
Annex C (informative) Example Evaluation . 14
C.1 General . 14
C.2 Evaluation . 14
C.2.1 Evaluating the prover . 14
C.2.2 Evaluating the model . 14
C.2.3 Evaluating the evidence . 14
Annex D (informative) Dolev-Yao model . 15
Annex E (informative) Security Properties . 16
E.1 Secrecy . 16
E.2 Perfect Forward Secrecy . 16
E.3 Strong Secrecy . 16
E.4 Integrity . 16
E.5 Authentication . 16
E.5.1 General . 16
E.5.2 Aliveness . 16
E.5.3 Injective Agreement . 17
Bibliography . 17
v© ISO/IEC 2023 – All rights reserved © ISO/IEC 2021 – All rights reservedv
---------------------- Page: 4 ----------------------
ISO/IEC 29128-1:20212023(E)
Foreword
ISO (the International Organization for Standardization) is a worldwide federation of national
standards bodies (ISO member bodies). The work of preparing International Standards is normally
carried out through ISO technical committees. Each member body interested in a subject for which a
technical committee has been established has the right to be represented on that committee.
International organizations, governmental and non-governmental, in liaison with ISO, also take part in
the work. ISO collaborates closely with the International Electrotechnical Commission (IEC) on all
matters of electrotechnical standardization.
The procedures used to develop this document and those intended for its further maintenance are
described in the ISO/IEC Directives, Part 1. In particular, the different approval criteria needed for the
different types of ISO documents should be noted. This document was drafted in accordance with the
editorial rules of the ISO/IEC Directives, Part 2 (see www.iso.org/directiveswww.iso.org/directives or
www.iec.ch/members_experts/refdocs).
Attention is drawn to the possibility that some of the elements of this document may be the subject of
patent rights. ISO shall not be held responsible for identifying any or all such patent rights. Details of
any patent rights identified during the development of the document will be in the Introduction and/or
on the ISO list of patent declarations received (see www.iso.org/patentswww.iso.org/patents) or the
IEC list of patent declarations received (see patents.iec.ch).
Any trade name used in this document is information given for the convenience of users and does not
constitute an endorsement.
For an explanation of the voluntary nature of standards, the meaning of ISO specific terms and
expressions related to conformity assessment, as well as information about ISO's adherence to the
World Trade Organization (WTO) principles in the Technical Barriers to Trade (TBT), see
www.iso.org/iso/foreword.html. In the IEC, see www.iec.ch/understanding-standards.
This document was prepared by Joint Technical Committee ISO/IEC JTC 1, Information Technology,
Subcommittee SC 27, Information security, cybersecurity and privacy protection.
This second edition cancels and replaces the first edition (ISO/IEC 29128:2011), which has been
technically revised.
The main changes are as follows:
— removal of informal and paper-and-pencil proofs;
— deprecation of PAL levels;
— streamlining of technical requirements and explanations;
— minor editorial changes to bring the document in line with the ISO/IEC Directives Part 2, 2021.
A list of all parts in the ISO/IEC 29128 series can be found on the ISO and IEC websites.
Any feedback or questions on this document should be directed to the user’s national standards body. A
complete listing of these bodies can be found at
www.iso.org/members.htmlwww.iso.org/members.html and www.iec.ch/national-committees.
© ISO/IEC 2022 – All rights reservedvi vi© ISO/IEC 2023 – All rights reserved
---------------------- Page: 5 ----------------------
ISO/IEC 29128-1:20222023(E)
Introduction
Many cryptographic protocols have failed to achieve their stated security goals because they are
complicated and difficult to design correctly in order to achieve the desired functional and security
requirements. This inherent difficulty means that protocols need to be rigorously analysed in order to
find errors in their design. The goal of this document is to standardize a method for analysing protocols
by proposing a clearly defined verification framework based on well-founded scientific methods.
This document proposes a standardization procedure analogous to what exists for cryptographic
algorithms. National and international bodies have evaluation processes that instil a high degree of
confidence that a standardized cryptographic algorithm meets the specific security requirements it was
designed for. A similar process for cryptographic protocols would provide confidence that a verified
protocol meets its stated security properties and can be used in security-critical systems.
The proposed verification process is based on state-of-the-art protocol modelling techniques using
rigorous logic, mathematics, and computer science. It is designed to provide objective evidence that a
protocol satisfies its stated security goals. Verification is not a guarantee of security; as with any
modelling, the results are constrained by the scope and quality of the model and tools used.
vii© ISO/IEC 2023 – All rights reserved © ISO/IEC 2021 – All rights reservedvii
---------------------- Page: 6 ----------------------
ISO/IEC 29128:2021(E)
INTERNATIONAL STANDARD ISO/IEC 29128-1:2023(E)
Information security, cybersecurity and privacy protection —
Verification of cryptographic protocols — Part 1: Framework
1 Scope
This document establishes a framework for the verification of cryptographic protocol specifications
according to academic and industry best practices.
2 Normative references
There are no normative references in this document.
3 Terms and definitions
For the purposes of this document, the following terms and definitions apply.
ISO and IEC maintain terminology databases for use in standardization at the following addresses:
— ISO Online browsing platform: available at https://www.iso.org/obp
— IEC Electropedia: available at https://www.electropedia.org/
3.1
adversarial model
capabilities an adversary (3.2) has when attempting to attack a cryptographic protocol (3.4)
3.2
adversary
party attempting to disrupt the secure operation of a cryptographic protocol (3.4), with abilities defined
by the adversarial model (3.1)
3.3
automated prover
tool used for evaluating the security properties (3.9) of a cryptographic protocol model (3.5)
3.4
cryptographic protocol
communication protocol which uses cryptography to perform security-related functions
3.5
cryptographic protocol model
formal cryptographic protocol specification (3.6) combined with an adversarial model (3.1) and a set of
security properties (3.9)
3.6
© ISO/IEC 2023 – All rights reserved 1
---------------------- Page: 7 ----------------------
ISO/IEC 29128-1:2023(E)
cryptographic protocol specification
human-readable document which defines the functionality of a cryptographic protocol (3.4)
3.7
evaluator
party in the verification process defined by this document who evaluates a submitted protocol
3.8
formal cryptographic protocol specification
model of a cryptographic protocol specification (3.6) written in a machine-readable language
3.9
security property
security goal which a cryptographic protocol (3.4) is designed to guarantee, transcribed into a machine-
readable language
3.10
soundness
property of a mathematical system in which every statement that can be proved is true
3.11
self-assessment evidence
proofs of security properties (3.9) produced by an automated prover run on a cryptographic protocol
model (3.5)
3.12
submitter
party in the verification process defined by this document who submits a protocol for evaluation
4 Formal verification of cryptographic protocols
4.1 Methods for modelling cryptographic protocols
The goal of the formal verification of a cryptographic protocol is to obtain a formal proof that the
protocol, as defined in a protocol specification, meets its security properties and objectives within a
specified adversarial framework. Achieving this goal requires the construction of a protocol model.
There are two common paradigms for defining a protocol model - the symbolic model and the
[11]
computational model . The standardization process in this document considers only the symbolic
model, however both models are reviewed here for completeness.
In the symbolic model, aspects of cryptography are abstracted out of the model, so cryptographic
primitives are represented as black box functions and cryptography is assumed to be perfect. The
adversary is restricted to computations and algebraic operations that are part of the given primitives,
such as encrypting a message using a key, verifying a signature on a message, or computing the Diffie-
Hellman public value from a known private value. In particular, this means that if an adversary knows
some encrypted text, the only way they can learn the plain text from it is if they also possess the
relevant key. Abstracting away from purely cryptographic attacks allows for the construction of a
simple protocol model which is focused on the security of the protocol rather than the underlying
cryptography.
In the computational model, the cryptographic aspects are an integral part of the model. The method of
showing security in the protocol is to prove that attacking the protocol is at least as difficult as breaking
one of the hard problems that the cryptographic primitives are based on. The adversary may do any
computations on values they know, provided the computations run in polynomial time.
2 © ISO/IEC 2023 – All rights reserved
---------------------- Page: 8 ----------------------
ISO/IEC 29128-1:2023(E)
Automated tools for the computational model are limited and much less mature than for the symbolic
model. As such, proofs in the computational model are generally hand-written rather than automated.
Once tooling for computational models evolves, verification of protocols using those proofs can be
incorporated into this document.
Another paradigm for proving protocol security, known as composition, involves proving statements
about small parts of protocols and then combining those pieces together to prove statements about the
whole protocol. Universal composability is one major type of composability that has recently been used
to prove security properties of protocols that are used in practice. Automated provers for composability
are still in their infancy, but as they mature, verification of protocols using those proofs can be
incorporated into this document.
4.2 Verification requirements
4.2.1 Methods of verification
The state-of-the-art methodology for verifying the security properties of cryptographic protocols is
through the use of tools called automated provers. An automated prover takes in a description of a
protocol along with descriptions of security properties for that protocol. The prover then attempts to
either prove that, under certain assumptions, each security property holds or findfinds a sequence of
messages which allows an adversary to violate the security property. These inputs are part of a
cryptographic protocol model, which is defined fully in 5.3.
An automated prover may take advantage of computational power to verify complex security
properties by checking many cases and sub-cases without human intervention. It also produces
repeatable results which can be reviewed and verified by other parties. Automated provers require the
protocol specification to be written in a language that the tool is able to parse; in this document, this is
termed a formal specification.
4.2.2 Verification tools
Many automated provers currently exist for verifying security properties. In the future, new tools will
surely be developed, and it is always possible for errors and bugs to be found in tools. As such, this
document does not specify a list of eligible tools which can be used and instead specifies the properties
that a tool shall have.
The only tools which are eligible to be used for this standardization process are automated provers,
including model checkers, which are capable of accepting as input a cryptographic protocol model as
described in 4.3.
Automated provers are based on an underlying mathematical framework, which is the foundation on
which the proofs produced by the prover are based. In order to have confidence in the proof results, the
soundness of the framework shall be verified. Many provers have papers claiming to prove soundness,
which provide an excellent starting point for this verification.
Automated provers are software, and like all software the possibility of errors in the code exists. The
tool shall be auditable, such that anybody is able to review the code for the tool and its dependencies.
Lastly, the tool shall produce results which are repeatable. This means that anyone possessing the
inputs and a copy of the tool may reconstruct the results.
4.2.3 Bounded vs unbounded verification
Proofs taking advantage of automated tools can provide a particularly effective way to simplify the
formal verification process. Automatic provers obtain predictable results since their soundness and
completeness are already proven. Another important advantage of an automatic prover is the fact that
they can use available computational power to solve particularly complex security properties;
properties that would be out of reach of manual verification.
© ISO/IEC 2023 – All rights reserved 3
---------------------- Page: 9 ----------------------
ISO/IEC 29128-1:2023(E)
Tool-aided proofs require the specification of the cryptographic protocol to be written in a language
that the tool can execute; in this document this is termed a formal cryptographic protocol specification.
Two types of verification tools are recognized by this document: model checkers and theorem provers.
Confidence in a tool is not determined by its type but by whether it can handle unbounded sessions or
not.
Finally, verification tools maycan be fully automated (automatic) or require guidance from the
developer (semi-automatic).
4.3 Cryptographic Protocol Modelprotocol model
4.3.1 Description of a model
In order to create formal proofs of security properties, the construction of a cryptographic protocol
model is required. For the purposes of this document, such a model consists of:
— a formal cryptographic protocol specification based on the protocol specification;
— an adversarial model defining the adversary’s capabilities;
— a model of the desired security properties.
Annex A provides an example of a cryptographic protocol model.
Verification techniques are applied to the protocol model in an attempt to prove the correctness of the
security properties. For each desired security property, these techniques can result in a proof of
correctness for that security property, an attack that shows the protocol does not satisfy the desired
security property, or they maycan fail to find either a proof or an attack. Such proofs of correctness of
security properties will be referred to as self-assessment evidence.
4.3.2 Formal specification
Cryptographic protocol specifications are written in a way that humans can read and implement them.
In order to use such a specification for modelling, it shall be re-written in a computer-readable language
which can be interpreted by an automated prover. This new specification is called a formal
cryptographic protocol specification and shall encapsulate all relevant aspects of the protocol.
The formal specification shall model all the messages which can be sent by the parties involved in the
protocol. Typically, this is done by modelling the set of messages for each party as a separate role in the
protocol, or by modelling messages individually.
The formal specification shall model all of the functions which are used in constructing the messages
defined above. Common functions are often built into the automated prover, and any which are not shall
be included in the formal specification. These functions include cryptographic functions such as
encryption, signing, and hashing, as well as non-cryptographic functions such as concatenation. If the
modelled protocols make use of Diffie-Hellman, this should include, for example, functions for
exponentiation and multiplication.
The formal specification shall model variables. Variables are used as inputs to and outputs of functions
and also as components of messages sent over the network.
The formal specification shall contain an algebraic structure which defines the mathematical rules
governing functions and variables. The structure defines the behaviour about how functions and
variables interact with each other, in order to model the way cryptographic operations interact with
each other.
EXAMPLE The functions for encrypting and decrypting a message m with a key k can be written as
enc(m,k) and dec(m,k)
4 © ISO/IEC 2023 – All rights reserved
---------------------- Page: 10 ----------------------
ISO/IEC 29128-1:2023(E)
with the relationship
dec(enc(m,k),k) = m
Typically, most or all of the algebraic structure is built into the automated prover. Any algebraic
relations which are needed for the protocol but not built into the prover shall be included as part of the
model.
4.3.3 Adversarial model
4.3.3.1 General
The adversarial model constitutes the powers and abilities used by a hypothetical adversary to
compromise the system. It defines what information the adversary has access to and what actions they
are capable of taking. The starting point for most symbolic adversarial models is the Dolev-Yao model,
and using this model is required for protocol verification in this document. As this is the most common
model, it is also the model used by most automated provers. A brief description is provided in 4.3.3.3,
and a more detailed explanation can be found in Annex E.
4.3.3.2 Network specification
The network specification explains the network operating environment of the protocol. Typically, this
consists of a single public communication channel which is shared by all parties and which an adversary
has full control over. However, additional channels where the adversary has less control are also part of
some protocols and can be modelled by many tools.
4.3.3.3 Dolev-Yao model
The Dolev-Yao adversarial model defines three main types of abilities of an adversary.
The adversary has full control of the public portions of the network. They are able to read all messages
sent over the network, send their own messages over the network, and delete messages preventing
them from being seen by others on the network. Messages sent over the network by the adversary will
be of a type defined in the formal specification. Full network control is, in many cases, an unrealistically
strong threat model, however all modern protocols are designed to withstand attack from adversaries
with this capability.
The adversary maycan know and retain information. Any values they see on the network and any values
they are able to compute can be stored indefinitely for later use.
The adversary maycan perform computations. The formal specification defines algebraic operations
and functions which are part of the protocol being studied. An adversary may use all of these operations
and functions with any of the information it has. This allows the adversary to learn new information
derived from existing information.
EXAMPLE If an adversary is in possession of an encrypted message and the key that is needed to decrypt the
message, then the adversary can learn the message.
Annex D provides more information on the Dolev-Yao model.
4.3.4 Submitting a Modelmodel
If the automated prover does not have an embedded Dolev-Yao model, then a specification for the
adversarial model shall be included as part of the protocol specification. If no adversarial model is
submitted, it is assumed that
...
INTERNATIONAL ISO/IEC
STANDARD 29128-1
Second edition
Information security, cybersecurity
and privacy protection — Verification
of cryptographic protocols —
Part 1:
Framework
PROOF/ÉPREUVE
Reference number
ISO/IEC 29128-1:2023(E)
© ISO/IEC 2023
---------------------- Page: 1 ----------------------
ISO/IEC 29128-1:2023(E)
COPYRIGHT PROTECTED DOCUMENT
© ISO/IEC 2023
All rights reserved. Unless otherwise specified, or required in the context of its implementation, no part of this publication may
be reproduced or utilized otherwise in any form or by any means, electronic or mechanical, including photocopying, or posting on
the internet or an intranet, without prior written permission. Permission can be requested from either ISO at the address below
or ISO’s member body in the country of the requester.
ISO copyright office
CP 401 • Ch. de Blandonnet 8
CH-1214 Vernier, Geneva
Phone: +41 22 749 01 11
Email: copyright@iso.org
Website: www.iso.org
Published in Switzerland
ii
PROOF/ÉPREUVE © ISO/IEC 2023 – All rights reserved
---------------------- Page: 2 ----------------------
ISO/IEC 29128-1:2023(E)
Contents Page
Foreword .iv
Introduction .v
1 Scope . 1
2 Normative references . 1
3 Terms and definitions . 1
4 Formal verification of cryptographic protocols . 2
4.1 Methods for modelling cryptographic protocols . 2
4.2 Verification requirements . 3
4.2.1 Methods of verification . 3
4.2.2 Verification tools . 3
4.2.3 Bounded vs unbounded verification . 3
4.3 Cryptographic protocol model . 4
4.3.1 Description of a model . . 4
4.3.2 Formal specification . 4
4.3.3 Adversarial model . 5
4.3.4 Submitting a model . 5
4.3.5 Security properties . 5
4.3.6 Self-assessment evidence . . . 6
5 Verification process .6
5.1 General . 6
5.2 Duties of the submitter . 6
5.3 Duties of the evaluator . 6
5.3.1 Main duties . 6
5.3.2 Evaluating the prover . 6
5.3.3 Evaluating the model . 6
5.3.4 Evaluating the evidence . 7
5.3.5 Example evaluation . 7
Annex A (informative) The Needham-Schroeder-Lowe public key protocol .8
Annex B (informative) Example submission . 9
Annex C (informative) Example evaluation.10
Annex D (informative) Dolev-Yao model .11
Annex E (informative) Security Properties .12
Bibliography .14
iii
© ISO/IEC 2023 – All rights reserved PROOF/ÉPREUVE
---------------------- Page: 3 ----------------------
ISO/IEC 29128-1:2023(E)
Foreword
ISO (the International Organization for Standardization) is a worldwide federation of national standards
bodies (ISO member bodies). The work of preparing International Standards is normally carried out
through ISO technical committees. Each member body interested in a subject for which a technical
committee has been established has the right to be represented on that committee. International
organizations, governmental and non-governmental, in liaison with ISO, also take part in the work.
ISO collaborates closely with the International Electrotechnical Commission (IEC) on all matters of
electrotechnical standardization.
The procedures used to develop this document and those intended for its further maintenance
are described in the ISO/IEC Directives, Part 1. In particular, the different approval criteria
needed for the different types of ISO documents should be noted. This document was drafted in
accordance with the editorial rules of the ISO/IEC Directives, Part 2 (see www.iso.org/directives or
www.iec.ch/members_experts/refdocs).
Attention is drawn to the possibility that some of the elements of this document may be the subject of
patent rights. ISO shall not be held responsible for identifying any or all such patent rights. Details of
any patent rights identified during the development of the document will be in the Introduction and/
or on the ISO list of patent declarations received (see www.iso.org/patents) or the IEC list of patent
declarations received (see patents.iec.ch).
Any trade name used in this document is information given for the convenience of users and does not
constitute an endorsement.
For an explanation of the voluntary nature of standards, the meaning of ISO specific terms and
expressions related to conformity assessment, as well as information about ISO's adherence to
the World Trade Organization (WTO) principles in the Technical Barriers to Trade (TBT), see
www.iso.org/iso/foreword.html. In the IEC, see www.iec.ch/understanding-standards.
This document was prepared by Joint Technical Committee ISO/IEC JTC 1, Information Technology,
Subcommittee SC 27, Information security, cybersecurity and privacy protection.
This second edition cancels and replaces the first edition (ISO/IEC 29128:2011), which has been
technically revised.
The main changes are as follows:
— removal of informal and paper-and-pencil proofs;
— deprecation of PAL levels;
— streamlining of technical requirements and explanations;
— minor editorial changes to bring the document in line with the ISO/IEC Directives Part 2, 2021.
A list of all parts in the ISO/IEC 29128 series can be found on the ISO and IEC websites.
Any feedback or questions on this document should be directed to the user’s national standards
body. A complete listing of these bodies can be found at www.iso.org/members.html and
www.iec.ch/national-committees.
iv
PROOF/ÉPREUVE © ISO/IEC 2023 – All rights reserved
---------------------- Page: 4 ----------------------
ISO/IEC 29128-1:2023(E)
Introduction
Many cryptographic protocols have failed to achieve their stated security goals because they are
complicated and difficult to design correctly in order to achieve the desired functional and security
requirements. This inherent difficulty means that protocols need to be rigorously analysed in order to
find errors in their design. The goal of this document is to standardize a method for analysing protocols
by proposing a clearly defined verification framework based on well-founded scientific methods.
This document proposes a standardization procedure analogous to what exists for cryptographic
algorithms. National and international bodies have evaluation processes that instil a high degree of
confidence that a standardized cryptographic algorithm meets the specific security requirements
it was designed for. A similar process for cryptographic protocols would provide confidence that a
verified protocol meets its stated security properties and can be used in security-critical systems.
The proposed verification process is based on state-of-the-art protocol modelling techniques using
rigorous logic, mathematics, and computer science. It is designed to provide objective evidence that
a protocol satisfies its stated security goals. Verification is not a guarantee of security; as with any
modelling, the results are constrained by the scope and quality of the model and tools used.
v
© ISO/IEC 2023 – All rights reserved PROOF/ÉPREUVE
---------------------- Page: 5 ----------------------
INTERNATIONAL STANDARD ISO/IEC 29128-1:2023(E)
Information security, cybersecurity and privacy
protection — Verification of cryptographic protocols —
Part 1:
Framework
1 Scope
This document establishes a framework for the verification of cryptographic protocol specifications
according to academic and industry best practices.
2 Normative references
There are no normative references in this document.
3 Terms and definitions
For the purposes of this document, the following terms and definitions apply.
ISO and IEC maintain terminology databases for use in standardization at the following addresses:
— ISO Online browsing platform: available at https:// www .iso .org/ obp
— IEC Electropedia: available at https:// www .electropedia .org/
3.1
adversarial model
capabilities an adversary (3.2) has when attempting to attack a cryptographic protocol (3.4)
3.2
adversary
party attempting to disrupt the secure operation of a cryptographic protocol (3.4), with abilities defined
by the adversarial model (3.1)
3.3
automated prover
tool used for evaluating the security properties (3.9) of a cryptographic protocol model (3.5)
3.4
cryptographic protocol
communication protocol which uses cryptography to perform security-related functions
3.5
cryptographic protocol model
formal cryptographic protocol specification (3.6) combined with an adversarial model (3.1) and a set of
security properties (3.9)
3.6
cryptographic protocol specification
human-readable document which defines the functionality of a cryptographic protocol (3.4)
1
© ISO/IEC 2023 – All rights reserved PROOF/ÉPREUVE
---------------------- Page: 6 ----------------------
ISO/IEC 29128-1:2023(E)
3.7
evaluator
party in the verification process defined by this document who evaluates a submitted protocol
3.8
formal cryptographic protocol specification
model of a cryptographic protocol specification (3.6) written in a machine-readable language
3.9
security property
security goal which a cryptographic protocol (3.4) is designed to guarantee, transcribed into a machine-
readable language
3.10
soundness
property of a mathematical system in which every statement that can be proved is true
3.11
self-assessment evidence
proofs of security properties (3.9) produced by an automated prover run on a cryptographic protocol
model (3.5)
3.12
submitter
party in the verification process defined by this document who submits a protocol for evaluation
4 Formal verification of cryptographic protocols
4.1 Methods for modelling cryptographic protocols
The goal of the formal verification of a cryptographic protocol is to obtain a formal proof that the
protocol, as defined in a protocol specification, meets its security properties and objectives within a
specified adversarial framework. Achieving this goal requires the construction of a protocol model.
There are two common paradigms for defining a protocol model - the symbolic model and the
[11]
computational model . The standardization process in this document considers only the symbolic
model, however both models are reviewed here for completeness.
In the symbolic model, aspects of cryptography are abstracted out of the model, so cryptographic
primitives are represented as black box functions and cryptography is assumed to be perfect. The
adversary is restricted to computations and algebraic operations that are part of the given primitives,
such as encrypting a message using a key, verifying a signature on a message, or computing the
Diffie-Hellman public value from a known private value. In particular, this means that if an adversary
knows some encrypted text, the only way they can learn the plain text from it is if they also possess
the relevant key. Abstracting away from purely cryptographic attacks allows for the construction of
a simple protocol model which is focused on the security of the protocol rather than the underlying
cryptography.
In the computational model, the cryptographic aspects are an integral part of the model. The method of
showing security in the protocol is to prove that attacking the protocol is at least as difficult as breaking
one of the hard problems that the cryptographic primitives are based on. The adversary may do any
computations on values they know, provided the computations run in polynomial time.
Automated tools for the computational model are limited and much less mature than for the symbolic
model. As such, proofs in the computational model are generally hand-written rather than automated.
Once tooling for computational models evolves, verification of protocols using those proofs can be
incorporated into this document.
Another paradigm for proving protocol security, known as composition, involves proving statements
about small parts of protocols and then combining those pieces together to prove statements about
2
PROOF/ÉPREUVE © ISO/IEC 2023 – All rights reserved
---------------------- Page: 7 ----------------------
ISO/IEC 29128-1:2023(E)
the whole protocol. Universal composability is one major type of composability that has recently
been used to prove security properties of protocols that are used in practice. Automated provers for
composability are still in their infancy, but as they mature, verification of protocols using those proofs
can be incorporated into this document.
4.2 Verification requirements
4.2.1 Methods of verification
The state-of-the-art methodology for verifying the security properties of cryptographic protocols is
through the use of tools called automated provers. An automated prover takes in a description of a
protocol along with descriptions of security properties for that protocol. The prover then attempts
to either prove that, under certain assumptions, each security property holds or finds a sequence
of messages which allows an adversary to violate the security property. These inputs are part of a
cryptographic protocol model, which is defined fully in 5.3.
An automated prover may take advantage of computational power to verify complex security properties
by checking many cases and sub-cases without human intervention. It also produces repeatable
results which can be reviewed and verified by other parties. Automated provers require the protocol
specification to be written in a language that the tool is able to parse; in this document, this is termed a
formal specification.
4.2.2 Verification tools
Many automated provers currently exist for verifying security properties. In the future, new tools will
surely be developed, and it is always possible for errors and bugs to be found in tools. As such, this
document does not specify a list of eligible tools which can be used and instead specifies the properties
that a tool shall have.
The only tools which are eligible to be used for this standardization process are automated provers,
including model checkers, which are capable of accepting as input a cryptographic protocol model as
described in 4.3.
Automated provers are based on an underlying mathematical framework, which is the foundation on
which the proofs produced by the prover are based. In order to have confidence in the proof results, the
soundness of the framework shall be verified. Many provers have papers claiming to prove soundness,
which provide an excellent starting point for this verification.
Automated provers are software, and like all software the possibility of errors in the code exists. The
tool shall be auditable, such that anybody is able to review the code for the tool and its dependencies.
Lastly, the tool shall produce results which are repeatable. This means that anyone possessing the
inputs and a copy of the tool may reconstruct the results.
4.2.3 Bounded vs unbounded verification
Proofs taking advantage of automated tools can provide a particularly effective way to simplify the
formal verification process. Automatic provers obtain predictable results since their soundness and
completeness are already proven. Another important advantage of an automatic prover is the fact
that they can use available computational power to solve particularly complex security properties;
properties that would be out of reach of manual verification.
Tool-aided proofs require the specification of the cryptographic protocol to be written in a language
that the tool can execute; in this document this is termed a formal cryptographic protocol specification.
Two types of verification tools are recognized by this document: model checkers and theorem provers.
Confidence in a tool is not determined by its type but by whether it can handle unbounded sessions or
not.
3
© ISO/IEC 2023 – All rights reserved PROOF/ÉPREUVE
---------------------- Page: 8 ----------------------
ISO/IEC 29128-1:2023(E)
Finally, verification tools can be fully automated (automatic) or require guidance from the developer
(semi-automatic).
4.3 Cryptographic protocol model
4.3.1 Description of a model
In order to create formal proofs of security properties, the construction of a cryptographic protocol
model is required. For the purposes of this document, such a model consists of:
— a formal cryptographic protocol specification based on the protocol specification;
— an adversarial model defining the adversary’s capabilities;
— a model of the desired security properties.
Annex A provides an example of a cryptographic protocol model.
Verification techniques are applied to the protocol model in an attempt to prove the correctness of
the security properties. For each desired security property, these techniques can result in a proof of
correctness for that security property, an attack that shows the protocol does not satisfy the desired
security property, or they can fail to find either a proof or an attack. Such proofs of correctness of
security properties will be referred to as self-assessment evidence.
4.3.2 Formal specification
Cryptographic protocol specifications are written in a way that humans can read and implement
them. In order to use such a specification for modelling, it shall be re-written in a computer-readable
language which can be interpreted by an automated prover. This new specification is called a formal
cryptographic protocol specification and shall encapsulate all relevant aspects of the protocol.
The formal specification shall model all the messages which can be sent by the parties involved in the
protocol. Typically, this is done by modelling the set of messages for each party as a separate role in the
protocol, or by modelling messages individually.
The formal specification shall model all of the functions which are used in constructing the messages
defined above. Common functions are often built into the automated prover, and any which are not
shall be included in the formal specification. These functions include cryptographic functions such
as encryption, signing and hashing, as well as non-cryptographic functions such as concatenation.
If the modelled protocols make use of Diffie-Hellman, this should include, for example, functions for
exponentiation and multiplication.
The formal specification shall model variables. Variables are used as inputs to and outputs of functions
and also as components of messages sent over the network.
The formal specification shall contain an algebraic structure which defines the mathematical rules
governing functions and variables. The structure defines the behaviour about how functions and
variables interact with each other, in order to model the way cryptographic operations interact with
each other.
EXAMPLE The functions for encrypting and decrypting a message m with a key k can be written as
enc(m,k) and dec(m,k)
with the relationship
dec(enc(m,k),k) = m
Typically, most or all of the algebraic structure is built into the automated prover. Any algebraic relations
which are needed for the protocol but not built into the prover shall be included as part of the model.
4
PROOF/ÉPREUVE © ISO/IEC 2023 – All rights reserved
---------------------- Page: 9 ----------------------
ISO/IEC 29128-1:2023(E)
4.3.3 Adversarial model
4.3.3.1 General
The adversarial model constitutes the powers and abilities used by a hypothetical adversary to
compromise the system. It defines what information the adversary has access to and what actions they
are capable of taking. The starting point for most symbolic adversarial models is the Dolev-Yao model,
and using this model is required for protocol verification in this document. As this is the most common
model, it is also the model used by most automated provers. A brief description is provided in 4.3.3.3,
and a more detailed explanation can be found in Annex E.
4.3.3.2 Network specification
The network specification explains the network operating environment of the protocol. Typically, this
consists of a single public communication channel which is shared by all parties and which an adversary
has full control over. However, additional channels where the adversary has less control are also part of
some protocols and can be modelled by many tools.
4.3.3.3 Dolev-Yao model
The Dolev-Yao adversarial model defines three main types of abilities of an adversary.
The adversary has full control of the public portions of the network. They are able to read all messages
sent over the network, send their own messages over the network and delete messages preventing them
from being seen by others on the network. Messages sent over the network by the adversary will be of
a type defined in the formal specification. Full network control is, in many cases, an unrealistically
strong threat model, however all modern protocols are designed to withstand attack from adversaries
with this capability.
The adversary can know and retain information. Any values they see on the network and any values
they are able to compute can be stored indefinitely for later use.
The adversary can perform computations. The formal specification defines algebraic operations and
functions which are part of the protocol being studied. An adversary may use all of these operations
and functions with any of the information it has. This allows the adversary to learn new information
derived from existing information.
EXAMPLE If an adversary is in possession of an encrypted message and the key that is needed to decrypt the
message, then the adversary can learn the message.
Annex D provides more information on the Dolev-Yao model.
4.3.4 Submitting a model
If the automated prover does not have an embedded Dolev-Yao model, then a specification for the
adversarial model shall be included as part of the protocol specification. If no adversarial model is
submitted, it is assumed that the embedded Dolev-Yao adversarial model is being used.
It is possible to grant additional powers to an adversary to obtain a stronger proof of security. Granting
additional powers is permitted in this document and such powers are defined as part of the adversarial
model. Any such powers defined include a plain language description of the powers.
4.3.5 Security properties
Security properties define the security goals of a cryptographic protocol, such as authentication of a
party or secrecy of a transmitted message. In the protocol model, security properties are statements
about the formal specification, written in the same language, which the automated prover will attempt
to verify.
5
© ISO/IEC 2023 – All rights reserved PROOF/ÉPREUVE
---------------------- Page: 10 ----------------------
ISO/IEC 29128-1:2023(E)
4.3.6 Self-assessment evidence
After constructing the cryptographic protocol model, the model is run through the automated prover.
The self-assessment evidence is the collection of proofs of security properties this process generates.
5 Verification process
5.1 General
This clause defines the process that shall be undertaken to complete a verification of a candidate
protocol. There are two separate parties involved in the process: the submitter and the evaluator. The
submitter is the party who creates a cryptographic protocol model for the protocol they wish to verify.
The submitter would likely be a protocol designer or someone who wishes to use a protocol, but anybody
can be a submitter. The evaluator is the party that verifies the self-assessment evidence produced from
the cryptographic protocol. The evaluator shall be someone with the technical expertise to conduct the
verification process defined in 5.3 and shall be independent from the submitter.
5.2 Duties of the submitter
The submitter shall provide the following to the evaluator:
— the cryptographic protocol specification which defines the protocol to be evaluated;
— the cryptographic protocol model produced based on the specification (as defined in 4.3);
— the self-assessment evidence produced by the automated prover (as defined in 4.3.6);
— the name and version number of the automated prover used to produce the self-assessment evidence;
— a copy of, or access to, the automated prover, if it is not readily available to the evaluator;
— a list of the claimed security properties written in plain language;
— a list of additional powers granted to the adversary written in plain language, if applicable.
Annex B provides an example of a protocol submission for evaluation.
5.3 Duties of the evaluator
5.3.1 Main duties
The evaluator is responsible for evaluating all material provided by the submitter. This consists of:
— evaluating the automated prover used to produce the self-assessment evidence;
— evaluating the cryptographic protocol model created by the submitter;
— evaluating the self-assessment evidence provided by the submitter.
5.3.2 Evaluating the prover
The evaluator shall evaluate the suitability of the prover being used. The evaluator shall examine the
prover and verify that it meets all of the criteria defined in 4.2.2.
5.3.3 Evaluating the mode
...
Questions, Comments and Discussion
Ask us and Technical Secretary will try to provide an answer. You can facilitate discussion about the standard in here.