Scyther形式化验证工具简单教程

Scyther形式化验证工具

Scyther是一种自动化的安全协议验证工具。在协议的安全性验证方面有着广泛的应用。
下面介绍其安装方法以及使用教程。

安装方法

Scyther工具在Windows 10环境下的安装需要以下工具包：
Python2.X
wxPython
graphviz
下面是我使用的软件包的版本：
python我使用的是python-2.7.18.amd64。（我是AMD的CPU）
wxPython是wxPython3.0-win64-3.0.0.0-py27。
graphviz是stable_windows_10_cmake_Release_x64_graphviz-install-2.47.0-win64。
此外要需要在Scyther官网上下载Scyther的文件包，我下载的是scyther-w32-v1.1.3。
出于方便起见，我将上述内容上传到百度网盘中，有需要的朋友可以直接下载。链接：https://pan.baidu.com/s/1sjX2Ad0feupCJx_kkO_sAQ 提取码：5204
建议使用默认路径安装，不要出现中文路径，graphviz需要把安装位置下的 bin 路径加入环境变量Path。
验证安装使用成功可以在cmd下输入

dot --version

打开cmd。cd到Scyther的存放路径，输入python scyther-gui.py，就会出现Scyther的界面。
输入代码后点击Verify中的第一个选项，如果是使用自动安全声明则使用第三个选项。（安全声明后续讲）
2. 使用教程
在我看来，Scyther的语法是比较简单的，至少比AVISPA简单多了，反正AVISPA我是学不会。。。
首先，我们给协议起一个名字，就叫yuyu吧，然后假设我们的协议里面一共有三个角色，分别是I，R，S。那么我们的代码框架就出来了。

