形式化分析工具（六）：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选项对于快速检查可执行性也很方便。但是，在当前版本中，只有在每个角色的状态变量从一个过渡到下一个过渡严格增加的情况下，它才有效。（自动生成的可行。按惯例写的不行）