专栏首页认证协议的形式化分析形式化分析工具(五)使用CAS +语法轻松编写HLPSL规范
原创

形式化分析工具(五)使用CAS +语法轻松编写HLPSL规范

使用CAS+语法的优势

  1. CAS +是一种非常简单的协议规范语法,非常类似于常用的Alice&Bob表示法。
  2. SPAN提供了将CAS +规范转换为HLPSL的最后工具。(用SPAN打开自动转换,如下图)
  3. 注意:请勿在CAS+文件中定义验证目标。因为翻译器无法正确翻译他们。
将CAS+语法转换为HLPSL

参考资料:CAS+.PDF A SHORT SPAN + AVISPA TUTORIAL.PDF

资料获取:关注:养两只猫,发送VISPA教程

CAS书写的协议规范

1. declare identifiers

声明类型:

  • user
  • public_key 通常用'表示对应的私钥
  • symmetric_key
  • function 标识符F是单向(hash)函数
  • number 此类型是对不属于其它类型(user、key)的任何数据(数字num、文本text、记录record等)的抽象

2. message sequences

协议描述的核心是指定发送消息的规则的行列表

表达形式:

  • 分量i是步骤编号
  • SiRi是用户(分别是信息的发送者和接收者)
  • →i表示用于发送消息的通道类型,有三种类型:->∼>=>(如下表)
  • Mi发送的信息。有以下_' _[_] _(_) _,_ {_}_ _^_ _#_ _,...,_ 具体含义如下表

通道描述

通道表达形式

Dolev-Yao channels

->

write protected

∼>

read and write protected

=>

标识符

含义

例子

_'

arity greater than 0

_[_]

for tables access

_(_)

单向函数访问

_,_

pairing

{_}_

加密

{Ins}K

_^_

指数

_#_

异或

_,...,_

关联多个参数

C,D,{Ins}K

3. agent knowledge

在协议执行的开始,每个主体都需要一些初步的知识来撰写他的消息。知识之后的字段将与每个用户相关联的标识符列表,描述了协议开始之前他所知道的所有数据(names,keys,function等)。我们假设每个用户的名字总是隐含在他的初始知识中。

4. session instances

通过将不同的值分配给持久性标识符,从而来描述运行协议的不同系统。不同的会话可以同时发生,也可以连续发生任意次。

注(个人理解):indentifiers/messages/knowledge相当于定义了一个交互模版。赋值C/D为scard与tv则是scard与tv的交互。

5. intruder knowledge

入侵者知识是在会话实例中引入的一组值,而不是标识符。

6. verification goals

证明三个目标:保密、强身份认证、弱身份认证。

注:合作CAS+写的协议验证目标这一项不能够很好的由SPAN工具进行转换。需要在HLPSL中使用witness/request进行设置。

例:一个简单的协议

声明“messages”部分中出现的所有值,代理和键.变量名以大写开头。如下:messages中出现有A/B/S/Kab/Kas/Kbs/Na/Nb

protocolsimple;

identifiers

A, B, S : user; %%% Declare all values, agent and keys occurring in the "messages" section

Na, Nb : number; %%% Variable names should start by a capital letter.

Kab, Kas, Kbs:symmetric_key;

messages

1. A -> S : B, {B, Kab}Kas

2. S -> B : {A, Kab}Kbs

knowledge 部分,对于每个代理,我们在开始协议会话之前声明其知道的信息。已知信息只能是上一个“标识符”部分的变量。例如,在这里,A知道自己,S,B和长期共享密钥Kas。但是,不知道Kab !!!因为,在此协议中,我们希望Kab是为每个会话生成的会话密钥(像现时一样)。与B相同:他不知道Kab在启动协议之前,将在消息中收到它。 S知道密钥Kas和Kbs,但不知道Kab。

knowledge

A : A, S, B, Kas;

B : A, S, B, Kbs;

S : A, S, B, Kas, Kbs;

此“knowlege”部分不应声明任何有关入侵者的信息! “ session_instances”上方的所有部分都定义了***标准协议***,而没有入侵者。因此,我们绝不会定义任何入侵者或入侵者密钥等。它们将在下面定义。

session_instances

[A:alice,B:bob,S:server,Kas:kas,Kbs:kbs]

这是一个标准会话,其中alice,bob,server,kas,kbs是选择用来实例化"knowledge”部分中定义的变量的任意常量。特别是,您不应为Kab定义一个常量,因为我们希望在协议执行期间生成它。

