ISO/IEC 29128-1:2023

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

• Status: Published
• Publication Date: 19-Mar-2023
• ICS: 35.030 - IT Security
• 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: 6060 - International Standard published
• Start Date: 20-Mar-2023
• Due Date: 03-Jul-2023
• Completion Date: 20-Mar-2023

Relations

• Revises: ISO/IEC 29128:2011 - Information technology - Security techniques - Verification of cryptographic protocols
• Effective Date: 23-Apr-2020

Overview

ISO/IEC 29128-1:2023 - Information security, cybersecurity and privacy protection - Verification of cryptographic protocols - Part 1: Framework provides a standardized framework for the formal verification of cryptographic protocol specifications. It defines how protocol models, adversarial models and security properties should be described and assessed according to academic and industry best practices. This second edition updates the 2011 version (removing informal proofs, deprecating PAL levels and streamlining technical requirements) and is intended to support objective, repeatable verification for security‑critical systems.

Key topics and requirements

• Scope and intent
  • Establishes a verification framework for cryptographic protocol specifications (symbolic-model focused for standardization; computational and compositional approaches are reviewed).
• Protocol modelling
  • Defines a cryptographic protocol model as a formal specification + adversarial model + set of security properties.
  • Distinguishes between formal cryptographic protocol specifications (machine‑readable) and human‑readable protocol documents.
• Adversarial and security models
  • Requires explicit adversarial models (capabilities of attackers) and clearly defined security properties transcribed into machine‑readable form.
• Automated provers and tools
  • Verification is expected to use automated provers / model checkers that accept protocol models as input.
  • Tools must be based on a verifiable mathematical framework (soundness), be auditable (code/reviewable), and provide repeatable results.
• Verification process
  • Describes roles and duties of submitter and evaluator, expectations for self‑assessment evidence (proofs from provers), and evaluation of provers, models and evidence.
• Bounded vs unbounded verification
  • Discusses verification approaches and limits; emphasizes that verification results depend on model scope and tool capabilities.
• Informative annexes
  • Includes worked examples and reference models (e.g., Needham–Schroeder–Lowe, Dolev–Yao) to illustrate submissions and evaluations.

Applications and users

• Protocol designers who need rigorous verification to reduce design flaws.
• Security evaluators and certification bodies conducting independent protocol assessments.
• Implementers and architects of security‑critical systems seeking objective evidence of protocol properties.
• Tool developers and researchers advancing automated provers and formal methods.
• Standardization committees and procurement teams requiring consistent verification evidence.

Related standards

• Part of the ISO/IEC 29128 series on verification of cryptographic protocols. This framework is intended to be used alongside other parts of the series and relevant ISO/IEC information security standards.

Keywords: ISO/IEC 29128-1:2023, cryptographic protocol verification, formal verification, automated prover, symbolic model, adversarial model, security properties, verification framework.

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 2023
© 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: [phone]
Email: [e-mail]
Website: www.iso.org
Published in Switzerland
ii
© ISO/IEC 2023 – All rights reserved

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

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

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

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)
© ISO/IEC 2023 – All rights reserved

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
© ISO/IEC 2023 – All rights reserved

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.
© ISO/IEC 2023 – All rights reserved

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 ne
...