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

ISO/IEC 29128-2:2026 is an International Standard from ISO for evaluating cryptographic protocols. It specifies evaluation methods and activities for cryptographic protocols, extends the evaluation-method framework in ISO/IEC 15408-4, and gives a four-level security assurance classification for assessments performed by automated provers. It is aimed at evaluators, submitters, and testing laboratories that need to assess protocol models before deployment.

What does ISO/IEC 29128-2:2026 specify?

ISO/IEC 29128-2:2026 specifies how cryptographic protocol evaluation work is mapped to evaluation activities or evaluation methods, and how automated prover assessments are classified into four increasing assurance levels. In practice, it tells the evaluator how to organize the model, what evidence to request, and how to relate each security property to specific work units.

The document is organized into six clauses:

• Scope
• Normative references
• Terms and definitions
• Security assessment and verification of cryptographic protocols
• Method for cryptographic protocol security evaluation
• Activities for cryptographic protocol security evaluation

Annex	What it covers
Annex A	Tools for automated model verification
Annex B	Evaluation of the prover
Annex C	Extension model
Annex D	Relationship between confidence levels with Implementation Assurance Levels in ISO/IEC 29128-3

What are the key requirements of ISO/IEC 29128-2:2026?

ISO/IEC 29128-2:2026 centers on a staged evaluation process, defined prover assurance and confidence levels, and a documented mapping from security properties to work units and rationale. The practical result is that an evaluation must be traceable from the protocol model all the way to the prover output and the report.

Model preparation, submission, and validation

Clause 4 describes three main steps: model preparation, model submission, and model validation. The evaluator first checks the cryptographic and adversarial models, then receives the protocol model and supporting information, then validates the prover against the stated security properties. This matters because the evidence is not just the model itself - it also includes how the model was prepared and tested.

Prover assurance levels

Clause 4.2.1 defines four prover assurance levels, PAL1 to PAL4. PAL1 uses known-answer tests, PAL2 uses cross-validation with another prover and another adversarial model, PAL3 requires a machine-checkable proof of correctness of the result, and PAL4 requires formal verification of the prover by a third-party tool. In practice, this classifies how much trust can be placed in the prover output.

Prover confidence levels

Clause 4.2.2 defines three prover confidence levels, PCL1 to PCL3. These levels distinguish bounded and unbounded sessions in the Dolev-Yao model, and PCL3 extends that to an extension model with cryptographic primitives. For readers, this tells you how strong the adversarial model is before the protocol is considered verified.

What the protocol model must contain

Clause 4.3 says the cryptographic protocol model includes the formal protocol specification, the adversarial model, and the security properties. The model must identify the parties, the message exchanges, the functions used, the algebraic structures, and the corruption status of parties. That is important because the automated prover can only verify what is formally stated.

Evaluation method and work units

Clause 5 maps each security property to one or more work units, and each work unit needs its own evaluation activities and rationale. The submission must include the formal specification, the security properties, the parties, the complete set of messages, and the network assumptions, including which channels are eavesdroppable or fully accessible. This gives the evaluator a clear audit trail for each property.

Evaluation activities

Clause 6 requires the evaluator to check that the prover capability matches the selected confidence level, that the validation report matches the selected assurance level, and that all work units are covered. Findings must be reported. In practice, this is the part that turns the model and prover results into documented evidence.

What terms does ISO/IEC 29128-2:2026 define?

• Prover assurance level (PAL) - the level of assurance of the prover output with regard to correctness.
• Prover confidence level (PCL) - the level of confidence that the prover can verify security properties against a given adversary strength.
• Evaluation method - a set of one or more evaluation activities used in a cryptographic protocol evaluation context.
• Evaluation activity - a specific action performed by an evaluator under this document.
• Automated prover - a tool or set of tools used to evaluate security properties of a cryptographic protocol model.
• Model verification - the proof of correctness of security properties after all required evaluation activities have been successfully performed.
• Rationale - the evidence or reason supporting conformity to expected requirements.
• Message - a communication unit exchanged between parties in a cryptographic protocol.

Who uses ISO/IEC 29128-2:2026?

ISO/IEC 29128-2:2026 is used by evaluators who assess cryptographic protocol models, by submitters who prepare the protocol and adversarial models, and by testing laboratories that validate automated provers. It is also relevant to protocol developers and assurance teams that need to document security properties, model assumptions, and verification evidence before deployment.

Which standards are used with ISO/IEC 29128-2:2026?

ISO/IEC 29128-1:2023 is the normative reference. It provides the framework, terminology, and security-property basis that Part 2 builds on.

ISO/IEC 29128-3 is the companion part named in the document introduction. It covers evaluation methods and activities for concrete implementations of cryptographic protocols and provides the implementation-assurance framework linked in Annex D.

ISO/IEC 15408-4 provides the evaluation-method framework that Part 2 extends. ISO/IEC 15408-5 and AVA_VAN are referenced in Annex D for the relationship between confidence levels and assurance levels.

What does the ISO/IEC 29128-2:2026 document contain?

The document contains the evaluation framework, the prover assurance and confidence level descriptions, and the mapping from work units to rationale for each security property. It also includes a table of prover confidence levels for model verification and figures showing the validation workflow and the activity-to-rationale mapping.

Annex A lists example tools for automated model verification, Annex B shows how to evaluate a prover with known-answer tests, and Annex C explains the extension model used for higher confidence. Annex D relates the confidence levels to Implementation Assurance Levels in ISO/IEC 29128-3, which helps readers place this part within a broader assurance workflow.

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