Foreword

Foreword

Introduction

1Scope

2Normative references

3Terms and definitions

4Formal verification of cryptographic protocols

4.1Methods for modelling cryptographic protocols

4.2Verification requirements

4.2.1Methods of verification

4.2.2Verification tools

4.2.3Bounded vs unbounded verification

4.3Cryptographic protocol model

4.3.1Description of a model

4.3.2Formal specification

4.3.3Adversarial model

4.3.3.1General

4.3.3.2Network specification

4.3.3.3Dolev-Yao model

4.3.4Submitting a model

4.3.5Security properties

4.3.6Self-assessment evidence

5Verification process

5.1General

5.2Duties of the submitter

5.3Duties of the evaluator

5.3.1Main duties

5.3.2Evaluating the prover

5.3.3Evaluating the model

5.3.4Evaluating the evidence

5.3.5Example evaluation

Annex AThe Needham-Schroeder-Lowe public key protocol (informative)

A.1Protocol specification

A.2Protocol model

Annex BExample submission (informative)

B.1General

B.2Protocol specification

B.3Protocol model

B.4Self-assessment evidence

B.5Automated prover

B.6Security properties

Annex CExample evaluation (informative)

C.1General

C.2Evaluation

C.2.1Evaluating the prover

C.2.2Evaluating the model

C.2.3Evaluating the evidence

Annex DDolev-Yao model (informative)

Annex ESecurity properties (informative)

E.1General

E.2Secrecy

E.3Perfect forward secrecy

E.4Strong secrecy

E.5Integrity

E.6Authentication

E.6.1General

E.6.2Aliveness

E.6.3Injective agreement

Bibliography