第1页 / 共123页
第2页 / 共123页
第3页 / 共123页
第4页 / 共123页
第5页 / 共123页
第6页 / 共123页
第7页 / 共123页
第8页 / 共123页
ProVerif manual.pdf
Chapter 1
Introduction
1.1 Applications of ProVerif
1.2 Scope of this manual
1.3 Support
1.4 Installation
1.4.1 Linux/Mac installation
1.4.2 Windows installtion
1.4.3 Emacs
1.5 Copyright
Chapter 2
Getting started
Chapter 3
Using ProVerif
3.1 Modeling protocols
3.1.1 Declarations
3.1.2 Example:Declaring cryptographic primitives for the handshake protocol
3.1.3 Process macros
3.1.4 Process
3.1.5 Example: handshake protocol
3.2 Security properties
3.2.1 Reachability and secrecy
3.2.2 Correspondence assertions,events,and authentications
3.2.3 Example: Secrecy and authentication in the handshake protocol
3.3 Understanding ProVerif output
3.3.1 Results
3.3.2 Example: ProVerif output for the handshake protocol
Chapter 4
Language features
4.1 Primitives and modeling features
4.1.1 Constants
4.1.2 Data constructors and type conversion
4.1.3 Enriched terms
4.1.4 Tables and key distribution
4.1.5 Phases
4.1.6 Synchronization
4.2 Further cryptographic operators
4.2.1 Extended destructions
4.2.2 Equations
4.2.3 Function macros
4.2.4 Process macros with fail
4.2.5 Suitable formalizations of cryptographic primitives
4.3 Further security properties
4.3.1 Complex correspondence assertions,secrecy,and events
Chapter 5
Needham-Schroeder public key protocol:Case Study
5.1 Simplified Needham-Schroeder protocol
5.1.1 Basic encoding
5.1.2 Security properties
5.2 Full Needham-Schroeder protocol
ProVerif 1.97pl1:
Automatic Cryptographic Protocol Verifier,
User Manual and Tutorial
Bruno Blanchet, Ben Smyth, Vincent Cheval, and Marc Sylvestre
Bruno.Blanchet@inria.fr, research@bensmyth.com, vincent.cheval@icloud.com,
marc.sylvestre@inria.fr
September 12, 2017
ii
Acknowledgements
This manual was written with support from the Direction G´en´erale pour l’Armement (DGA) and the
EPSRC project UbiVal (EP/D076625/2). ProVerif was developed while Bruno Blanchet was affiliated
with INRIA Paris-Rocquencourt, with CNRS, Ecole Normale Sup´erieure, Paris, and with Max-Planck-
Institut f¨ur Informatik, Saarbr¨ucken. This manual was written while Bruno Blanchet was affiliated with
INRIA Paris-Rocquencourt and with CNRS, Ecole Normale Sup´erieure, Paris, Ben Smyth was affiliated
with Ecole Normale Sup´erieure, Paris and with University of Birmingham, Vincent Cheval was affiliated
with CNRS, and Marc Sylvestre was affiliated with INRIA Paris. The development of ProVerif would
not have been possible without the helpful remarks from the research community; their contributions
are greatly appreciated and further feedback is encouraged.
iii
iv
Contents
1 Introduction
1.1 Applications of ProVerif
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.2 Scope of this manual . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.3 Support . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Installation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.4
1.4.1 Linux/Mac installation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.4.2 Windows installation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.4.3 Emacs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.5 Copyright . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2 Getting started
1
1
2
2
2
3
3
4
4
5
3 Using ProVerif
9
9
3.1 Modeling protocols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.1.1 Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
9
3.1.2 Example: Declaring cryptographic primitives for the handshake protocol . . . . . . 11
3.1.3 Process macros . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
3.1.4 Processes
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.1.5 Example: handshake protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.2 Security properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.2.1 Reachability and secrecy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.2.2 Correspondence assertions, events, and authentication . . . . . . . . . . . . . . . . 17
3.2.3 Example: Secrecy and authentication in the handshake protocol
. . . . . . . . . . 18
3.3 Understanding ProVerif output . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
. . . . . . . . . . . . . . . . 21
3.3.1 Results
3.3.2 Example: ProVerif output for the handshake protocol
4 Language features
4.2 Further cryptographic operators
29
4.1 Primitives and modeling features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4.1.1 Constants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4.1.2 Data constructors and type conversion . . . . . . . . . . . . . . . . . . . . . . . . . 29
4.1.3 Enriched terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
4.1.4 Tables and key distribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
4.1.5 Phases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
Synchronization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4.1.6
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4.2.1 Extended destructors
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4.2.2 Equations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4.2.3 Function macros . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4.2.4 Process macros with fail . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2.5
Suitable formalizations of cryptographic primitives . . . . . . . . . . . . . . . . . . 37
4.3 Further security properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
4.3.1 Complex correspondence assertions, secrecy, and events
. . . . . . . . . . . . . . . 40
4.3.2 Observational equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
v
vi
CONTENTS
5 Needham-Schroeder: Case study
5.1 Simplified Needham-Schroeder protocol
53
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
5.1.1 Basic encoding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
5.1.2
Security properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
5.2 Full Needham-Schroeder protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
. . . . . . . . . . . . . . . . . . . . . . . . . . . 60
5.3 Generalized Needham-Schroeder protocol
5.4 Variants of these security properties
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5.4.1 A variant of mutual authentication . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5.4.2 Authenticated key exchange . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
5.4.3 Full ordering of the messages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
6 Advanced reference
6.2 ProVerif options
6.1 Advanced modeling features and security properties
77
. . . . . . . . . . . . . . . . . . . . . 77
6.1.1 Predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
6.1.2 Referring to bound names in queries . . . . . . . . . . . . . . . . . . . . . . . . . . 80
6.1.3 Exploring correspondence assertions . . . . . . . . . . . . . . . . . . . . . . . . . . 82
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
6.2.1 Command-line arguments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
6.2.2
Settings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
6.3 Theory and tricks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
6.3.1 Performance and termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
6.3.2 Alternative encodings of protocols
. . . . . . . . . . . . . . . . . . . . . . . . . . . 94
6.3.3 Applied pi calculus encodings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
6.3.4
Sources of incompleteness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
6.3.5 Misleading syntactic constructs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
6.4 Compatibility with CryptoVerif . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
7 Outlook
A Language reference
103
105
List of Figures
3.1 Handshake protocol
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
3.2 Term and process grammar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
3.3 Pattern matching grammar
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
3.4 Messages and events for authentication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.5 Handshake Protocol Attack Trace . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
4.1 Enriched terms grammar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
4.2 Grammar for correspondence assertions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
A.1 Grammar for terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
A.2 Grammar for declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
A.3 Grammar for not and queries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
A.4 Grammar for nounif . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
A.5 Grammar for clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
A.6 Grammar for processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
vii
viii
LIST OF FIGURES
相关推荐
2023年江西萍乡中考道德与法治真题及答案.doc
2012年重庆南川中考生物真题及答案.doc
2013年江西师范大学地理学综合及文艺理论基础考研真题.doc
2020年四川甘孜小升初语文真题及答案I卷.doc
2020年注册岩土工程师专业基础考试真题及答案.doc
2023-2024学年福建省厦门市九年级上学期数学月考试题及答案.doc
2021-2022学年辽宁省沈阳市大东区九年级上学期语文期末试题及答案.doc
2022-2023学年北京东城区初三第一学期物理期末试卷及答案.doc
2018上半年江西教师资格初中地理学科知识与教学能力真题及答案.doc
2012年河北国家公务员申论考试真题及答案-省级.doc
2020-2021学年江苏省扬州市江都区邵樊片九年级上学期数学第一次质量检测试题及答案.doc
2022下半年黑龙江教师资格证中学综合素质真题及答案.doc
