专栏首页认证协议的形式化分析形式化分析工具(六):HLPSL Tutorial(Example3)
原创

形式化分析工具(六):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。

划重点:

  1. 含义:alice希望确保该值确实是由bob创建的,是为她创建的
  2. 位置:我们在alice的最后一个过渡中编写了这一行
  3. 格式:身份验证角色的名称,要身份验证的角色以及要检查的变量的名称(以小写形式)串联在一起

还存在与弱认证相对应的请求。如果使用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应该重新生成(而不是重播)

  1. 认证目标实际上是时间逻辑公式的宏。
  2. 请求事件之前总是伴随有见证人事件。先有witness后有request
  3. 在这种情况下,相伴表示这两个事实在协议ID和值上都一致,并且两个代理名称都被颠倒了。
  4. 而且,对于强身份验证,任何代理都不应两次从同一通信伙伴接受相同的值:也就是说,从请求事件之前的某个时间点开始,以前从未请求过相同的值

划重点(witness):

  1. 含义:代理B断言我们要成为代理A的对等方,并在协议ID alice_bob_k1ab标识的身份验证工作中就值K1ab'达成一致
  2. 位置:首次见到要检查变量名的时候。如B首次收到Na的时候,A首次收到Nb的时候,B首次创建K1ab的时候。
  3. 格式:要身份验证的角色,身份验证角色的名称,以及要检查的变量的名称(以小写形式)串联在一起。 代理人与request相的,其它一致。

Detecting Replay Attacks

通常,重播攻击可以通过在相同代理之间指定多个并行会话来找到,就像在上述环境角色中声明的前两个会话一样。不幸的是,这可能会导致分析速度显着下降。

第一个会话与第二个会话完全一致

此外SPAN软件自带了重放检测的选项

通过会话编译,OFMC即使没有在a和b之间进行第二次并行会话,也可以找到重放攻击。这是因为它首先模拟整个系统的运行,然后在第二次运行中让入侵者利用在第一次运行中学到的知识

我们注意到,-sessco选项对于快速检查可执行性也很方便。但是,在当前版本中,只有在每个角色的状态变量从一个过渡到下一个过渡严格增加的情况下,它才有效。(自动生成的可行。按惯例写的不行

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

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

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 虚拟化资源管理阅读笔记(一)

    一种新的资源管理系统模型,并提出一种在云数据中心中进行有效的虚拟机分配的方法。从技术上讲,虚拟机分配问题正式化为装箱问题,而Best Fit算法(BF)被部署为...

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

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

    春风大魔王
  • uthentication Handover and Privacy Protection in 5G HetNets Using Software-Defin

    最近,通过共存的异构网络进行覆盖覆盖的密集小蜂窝部署已成为5G移动网络的可行解决方案。但是,由于5G小型蜂窝和HetNets中潜在的频繁切换和认证,这种多层体系...

    春风大魔王
  • motan入门

    叔牙
  • Oracle 还原历史统计信息

          统计信息是个非常有用的东东,没有它,SQL优化器就好比巧妇难为无米之炊!良好高效的SQL执行计划依赖于真实的统计信息。然而在有些情况下,比如对比生产...

    Leshami
  • 使用FME获取POI信息

    这篇推送,想法来源与群里的朋友。 作为数据处理从业人员,经常需要从互联网上采集一些数据,其中就包括一些POI。有时候数据的需求量不大,又懒得去写代码,就可以用F...

    数据处理与分析
  • 机器学习库初探之MXnet

    与其他工具相比,MXnet 结合了符号语言和过程语言的编程模型,并试图最大化各自优势,利用统一的执行引擎进行自动多 GPU 并行调度优化。不同的编程模型有各自的...

    吕晟
  • Databricks说的Lakehouse是什么?

    在过去的几年里,Lakehouse作为一种新的数据管理范式,已独立出现在Databricks的许多用户和应用案例中。在这篇文章中,我们将阐述这种新范式以及它相...

    大数据学习与分享
  • Jmeter+Shell,20分钟部署一整天的性能测试任务

    前几天接到一个性能测试任务,要求对语音识别服务进行性能测试。当拿到任务列表时,眼前的一幕...

    用户5521279
  • 2017年的Linux内核防护依然脆弱

    Linux 内核 “社区” 对待安全的优先级并不高,虽然经历了 2000 年代的多次大规模漏洞利用事件但并没有让 Linus Torvalds 本人改变 "A...

    小小科

扫码关注云+社区

领取腾讯云代金券