专栏首页认证协议的形式化分析SPAN: a Security Protocol ANimator for A VISPA
原创

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自动建立攻击)。

原创声明,本文系作者授权云+社区发表,未经许可,不得转载。

如有侵权,请联系 yunjia_community@tencent.com 删除。

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 形式化分析工具(六):HLPSL Tutorial

    本文为阅读笔记。文章题目为: HLPSL Tutorial A Beginner’s Guide to Modelling and Analysing Inte...

    春风大魔王
  • 形式化分析工具AVISPA(二):使用及教程资料

    参考资料:https://blog.csdn.net/pan_tian/article/details/22619687

    春风大魔王
  • 形式化分析工具(七)AVISPA v1.1 User Manual

    A VISPA (Automated Validation of Internet Security Protocols and Applications) I...

    春风大魔王
  • spss C# 二次开发 学习笔记(六)——Spss统计结果的输出

    Spss的二次开发可以很简单,实例化一个对象,然后启用服务,接着提交命令,最后停止服务。 其中重点为提交命令,针对各种统计功能需求,以及被统计分析的数据内容等,...

    用户1637609
  • 约束条件变更对算法运行时间所带来的影响

    有1,...,n次请求,去获取单个资源,每个请求的开始时间是s(i),结束时间是f(i), 对于请求i和j,如果二者的区间不重合,即f(i)<=s(j) 或者 ...

    爬蜥
  • 【CV中的注意力机制】史上最强"ResNet"变体--ResNeSt

    【前言】:我们前面已经详细介绍了Attention机制和视觉注意力机制在图像分类结构中的应用--SENet 和 基于SENet的改进版--SKNet。本篇我们将...

    深度学习技术前沿公众号博主
  • Java浮点数机制及所存在的问题

    Java中浮点数的机制,IEEE 754规则,以及为什么在java中0.1+0.2!=0.3

    俺也想起舞
  • 如何查看Django ORM执行的SQL语句

    Django ORM对数据库操作的封装相当完善,日常大部分数据库操作都可以通过ORM实现。

    BigYoung小站
  • 前端笔试题(附答案)

    var obj = { id:1, name:"jacky" };alert(obj.name);上例表示创建一个具有属性 id (值为 1)、属性 name(...

    用户7657330
  • 读C#开发实战1200例子记录-2017年8月14日10:03:55

    landv

扫码关注云+社区

领取腾讯云代金券