[A:i,B:bob,S:server,Kas:kis,Kbs:kbs]

这是一个会话,其中角色A将由i扮演,i是代表入侵者的保留常数。由于S和B由与上一会话相同的代理播放,因此SAME常量kbs用于此第二会话,表示B和S之间的长期密钥。由于A由i播放,因此我们创建了一个新常量入侵者和服务器之间共享的密钥。

;会话列表以分号结尾。

intruder_knowledge

alice,bob,server,kis;入侵者知道alice,bob,服务器和kis

其它参考:

  1. 针对AVISPA的文献: A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.-C. H´ eam, O. Kouchnarenko,J. Mantovani, S. M¨ odersheim, D. von Oheimb, M. Rusinowitch, J. Santos Santiago, M. Turuani, L. Vigan` o, and L. Vigneron. The A VISPA Tool for the automated validation of internet security protocols and applications. In CA V’2005, volume 3576 of LNCS, pages 281–285. Springer, 2005.
  2. 针对HLSPL的文献: Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, J. Mantovani, S. M¨ odersheim, and L. Vigneron. A high level protocol specification language for industrial security-sensitive protocols. In Proceedings of Workshop on Specification and Automated Processing of Security Requirements (SAPS), Linz, Austria, 2004.
  3. 针对CASRUL的文献: F. Jacquemard, M. Rusinowitch, and L. Vigneron. Compiling and Verifying Security Protocols. In Proceedings of 7th Conference on Logic for Programming and Automated Reasoning, volume 1955 of LNAI. Springer-Verlag, 2000.

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

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

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 形式化分析工具AVISPA(三)学习User micro-manual of AVISPA

    hlpsl2if:将用HLPSL语言编写的规范转换为IF语言的低级规范的工具。cl-atse:用于分析安全属性的工具

    春风大魔王
  • (补充)SPAN+AVISPA for Verifying Cryptographic Protocols

    消息认证:如果A知道是谁创建的消息m,则称A能认证m。电子签名:私钥加密、公钥解密。(ID,{ID}K-1) 比较ID是否一样。

    春风大魔王
  • SPAN: a Security Protocol ANimator for A VISPA

    Protocol Simulation:模拟协议并建立对应于HLPSL规范的特定MSC(Message Sequence Charts,消息序列图);

    春风大魔王
  • 微信小程序一行文字水平居中

    特别声明:除特别标注,本站文章均为原创,本站文章原则上禁止转载,如确实要转载,请电联:wangyeuuu@qq.com,尊重他人劳动成果,谢过~

    lollipop72
  • SpringCloud 系列Eureka 注册中心初体验

    在 SpringCloud 微服务体系中,有几个比较重要的组件,如注册中心,配置中心,网关,安全、负载均衡、监控等等,接下来我们将来看一下这些常用的组件有什么用...

    一灰灰blog
  • 微服务架构的服务发现机制

    分布式微服务系统架构其最大一个特性即分布式,所以如何知道每个独立的微服务的服务器地址、端口、以及其他相关信息呢?同时,相对于传统分布式系统的部署:相关独立业务逻...

    IMWeb前端团队
  • PaddlePaddle发布基于Docker的AI系统开发流程

    【新智元导读】 本文来自PaddlePaddle团队,介绍了PaddlePaddle与众不同的基于Docker的编译、开发、测试、调试、发布、部署、和运行的全...

    新智元
  • mysql 登陆异常 Host 'x.x.x.x' is not allowed to connect to this MySQL server"

    Host列指定了允许用户登录所使用的IP,可以使用通配符%,例如‘10.1.%’。 如果host=’%‘标识允许所有地址访问

    路过君
  • 为什么要用私钥加签,公钥加密

    之所以用发送方的私钥加签,是因为,即便信息被黑客拦截,黑客修改了信息,但是加签需要用发送方的私钥,黑客没有发送方的私钥,所以也无法生成正确的签名,接收方验签就不...

    yaphetsfang
  • MySQL之ROUND函数四舍五入的陷阱

    在MySQL中,ROUND函数用于对查询结果进行四舍五入,不过最近使用ROUND函数四舍五入时意外发现并没有预期的那样,本文将这一问题记录下来,以免大家跟我一样...

    用户2131907

扫码关注云+社区

领取腾讯云代金券