ISO/IEC 29128-2:2026

• Abstract:

  This document specifies an extension of evaluation methods and activities for cryptographic protocols based on ISO/IEC 15408-4, which provides a framework for evaluation methods and activities. This document provides a mapping between the work items for cryptographic protocol evaluation and the associated evaluation activities or evaluation methods. Additionally, this document also provides security assurance classification based on the cryptographic assessment performed by automated provers in four different levels of increasing assurance.

• Status: Published
• Publication Date: 31-Aug-2026
• 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 - Information security, cybersecurity and privacy protection
• Current Stage: 6060 - International Standard published
• Start Date: 01-Sep-2026
• Due Date: 03-Nov-2026
• Completion Date: 01-Sep-2026

Overview

ISO/IEC 29128-2:2026, "Information security, cybersecurity and privacy protection - Verification of cryptographic protocols - Part 2: Evaluation methods and activities for cryptographic protocols," extends established frameworks for evaluating cryptographic protocols. Based on ISO/IEC 15408-4, this standard provides detailed methodologies for the assessment of cryptographic protocols, supplying clear mappings between evaluation tasks, activities, and methods. It introduces a security assurance classification for cryptographic protocol evaluations performed with automated provers, structured into four distinct levels of increasing assurance.

This standard is crucial for organizations and professionals involved in designing, assessing, or certifying the security of digital communication protocols. It enables reliable, reproducible, and auditable verification processes in line with recognized cybersecurity and privacy protection best practices.

Key Topics

• Security Assessment of Protocols: Outlines a methodical approach to verifying and evaluating cryptographic protocols using formal models and automated tools.
• Automated Provers: Explains the role, assurance levels, and required capabilities of automated provers in cryptographic protocol evaluation.
• Assurance and Confidence Levels: Defines four assurance levels (PAL1–PAL4) and three confidence levels (PCL1–PCL3), establishing a scalable framework for classifying the robustness of evaluation results.
• Model Preparation and Submission: Details the process of creating, submitting, and validating protocol, adversarial, and security property models.
• Evaluation Methods and Activities: Specifies how evaluation activities are mapped to work units and security properties, ensuring systematic assessment and comprehensive reporting.
• Adversarial Models: Describes the incorporation of the Dolev-Yao and extension models for simulating adversarial behavior in different protocol scenarios.
• Tool Selection: Offers guidance in choosing appropriate formal verification tools for protocol validation based on maturity, acceptance, and documentation.

Applications

ISO/IEC 29128-2:2026 finds practical application in several key areas, supporting robust information security, cybersecurity, and privacy protection practices:

• Protocol Designers and Developers: Enables methodical verification of cryptographic protocols before deployment, reducing vulnerabilities and ensuring alignment with security requirements.
• Security Evaluators and Test Labs: Provides clear methodology for evaluating the correctness and assurance of protocol models, leveraging structured activities and evidence collection.
• Compliance and Certification: Facilitates adherence to security standards and regulatory frameworks by offering auditable processes and traceable rationale for each evaluation step.
• Tool Integrators and Users: Assists in the rational selection and validation of automated theorem provers or model checkers according to required assurance and confidence levels.
• Policy Makers and Auditors: Supports policy formulation and independent assessment of protocol security assurance claims.

These applications help streamline security assurance processes, enhance trust in cryptographic communications, and promote best-practice adoption across industries requiring secure digital exchanges.

Related Standards

• ISO/IEC 29128-1:2023 - Framework for verification of cryptographic protocols, providing definitions and foundational formal verification processes.
• ISO/IEC 29128-3 (forthcoming) - Evaluation methods and activities for concrete implementations of cryptographic protocols, aligned with vulnerability assessment frameworks.
• ISO/IEC 15408-4 - Establishes the general framework for specification and execution of evaluation methods and activities in IT security.
• ISO/IEC 18045 - Specifies the methodology for IT security evaluation.
• ISO/IEC 15408-5 - Defines pre-packaged security requirements aiding standardization in IT security evaluation.

Leveraging these related standards supports cohesive implementation, facilitating cross-referencing and alignment with internationally recognized best practices for cryptographic assurance and cybersecurity.

