没有合适的资源?快使用搜索试试~ 我知道了~
首页ProVerif manual
ProVerif manual
需积分: 50 15 下载量 80 浏览量
更新于2023-03-16
评论
收藏 1.1MB PDF 举报
形式化分析工具,可以帮助我们在构建了认证协议后给出我们方案的安全性证明。
资源详情
资源评论
资源推荐
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-Rocquen cour t , 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-Rocquenc our t 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 wit hout the helpful remark s from the research community; their contributions
are greatly appreciated and further feedback is en cour aged.
iii
iv
Contents
1 Introduction 1
1.1 Applications of ProVerif . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Scope of this manual . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Support . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.4 Installation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.4.1 Linux/Mac installation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.4.2 Windows installation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.4.3 Emacs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.5 Copyright . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
2 Getting started 5
3 Using ProVerif 9
3.1 Modeling protocols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
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
3.3.1 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.3.2 Example: ProVerif output for the handshake protocol . . . . . . . . . . . . . . . . 21
4 Language features 29
4.1 Primitives and mode li ng features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4.1.1 Constants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4.1.2 Data constr u ct ors and type conversion . . . . . . . . . . . . . . . . . . . . . . . . . 29
4.1.3 Enriched terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
4.1.4 Tables and key distribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
4.1.5 Phases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
4.1.6 Synchronization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4.2 Further cryptographic operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 cor r es pondence assertions, secrecy, and events . . . . . . . . . . . . . . . 40
4.3.2 Observational equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
v
剩余122页未读,继续阅读
qq_40593586
- 粉丝: 0
- 资源: 1
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- RTL8188FU-Linux-v5.7.4.2-36687.20200602.tar(20765).gz
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
- SPC统计方法基础知识.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功
评论0