没有合适的资源?快使用搜索试试~ 我知道了~
首页形式化分析工具Scyther软件的说明手册
资源详情
资源评论
资源推荐
Scyther
User Manual
Cas Cremers
Draft February 18, 2014
2
Contents
1 Introduction 5
2 Background 7
3 Installation 9
4 Quick start tutorial 11
5 Input Language 15
5.1 A minimal input file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
5.2 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
5.2.1 Atomic terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
5.2.2 Pairing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
5.2.3 Symmetric keys . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
5.2.4 Asymmetric keys . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
5.2.5 Hash functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
5.2.6 Predefined types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
5.2.7 Usertypes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
5.3 Events . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
5.3.1 Receive and send events . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
5.3.2 Claim events and Security properties . . . . . . . . . . . . . . . . . . . . . 18
5.3.3 Internal computation/pattern match events . . . . . . . . . . . . . . . . . 19
5.4 Role definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
5.5 Protocol definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
5.6 Global declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
5.7 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
5.7.1 Macro . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
5.7.2 Include . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
5.7.3 one-role-per-agent . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
5.8 Language BNF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
5.8.1 Input file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
5.8.2 Protocols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
5.8.3 Roles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
5.8.4 Events . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
5.8.5 Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
5.8.6 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
3
4 CONTENTS
6 Modeling security protocols 25
6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
6.2 Example: Needham-Schroeder Public Key . . . . . . . . . . . . . . . . . . . . . . 25
7 Specifying security properties 29
7.1 Specifying secrecy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7.2 Specifying authentication properties . . . . . . . . . . . . . . . . . . . . . . . . . 29
7.2.1 Aliveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7.2.2 Non-injective synchronisation . . . . . . . . . . . . . . . . . . . . . . . . . 29
7.2.3 Non-injective agreement . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7.2.4 Agreement over data . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8 Using the Scyther tool GUI 31
8.1 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8.2 Bounding the statespace . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8.3 Attack graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8.3.1 Runs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8.3.2 Communication events . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
8.3.3 Claims . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9 Using the Scyther command-line tools 37
10 Advanced topics 39
10.1 Modeling more than one asymmetric key pair . . . . . . . . . . . . . . . . . . . . 39
10.2 Approximating equational theories . . . . . . . . . . . . . . . . . . . . . . . . . . 39
10.3 Modeling time-stamps and global counters . . . . . . . . . . . . . . . . . . . . . . 41
10.3.1 Modeling global counters . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
10.3.2 Modeling time-stamps using nonces . . . . . . . . . . . . . . . . . . . . . 41
10.3.3 Modeling time-stamps using variables . . . . . . . . . . . . . . . . . . . . 42
10.4 Multi-protocol attacks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
11 Further reading 45
A Full specification for Needham-Schroeder public key 49
Chapter 1
Introduction
Note:
This is a draft of the new version of the Scyther manual. The manual
may therefore be incomplete at p oints.
Any feedback is welcome and can be sent to Cas Cremers by e-mail:
cas.cremers@cs.ox.ac.uk.
This is the user manual for the Scyther security protocol verification tool.
The purpose of this manual is to explain the details of the Scyther input language, explain
how to model basic protocols, and how to effectively use the Scyther tool. This manual does not
detail the protocol execution model nor the adversary model used by the tool. It is therefore
highly recommended to read the accompanying book [1]. The book includes a detailed description
of Scyther’s underlying protocol model, security property specifications, and the algorithm.
We proceed in the following way. Some background is given in Chapter 2. Chapter 3 explains
how to install the Scyther tool on various platforms. In Chapter 4 we give a brief tutorial using
simple examples to show the basics of the tool. Then we discuss things in more detail as we
introduce the input language of the tool in Chapter 5. Modeling of basic protocols is described in
Chapter 6, and Chapter 7 describes how to specify security properties. The usage of the GUI
version of tool is then explained in more detail in Section 8. The underlying command-line tool is
described in Section 9. Advanced topics are discussed in Section 10.
Online information
More help can be found online on the Scyther website:
http://users.ox.ac.uk/
~
coml0529/scyther/index.html
Users are advised to subscribe to the Scyther mailing list, whose details can also be found on the
Scyther website.
5
剩余51页未读,继续阅读
明月嫣然-疏桐-暖阳
- 粉丝: 348
- 资源: 23
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- zigbee-cluster-library-specification
- JSBSim Reference Manual
- 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
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功
评论0