International
Standard
ISO/IEC 29128-2
First edition
Information security, cybersecurity
2026-09
and privacy protection —
Verification of cryptographic
protocols —
Part 2:
Evaluation methods and activities
for cryptographic protocols
Sécurité de l'information, cybersécurité et protection de la vie
privée — Vérification des protocoles cryptographiques —
Partie 2: Méthodes et activités d'évaluation pour les protocoles
cryptographiques
Reference number
© ISO/IEC 2026
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
© ISO/IEC 2026 – All rights reserved
ii
Contents Page
Foreword .iv
Introduction .v
1 Scope . 1
2 Normative references . 1
3 Terms and definitions . 1
4 Security assessment and verification of cryptographic protocols . 2
4.1 Overview .2
4.2 Prover .4
4.2.1 Prover assurance level .4
4.2.2 Prover confidence level .4
4.3 Models .4
4.3.1 Cryptographic protocol model .4
4.3.2 Adversarial model .5
4.3.3 Formal protocol specification.5
4.3.4 Security properties .6
5 Method for cryptographic protocol security evaluation . 6
5.1 Overview .6
5.2 Scope of cryptographic evaluation method .6
5.3 Cryptographic protocol evaluation method .7
5.3.1 General .7
5.3.2 Prover evaluation method .7
5.3.3 Model evaluation method .7
6 Activities for cryptographic protocol security evaluation . 8
Annex A (informative) List of tools for automated model verification .10
Annex B (informative) Evaluation of the prover .11
Annex C (informative) Extension model .12
Annex D (informative) Relationship between confidence levels with Implementation Assurance
Levels in ISO/IEC 29128-3 .13
Bibliography . 14

© ISO/IEC 2026 – All rights reserved
iii
Foreword
ISO (the International Organization for Standardization) and IEC (the International Electrotechnical
Commission) form the specialized system for worldwide standardization. National bodies that are
members of ISO or IEC participate in the development of International Standards through technical
committees established by the respective organization to deal with particular fields of technical activity.
ISO and IEC technical committees collaborate in fields of mutual interest. Other international organizations,
governmental and non-governmental, in liaison with ISO and IEC, also take part in the work.
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 document 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).
ISO and IEC draw attention to the possibility that the implementation of this document may involve the
use of (a) patent(s). ISO and IEC take no position concerning the evidence, validity or applicability of any
claimed patent rights in respect thereof. As of the date of publication of this document, ISO and IEC had not
received notice of (a) patent(s) which may be required to implement this document. However, implementers
are cautioned that this may not represent the latest information, which may be obtained from the patent
database available at www.iso.org/patents and https://patents.iec.ch. ISO and IEC shall not be held
responsible for identifying any or all such patent rights.
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 Technical Committee ISO/IEC/JTC 1, Information technology, Subcommittee
SC 27, Information security, cybersecurity and privacy protection.
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.

© ISO/IEC 2026 – All rights reserved
iv
Introduction
Cryptographic protocols form the basis of secure applications. A thorough evaluation is necessary to confirm
their expected behaviour before deployment.
The ISO/IEC 29128 series specifies methods for the verification and evaluation of cryptographic protocols.
ISO/IEC 29128-1 specifies the formal verification process and the evidence produced by this process.
This document (see ISO/IEC 29128-2) specifies the methodology and evaluation activities for collecting and
submitting the evidence from the formal verification process to the evaluator and the testing laboratory.
ISO/IEC 29128-3 specifies evaluation methods and activities for assessing a concrete implementation of a
cryptographic protocol. It provides an assurance framework based on vulnerability assessment principles
derived from the Common Criteria.

© ISO/IEC 2026 – All rights reserved
v
International Standard ISO/IEC 29128-2:2026(en)
Information security, cybersecurity and privacy protection —
Verification of cryptographic protocols —
Part 2:
Evaluation methods and activities for cryptographic protocols
1 Scope
This document specifies an extension of evaluation methods and activities for cryptographic protocols based
on ISO/IEC 15408-4, which provides a framework for evaluation methods and activities. This document
provides a mapping between the work items for cryptographic protocol evaluation and the associated
evaluation activities or evaluation methods. Additionally, this document also provides security assurance
classification based on the cryptographic assessment performed by automated provers in four different
levels of increasing assurance.
2 Normative references
The following documents are referred to in the text in such a way that some or all of their content constitutes
requirements of this document. For dated references, only the edition cited applies. For undated references,
the latest edition of the referenced document (including any amendments) applies.
ISO/IEC 29128-1:2023, Information security, cybersecurity and privacy protection — Verification of
cryptographic protocols — Part 1: Framework
3 Terms and definitions
For the purposes of this document, terms and definitions used in ISO/IEC 29128-1 and the following 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
prover assurance level
level of assurance of the prover output with regards to correctness
3.2
prover confidence level
level of confidence of the prover to verify the security properties with regards to strength of the adversary
3.3
evaluation method
set of one or more evaluation activities (3.4) for application in a cryptographic protocol evaluation context
3.4
evaluation activity
specific actions performed by an evaluator as defined in this document