protocol yuyu(I,R,S)
{role I{//xxxx}role R{//xxxx}role S{//xxxx}
}

然后我们向里面添加东西。在Scyther里面，所有的变量都需要预先定义，通过以下两种方法。第一种是新建变量并赋随机值，使用fresh，第二种只是新建变量，等待被赋值，使用var。我们使用这两种方法分别示范新建一个 N 随机数变量。

fresh N:Nonce;

var N:Nonce;

Scyther提供了若干类型让我们使用，比如刚刚提到的随机数用Nonce，哈希函数要首先定义hashfunction H;，后续操作就可以直接使用H()。
此外，我们还可以定义一些自己的类型，比如
定义密钥：

usertype Sessionkey;

定义时间戳：

usertype Timestamp;

定义String类型：

usertype String;

定义完成后这些自定义类型就可以像Nonce类型一样使用。在Scyther中，协议消息的传递使用的是send和recv。其参数中第一个是消息的发送人（角色），第二个是消息的接收人（角色），第三个则是消息的内容。
我们举个例子，I 向 R发送一个随机数N。
在I中应该使用send

send_1(I,R,N);

在R中应该使用Recv

recv_1(I,R,N);

我们变点花样，将N哈希函数哈希，那么I和R应该是这样：

send_1(I,R,H(N));

recv_1(I,R,H(N));

我们在变一变，将哈希结果使用I与R之间的对称密钥解密，对称密钥在Scyther中是这么表示的k(I,R)，这是默认存在的，不需要先定义。

send_1(I,R,{H(N)}k(I,R));

recv_1(I,R,{H(N)}k(I,R));

match可以被用于计算，比如我们将N1和N2的哈希结果作为Kc，可以这样子写：

match(Kc,H(N1,N2));

接下来讲述安全声明。Scyther提供了若干种声明，分别是Secret、Alive、Weakagree、Niagree、Nisynch。这些有的是保护消息机密性的，有的抗重放攻击，有的保障前后向安全性。按照我个人浅见，我们只需要把协议得出的会话密钥使用Secret声明，协议所有的角色分别使用Alive、Weakagree、Niagree、Nisynch声明，就没问题了。

claim(I,Secret,Kc);//Kc是生成的会话密钥
claim(I,Alive);
claim(I,Weakagree);
claim(I,Niagree);
claim(I,Nisynch);

那么，我们综合起来，假定角色I给角色R发了一个经过加密的消息，加密的内容是随机数的哈希结果，角色R给角色S发送一个新生成的会话密钥(由N1和N2哈希得到)和一串字符串，两者都被加密，那么代码应该是：

usertype String;
usertype Sessionkey;
hashfunction H;
protocol yuyu(I,R,S)
{role I{fresh N:Nonce;send_1(I,R,{H(N)}k(I,R));claim(I,Alive);claim(I,Weakagree);claim(I,Niagree);claim(I,Nisynch);}role R{fresh ID:String;fresh N2:Nonce;var Kc:Sessionkey;var N:Nonce;recv_1(I,R,{H(N)}k(I,R));match(Kc,H(N,N2));send_2(R,S,{Kc,ID}k(R,S));claim(R,Secret,Kc);claim(R,Alive);claim(R,Weakagree);claim(R,Niagree);claim(R,Nisynch);}role S{var Kc:Sessionkey;var ID:String;recv_2(R,S,{Kc,ID}k(R,S));claim(S,Secret,Kc);claim(S,Alive);claim(S,Weakagree);claim(S,Niagree);claim(S,Nisynch);}
}

Scyther形式化验证工具简单教程相关推荐

形式化验证工具TLA+：程序员视角的入门之道
简介: 女娲是飞天分布式系统中提供分布式协同的基础服务,支撑着阿里云的计算.网络.存储等几乎所有云产品.在女娲分布式协同服务中,一致性引擎是核心基础模块,支持了Paxos,Raft,EPaxos等多种 ...
成都链安重磅出品 | 基于VS Code插件的智能合约自动形式化验证工具Beosin—VaaS『离线免费版』...
11月4日,成都链安重磅推出『离线免费版』智能合约自动形式化验证工具Beosin-VaaS,该版本基于流行的开发工具VS Code插件,供广大开发者免费使用.获得方式如下,欢迎体验使用: https: ...
FPGA形式化验证工具OneSpin360学习笔记（一）
目录 OneSpin360图形界面一致性检查举例等价性检查举例 Onespin是领先的EDA解决方案提供商,其360系列产品为FPGA形式化验证工具.它以强大.高性能的形式化验证引擎为基础,能够覆 ...
mysql压力测试教程_Mysqlslap MySQL压力测试工具简单教程
MySQL从5.1.4版开始带有一个压力测试工具mysqlslap,通过模拟多个并发客户端访问mysql来执行测试,使用起来非常的简单.通过mysqlslap –help可以获得可用的选项,这里列一些 ...
软件形式化验证工具设备单项论证报告
1 设备名称混合形式化验证工具 (CT-Scan) 2 设备介绍 2.1理论基础采用C/C++语言进行编写的代码,在进行软件验证的过程中往往需要花费大量时间和精力,迫切需要一款能够自动测试验证软件 ...
linux内核形式化验证,聪明人的笨功夫 -- MesaTEE安全形式化验证实践
各类TEE(例如TPM和Intel SGX)提供了强大的可信计算硬件基础,但他们并不直接保证软件的安全性.诸如缓冲区溢出等内存安全问题为攻击者提供了侵入TEE的可乘之机.因此,软件内存安全保护极其重要 ...
操作系统形式化验证实践教程(7) - C代码的自动验证
操作系统形式化验证实践教程(7) - C代码的自动验证上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...
操作系统形式化验证实践教程(7) - C代码的自动验证（转载）
操作系统形式化验证实践教程(7) - C代码的自动验证上一节教程不知道大家看晕了没有,其实虽然细节很多还没有讲清楚,但是从结构上大家可以看到,其实是很模式化的工作. 那么能不能让这个模式化的工作自动 ...

Scyther形式化验证工具简单教程

Scyther形式化验证工具

Scyther形式化验证工具简单教程相关推荐

最新文章

热门文章