SPAN: a Security Protocol ANimator for A VISPA

本文较为详细的介绍了SPAN工具。

这是一次阅读笔记及个人思考。

原文：可以用科学上网获取。时间充足的话我会上传到百度网盘。会公布在评论处。

OFMC:the On-the-Fly Model-Checker( 即时模型检查器 )

CL:Constraint-Logic-based model-checker（基于约束逻辑的模型检查器）

SATMC: SAT-based Model-Checker（ 基于SAT的模型检查器 ）

TA4SP: Tree Automata based Automatic Approximations for the Analysis of Security Protocols （基于树自动机的自动近似分析安全协议）

Protocol Simulation：模拟协议并建立对应于HLPSL规范的特定MSC（Message Sequence Charts，消息序列图）；

Intruder Simulation：用主动/被动入侵者模拟协议

Attack Simulation： 用于从OFMC或CL-ATSE工具的输出自动构建MSC攻击。

HLPSL是一种表达性的，模块化的，基于角色的形式语言，用于指定控制流模式，数据结构，替代入侵者模型和复杂的安全属性，以及不同的密码原语及其代数属性。

以下为原文翻译

我们使用Needham-Schroeder公钥协议[NS78]的规范来介绍HLPSL：

HLPSL规范基于角色描述，即有限状态自动机，在发送或接收消息时会触发“transitions”。关于“ Alice＆Bob”（爱丽丝与鲍勃）符号，HLPSL明确规定了角色的内部状态，消息生成，消息发送和接收。这是从该协议的HLPSL规范中提取的基本角色声明的示例。（HLPSL协议的规范可以结合我前面的文章进行阅读）

然后，在“sessions”中将角色组合在一起，使角色（例如，公钥）之间共享的知识明确化。

最后，定义了用于协议执行的environment()，其中“ i”表示入侵者。该环境还定义了入侵者的初始知识和会话的初始设置，即运行了多少会话以及由谁运行。

在上面的示例中，定义了四个Honnest代理，即a，b，c和d，并且入侵者知道所有公共密钥以及其自己的私有密钥inv（ki）。

SPAN

SPAN带有AVISPA Web图形界面的本地版本。它看起来相同并且具有相同的功能：协议规范的简单编辑，AVISPA验证后端的选择和配置以及两个按钮（这些是新的）：协议模拟（仅诚实的代理），入侵者模拟（诚实的代理和入侵者）和攻击模拟（与入侵者模拟相同的布局，但是使用OFMC / CLATSE自动建立攻击）。