前往小程序,Get更优阅读体验!
立即前往
首页
学习
活动
专区
工具
TVP
发布
社区首页 >专栏 >SPAN: a Security Protocol ANimator for A VISPA

SPAN: a Security Protocol ANimator for A VISPA

原创
作者头像
春风大魔王
修改2020-07-22 09:53:10
1.7K0
修改2020-07-22 09:53:10
举报
文章被收录于专栏:认证协议的形式化分析

本文较为详细的介绍了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自动建立攻击)。

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

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

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

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

评论
登录后参与评论
0 条评论
热度
最新
推荐阅读
目录
  • 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 (基于树自动机的自动近似分析安全协议)
  • SPAN
领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档