形式化分析工具(六):HLPSL Tutorial(Example3)
本文主要对security goals这一节内容进行阅读并记录
前文总结:如何从零开始完成协议规范的书写,建议步骤。
1.用alice-bob形式写出流程
2.用CAS+语法进行编写
3.使用SPAN工具将CAS+编写的文件编译为hlpsl格式
4.完善安全目标部分(本节内容)
Example 3 - security goals
示例协议来源为安德鲁安全RPC协议的改编版:该协议用于相互认证双方,然后建立可以用于进一步通信的新共享密钥K1ab(可以作为其它协议的一部分)。此协议的A-B表示法如下。
HLPSL规范的协议如下:
具体步骤:(可以对照上一篇文章,加深对书写规则的理解,比如Na’ 什么时候用,state的值的问题。安全目标witness与request的用法)
0. State = 0 / RCV(start) =|>
State’:= 2 / Na’ := new()
/ SND(A.{Na’}_Kab)
1. State = 1 / RCV(A.{Na’}_Kab) =|>
State’:= 3 / Nb’ := new()
/ SND({Succ(Na’).Nb’}_Kab)
/ witness(B,A,alice_bob_na,Na’) % B 收到了能证明A的身份的Na。B希望Na能够得到认证。
2. State = 2 / RCV({Succ(Na).Nb’}_Kab) =|>
State’:= 4 / SND({Succ(Nb’)}_Kab)
/ witness(A,B,bob_alice_nb,Nb’)
3. State = 3 / RCV({Succ(Nb)}_Kab) =|>
State’:= 5 / N1b’ := new()
/ K1ab’ := new()
/ SND({K1ab’.N1b’}_Kab)
/ witness(B,A,alice_bob_k1ab,K1ab’)
/ request(B,A,bob_alice_nb,Nb)
/ secret(K1ab’,k1ab,{A,B})
/ secret(N1b’,n1b,{A,B})
4. State = 4 / RCV({K1ab’.N1b’}_Kab) =|>
State’:= 6
/ request(A,B,alice_bob_k1ab,K1ab’)
/ request(A,B,alice_bob_na,Na)
2.3.1讨论与分析结果
指定安全目标
机密性:
如,我们想确保交换的密钥K1ab和生成的现时N1b在A和B之间是机密的。 通常建议将这样的秘密事实放置在创建应为秘密值的角色中 。(即谁首次创建的这两个密钥,则在谁处声明安全目标。)
表明: B允许两个值(仅)在A和B之间共享。 表明从此刻起应具有保密性。
secret的常量第二个参数(k1ab、n1b)称为协议ID,并且必须在环境角色的const部分中声明为protocol_id类型。
建模惯例是将协议事实ID用作secret所指代的变量的名称(以小写形式表示)。对于secret,协议ID仅用于区分不同的保密目标。
在安全目标中如下表示:
goal
secrecy_of n1b, k1ab
认证
The witness
and request
events are goal facts related to authentication
.
例如,在此示例中,两个参与者当然应该就交换后的密钥K1ab的值达成共识。特别是,alice希望确保该值确实是由bob创建的,是为她创建的,目的是用作共享密钥,并且不会在上一个会话中重播该值。为此,我们在alice的最后一个过渡中编写了这一行。内容如下:(/ request(A,B,alice_bob_k1ab,K1ab’
)“代理A接受值K1ab',现在依靠该代理B存在的保证并就此值与她达成协议。”此外,第三个参数alice_bob_k1ab用于区分不同的验证对:即,用于断言该值的解释目的。作为建模约定,通常将身份验证角色的名称,要身份验证的角色以及要检查的变量的名称(以小写形式)串联在一起。在顶层角色中,应将其声明为protocol_id类型的常量。因此,对请求的解释甚至更强,因为A不仅要求B存在并且同意该值,还要求B打算将其用于协议id alice_bob_k1ab。
划重点:
- 含义:alice希望确保该值确实是由bob创建的,是为她创建的
- 位置:我们在alice的最后一个过渡中编写了这一行
- 格式:身份验证角色的名称,要身份验证的角色以及要检查的变量的名称(以小写形式)串联在一起
还存在与弱认证相对应的请求。如果使用wrequest,则不会施加任何重播保护。以上面的示例请求事实为例,如果是wrequest,则将放宽B存在的要求。这样就足够了,B在过去的某个时候存在,并且当时已经同意了值K1ab',并将其解释为协议ID alice_bob_k1ab。
witness(B,A,alice_bob_k1ab,K1ab’)
含义:代理B断言我们要成为代理A的对等方,并在协议ID alice_bob_k1ab标识的身份验证工作中就值K1ab'达成一致。
安全目标书写格式
authentication_on bob_alice_nb
或者 weak_authentication_on
在我们的示例中,我们将witness和request用于三个目的: •alice根据Na的值对bob进行身份验证(之所以成立,是因为只有bob可以解密Na并将Succ(Na)发送回给alice), •bob根据Na的值对爱丽丝进行身份验证(之所以成立,是因为只有alice才能解密Nb并将Succ(Nb)发送回bob), •alice对K1ab的值进行bob身份验证。我们在这里滥用了对K1ab的强身份验证,以表示K1ab应该重新生成(而不是重播)
- 认证目标实际上是时间逻辑公式的宏。
- 请求事件之前总是伴随有见证人事件。先有witness后有request
- 在这种情况下,相伴表示这两个事实在协议ID和值上都一致,并且两个代理名称都被颠倒了。
- 而且,对于强身份验证,任何代理都不应两次从同一通信伙伴接受相同的值:也就是说,从请求事件之前的某个时间点开始,以前从未请求过相同的值。
划重点(witness):
- 含义:代理B断言我们要成为代理A的对等方,并在协议ID alice_bob_k1ab标识的身份验证工作中就值K1ab'达成一致
- 位置:首次见到要检查变量名的时候。如B首次收到Na的时候,A首次收到Nb的时候,B首次创建K1ab的时候。
- 格式:要身份验证的角色,身份验证角色的名称,以及要检查的变量的名称(以小写形式)串联在一起。 代理人与request相的,其它一致。
Detecting Replay Attacks
通常,重播攻击可以通过在相同代理之间指定多个并行会话来找到,就像在上述环境角色中声明的前两个会话一样。不幸的是,这可能会导致分析速度显着下降。
此外SPAN软件自带了重放检测的选项
通过会话编译,OFMC即使没有在a和b之间进行第二次并行会话,也可以找到重放攻击。这是因为它首先模拟整个系统的运行,然后在第二次运行中让入侵者利用在第一次运行中学到的知识
我们注意到,-sessco选项对于快速检查可执行性也很方便。但是,在当前版本中,只有在每个角色的状态变量从一个过渡到下一个过渡严格增加的情况下,它才有效。(自动生成的可行。按惯例写的不行)
- php-redis扩展模块安装记录
- [silverlight基础]仿文字连接跑马灯效果-高手绕道
- 未解决:长字符串含…
- Iptables防火墙规则使用梳理
- “正在注册字体”问题解决
- linux下安装php的swoole扩展模块(安装后php加载不出来?)
- linux下查询域名或IP注册信息的操作记录(whois)
- 域名资讯:多枚区块链域名结拍,区块链概念火热
- 一批好米交易:qrf.com15.4万元结拍
- mysql主从同步(2)-问题梳理
- 老丁独家!前方高能,与“程序崩溃”的第一次邂逅!
- 微信可接收火车购票、退票及改签等通知啦!别忘了,春运火车票下周开售!
- 如何用SPSS分析问卷?用SPSS分析调查问卷数据的方法
- 【5】基于Log4Net的日志系统
- 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 数组属性和方法
- python3用ARIMA模型进行时间序列预测
- R语言马尔可夫转换模型研究交通伤亡人数事故预测
- scrapy爬虫框架和selenium的使用:对优惠券推荐网站数据LDA文本挖掘
- 使用R语言进行Metroplis-in-Gibbs采样和MCMC运行分析
- R语言中的马尔科夫机制转换(Markov regime switching)模型
- R语言ARMA-EGARCH模型、集成预测算法对SPX实际波动率进行预测
- nginx快速入门
- R语言中进行期权定价的Heston模型
- 使用R语言随机波动模型SV处理时间序列中的随机波动率
- 20个ES6面试高频问题
- i++和++i傻傻分不清楚?这里给你最清楚的解答
- android APT 使用
- Flutter异步编程async与await的基本使用
- 教大家一个万能PPT图片排版技巧,太赞了!
- 重复读取 HttpServletRequest 中 InputStream 的方法