形式化分析工具(五)使用CAS +语法轻松编写HLPSL规范
使用CAS+语法的优势
- CAS +是一种非常简单的协议规范语法,非常类似于常用的Alice&Bob表示法。
- SPAN提供了将CAS +规范转换为HLPSL的最后工具。(用SPAN打开自动转换,如下图)
- 注意:请勿在CAS+文件中定义验证目标。因为翻译器无法正确翻译他们。
参考资料: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
发送的信息。有以下_'
_[_]
_(_)
_,_
{_}_
_^_
_#_
_,...,_
具体含义如下表
通道描述 |
通道表达形式 |
---|---|
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
其它参考:
- 针对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.
- 针对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.
- 针对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.
- HTTP严格安全传输(HTTP Strict Transport Security, HSTS)chromuim实现源码分析(一)
- Linux下ls命令显示符号链接权限为777的探索
- Django form表单
- Django ORM那些相关操作
- 使用mitmproxy嗅探双向认证ssl链接——嗅探AWS IoT SDK的mqtts
- Django中ORM介绍和字段及其参数
- 几个实现分页的方法
- 如何识别IDA反汇编中动态链接库中的函数
- Kali Linux安装TL-WN821N USB无线网卡驱动(make失败)
- Cookie、Session登陆验证相关介绍和用法
- 题型分析
- .NET CORE 框架ABP的代码生成器(ABP Code Power Tools )使用说明文档
- Lua编写wireshark插件初探——解析Websocket上的MQTT协议
- 在Ubuntu 16.04环境下安装Docker-CE(附视频教程)
- JavaScript 教程
- JavaScript 编辑工具
- JavaScript 与HTML
- JavaScript 与Java
- JavaScript 数据结构
- JavaScript 基本数据类型
- JavaScript 特殊数据类型
- JavaScript 运算符
- JavaScript typeof 运算符
- JavaScript 表达式
- JavaScript 类型转换
- JavaScript 基本语法
- JavaScript 注释
- Javascript 基本处理流程
- Javascript 选择结构
- Javascript if 语句
- Javascript if 语句的嵌套
- Javascript switch 语句
- Javascript 循环结构
- Javascript 循环结构实例
- Javascript 跳转语句
- Javascript 控制语句总结
- Javascript 函数介绍
- Javascript 函数的定义
- Javascript 函数调用
- Javascript 几种特殊的函数
- JavaScript 内置函数简介
- Javascript eval() 函数
- Javascript isFinite() 函数
- Javascript isNaN() 函数
- parseInt() 与 parseFloat()
- escape() 与 unescape()
- Javascript 字符串介绍
- Javascript length属性
- javascript 字符串函数
- Javascript 日期对象简介
- Javascript 日期对象用途
- Date 对象属性和方法
- Javascript 数组是什么
- Javascript 创建数组
- Javascript 数组赋值与取值
- Javascript 数组属性和方法
- 数据结构 - 堆(Heap)
- 信息收集之主机发现:masscan
- 信息收集之社工字典
- CloudBase CMS 2.0 焕新升级,从「心」出发!
- 使用MySQL Keyring 的 SECRET类型密钥执行非对称加密
- node egg 实现跨域
- 使用Markdown画流程图
- HBase NotServingRegionException
- Flink SQL 写入 Hive表的性能问题
- 文件系统索引extent 和 bitmap区别
- MySQL的Bugs
- 对复制实施主键约束
- MySQL如何管理客户端的连接?
- 鸿蒙 Ability 讲解(页面生命周期、后台服务、数据访问)
- MySQL如何管理客户端连接?线程池篇