形式化分析工具（五）使用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是步骤编号
• Si和Ri是用户（分别是信息的发送者和接收者）
• →i表示用于发送消息的通道类型，有三种类型：->；∼>；=>（如下表）
• Mi发送的信息。有以下_' _[_] _(_) _,_ {_}_ _^_ _#_ _,...,_ 具体含义如下表

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.