© ISO/IEC 2026 – All rights reserved
3.5
message
communication unit of information exchange between parties in a cryptographic protocol
3.6
model verification
proof of correctness of security properties obtained after an evaluator successfully performs all evaluation
activities (3.4) for all security properties of the cryptographic protocol
3.7
rationale
evidence or reason for supporting the conformity to expected requirement(s)
3.8
automated prover
tool or set of tools used for evaluation of the security properties of a cryptographic protocol model
4 Security assessment and verification of cryptographic protocols
4.1 Overview
The security assessment and verification of cryptographic protocol performed by using an automated prover
is presented in Figure 1, also capturing the submitter’s responsibilities as specified in ISO/IEC 29128-1.

© ISO/IEC 2026 – All rights reserved
Key
1 model based on theoretical proof assurance level selection from Table 1
2 capabilities of prover based on theoretical proof assurance level selection from Table 1
Figure 1 — Cryptographic protocol validation framework providing an example model verification
using automated prover
Figure 1 does not indicate all the evaluator responsibilities which are detailed in this document but only
provides guidance to the automated prover’s validation rationale.
The process of security assessment and verification of cryptographic protocol is divided into three main
steps namely, model preparation, model submission and model validation. The model reparation steps
include the preparation of the cryptographic and the adversarial models which are described in detail in 4.3.
Next, the models along with other necessary information for evaluation based on the assurance level (see
Table 1) are passed to the automated prover in the model submission stage. Finally, in the model validation

© ISO/IEC 2026 – All rights reserved
stage, the automated prover attempts to run all the test cases to prove the security properties defined for
the cryptographic protocol utilizing the underlying adversarial model and provided initial information.
4.2 Prover
4.2.1 Prover assurance level
The prover assurance level of the automated prover are characterized as follows.
— Prover assurance level 1 (PAL1): The prover is evaluated using a methodology based on known-answer
tests for each security property. Annex B provides an example of the work performed by an evaluator
when evaluating the prover using known-answer tests methodology.
— Prover assurance level 2 (PAL2): The prover has undergone cross-validation by another prover along
with another adversarial model (similar models but different tool, or different models with the same
tool, or different tools with different models) validation testing (double blind validation).
— Prover assurance level 3 (PAL3): The prover has the capability to output a machine-checkable proof of
the correctness of the result. The output obtained from the prover was validated by a third-party tool
(independently developed).
— Prover assurance level 4 (PAL4): The prover underwent formal verification by a third-party tool
(independently developed).
The difference between PAL3 and PAL4 is that, at PAL4, each subfunction of the prover is formally verified,
whereas at PAL3 only the output is verified.
4.2.2 Prover confidence level
The prover confidence level of the automated prover are characterized as follows.
— Prover confidence level 1 (PCL1): The prover is capable of verifying security properties in the Dolev-Yao
model with all preliminary information and communication channel information (including public and
private) with bounded sessions.
— Prover confidence level 2 (PCL2): The prover is capable of verifying security properties in the Dolev-Yao
model with all preliminary information and communication channel information (including public and
private) with unbounded sessions.
— Prover confidence level 3 (PCL3): The prover is capable of verifying security properties in the Dolev-Yao
model with all preliminary information and communication channel information (including public and
private) with unbounded sessions and in the extension model, which consider cryptographic primitives
[6] [7]
(e.g. Goldwasser-Micali or Bana-Comon models ).
The relationship between Prover Confidence Level with AVA_VAN is described in the Annex D.
4.3 Models
4.3.1 Cryptographic protocol model
The automated prover processes a cryptographic protocol model that consists of the following models, as
defined in ISO/IEC 29128-1:2023, 4.3:
— the formal protocol specification, including the network information for the message exchanges between
the parties;
— the adversarial model with pre-defined power that includes information available at the beginning of the
evaluation, information about the honest agents in the network, public keys of honest agents, plaintext
identifiers, ability to craft hypothetical keys or nonces, and which are used in cryptographic operations
to intercept information;
© ISO/IEC 2026 – All rights reserved
— a model of the desired security properties that capture the intended security goals of the protocol.
4.3.2 Adversarial model
The adversarial model should have all capabilities of th
...