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.