形式化分析工具（六）：HLPSL Tutorial

本文为阅读笔记。文章题目为： HLPSL Tutorial A Beginner’s Guide to Modelling and Analysing Internet Security Protocols

原文地址懒得找。需要原文，请关注公号：养两只猫。发送：HLPSL教程。

1 HLPSL Basics

VISPA提供了一种称为高级协议规范语言（HLPSL）的语言，用于描述安全协议并指定其预期的安全属性，以及用于正式验证它们的一组工具。

1.1 Using the A VISPA Tool

1.2 Basic Roles

如果首先以Alice-Bob（A-B）表示法编写协议，则将协议转换为HLPSL最简单。例如，下面我们用著名的A-B表示法 Wide Mouth Frog protocol

请注意，加密用大括号表示，加密密钥用_标识

LPSL是一种基于角色的语言，这意味着我们在模块中指定每种参与者的动作，这被称为基本角色。稍后，我们将实例化这些角色，并通过将多个基本角色“粘合”到组成角色中来指定结果参与者之间的交互方式。在对协议进行建模时，从以A-B表示法说明消息流开始，然后再进行基本角色的说明可能会有所帮助。对于协议中的每个参与者（类型），将有一个基本角色来指定其操作顺序。稍后可以由一个或多个扮演给定角色的代理实例化此规范。例如，在WMF协议的情况下，存在三个基本角色，我们称为alice，bob和server。我们注意到角色名称总是以小写字母开头。例如，我们使用名称alice来表示角色本身，而扮演该角色的代理的名称将称为A，就像上面的A-B表示法一样。

每个基本角色描述参与者最初可以使用哪些信息（parameters）它的（initial state)及状态改变的方式(transitions)， 例如，alice在上述协议中的角色可能看起来像这样：

HLPSL中的所有变量均以大写字母开头，所有常量均以小写字母开头。而且，所有变量和常量都被键入。

1.3 Transitions

1.4 Composed Roles

Composed roles instantiate one or more basic roles, “gluing” them together so they execute together, usually in parallel (with interleaving semantics). Once you have defined your basic roles, you need to define composed roles which describe sessions of the protocol. If we assume, in addition to the alice role we’ve already discussed, that we also have a bob and a server role with the arguments one would expect, then we can define a composed role which instantiates one instance of each basic role and thus describes one whole protocol session. By convention, we generally call such a composed role session.

最后，总是定义一个顶层角色。该角色包含全局常量和一个或多个会话的组合，入侵者可能在其中扮演合法用户的角色。还有一条陈述描述了入侵者最初拥有的知识。通常，这包括所有代理的名称，所有公共密钥，他自己的私有密钥，他与他人共享的任何密钥以及所有公共已知功能。请注意，常数i用于表示入侵者。例如：

2 HLPSL Examples

语法规则：形式化分析工具AVISPA（三）学习User micro-manual of AVISPA

2.1 Example 1 - from Alice-Bob notation to HLPSL specification

假设A和B共享一个秘密密钥K（即K是仅A和B知道的值）。考虑以下协议以产生新的共享密钥K1：

在Alice-Bob表示法中，其内容为：A向B发送一个用K加密的随机数Na。B然后将另一个也用K加密的随机数Nb发送给A。一起，并将用K1加密的Nb的值发送回B。

role alice(

A,B : agent,

K : symmetric_key,

Hash : hash_func,

SND,RCV : channel(dy))

played_by A def=

local

State : nat,

Na,Nb : text,

K1 : message

init

State := 0

transition

1. State = 0 /\ RCV(start) =|>

State’:= 2 /\ Na’ := new()

/\ SND({Na’}_K)

2. State = 2 /\ RCV({Nb’}_K) =|>

State’:= 4 /\ K1’ := Hash(Na.Nb’)

/\ SND({Nb’}_K1’)

/\ witness(A,B,bob_alice_nb,Nb’)

end role

role bob(

A,B : agent,

K : symmetric_key,

Hash : hash_func,

SND,RCV : channel(dy))

played_by B def=

local

State : nat,

Nb,Na : text,

K1 : message

init

State := 1

transition

1. State = 1 /\ RCV({Na’}_K) =|>

State’:= 3 /\ Nb’ := new()

/\ SND({Nb’}_K)

/\ K1’:= Hash(Na’.Nb’)

/\ secret(K1’,k1,{A,B})

2. State = 3 /\ RCV({Nb}_K1) =|>

State’:= 5 /\ request(B,A,bob_alice_nb,Nb)

end role

role session(

A,B : agent,

K : symmetric_key,

Hash : hash_func)

def=

local SA, SB, RA, RB : channel (dy)

composition

alice(A,B,K,Hash,SA,RA)

/\ bob (A,B,K,Hash,SB,RB)

end role

role environment()

def=

const

bob_alice_nb,

k1 : protocol_id,

kab,kai,kib : symmetric_key,

a,b : agent,

h : hash_func

intruder_knowledge = {a,b,h,kai,kib}

composition

session(a,b,kab,h)

/\ session(a,i,kai,h)

/\ session(i,b,kib,h)

end role

goal

secrecy_of k1

authentication_on bob_alice_nb

end goal

environment()

2.2 示例2-常见错误，不受信任的代理，攻击跟踪

使用CAS+语法. 进行编写

1.使用CAS+语法进行对协议建模

复现的时候记得把汉字删干净。好像是SPAN编码不识别。

2.使用SPAN进行转换。转换

与原文写的HLPSL对比。看一下差异大不大。体验用CAS描述协议是否能够达到预期的简便效果。

3.编写安全目标

用HLPSL语言进行编写。

语法规则请参考之前的文章。

谈一 谈个人对安全目标使用（secret、witness、request）的理解：

机密性：

secret(K’,k,{A,B,S})

含义：K'对于｛ABS｝而言都是保密的，记作k（标签）

位置：首次出现的时候就要声明

身份认证：

request(A,B,alice_bob_na,Na) A想验证NA是由B构建的

witness(B,A,alice_bob_na,Na’) B希望NA'能够得到认证

信息的机密性

在此处添加

2.2.1 建模技巧和陷阱

1.priming

正确设置参数比较难（貌似用CAS自动生成不存在这个问题，所以我也不研究这个问题了）

应该为Na‘

• 遵循这些简单的priming规则，有望帮助建模人员避免大多数与priming位置有关的问题。（以下内容为百度翻译）
• 1. 转换（->）左侧的变量通常是接收动作的参数。在这种情况下，素数变量（例如X'）将被分配给消息中接收的值。unprimed的变量（例如X）将限制接受的消息。例如： RCV（A.X'） 这将出现在过渡的左侧，并且仅当收到的消息是一对其第一部分与当前值匹配的消息时才启用过渡如果触发了转换，则转换完成后，X的值将等于在消息的第二部分中发送的值。
• 2.在过渡的右侧，为变量分配新值时，请使用素数变量名称和赋值运算符：=。例如：State’：= 3 在生成和使用随机数时也是如此，例如： Na':=new()
• 3.质数X'是X的新值 转换中指定的所有状态更改会同时发生。因此，假设您有一个这样的过渡，在该过渡中，代理会收到一些值并简单地将其转发：RCV（X’）= |> SND（X）在此，两个变量都必须primed。否则，您将发送X的当前（旧）值，而不是转发新接收的值。

2. Variable Sharing

在这里，我们不参考前面的示例中讨论的对共享的初始知识进行建模的问题。相反，我们的意思是共享变量。例如，在此示例中，这三个角色中的每个角色都有一个称为K的局部变量。但是，由于这不是一些先验知识，必须作为协议的一部分进行协商，因此它们不宜共享该变量。因此，每个角色都应拥有自己的变量副本，以使我们能够看到此信息可能不正确对应的情况（可能表示攻击的情况）。

事实上，在HLPSL中，变量（具有更改能力）无法共享。3但是，当您要求角色具有预共享的知识时，共享（恒定）值是适当且可行的，例如，共享密钥。如上例所示，这是通过将要共享的值作为参数传递给多个角色来实现的。

3. Commas vs. Periods （CAS自动转换也不存在这个问题）

重要的是要注意使用逗号“，”和使用句点“。”之间的区别。在HLPSL规范中。

在表示复合消息时，应该始终使用句点，因为它们表示（子）消息的串联，例如从频道发送或接收时：SND（A.B.Na’）

类似地，在将消息作为函数调用中的参数进行连接时，应使用句点来形成一条消息，如在前面的示例之一中，已建立的键是通过获取两个随机数的哈希值来计算的：Hash（Na .Nb'）。

当分隔谓词，角色或目标事件的不同参数时（在下面的示例中讨论），应使用逗号，例如：server（A，S，B，Ka，Kb，SAS，RAS）

4.复合类型和建模转发（ Compound Types and Modelling Forwarding ）

在Kerberos样式的协议中，经常出现一种情况，即一个代理收到一条消息，其中有一些消息她实际上无法解密。相反，代理应将这些部分转发给其他人。协议建模者当然知道该消息的格式，并且可以指定转发代理的转换，就像她只是在接收消息一样。例如，您可以按照上述说明写出爱丽丝的第二次转换：

State=1 /\ RCV(A.B.{K'.Na.Ns'}_Ka.{K'.Na.Ns'}_Kb') =|>

State':=2 /\ SND(A.B.{K'.Na.Ns'}_Kb'.{Na.Ns'}_K')

我们更喜欢以一种不同的方式编写这样的转发过渡，这种方式旨在忠实地模拟协议的方面，即alice不能真正解密消息的后半部分的内容，因为它已用Kb加密。相反，我们想写的是alice收到（A.B. {K’.Na.Ns’} _ Ka.X’），其中X’只是alice无法理解的一些数据。她希望它的格式为{K'.Na.Ns'} _ Kb（对于某些Kb），但是即使她知道纯文本（K'.Na.Ns'），也无法将X'与{K' .Na.Ns'} _ Kb，因为她不知道密钥Kb。 因此，我们宁愿将过渡编写如下：

其中X是用于代替{K'.Na.Ns'} _ Kb的局部变量，因此X应该以复合类型{symmetric_key.text.text} _symmetric_key的形式声明，因为要接收的值具有以下形式：对称密钥和两个比特串，由对称密钥共同加密。

5. Assigning State Numbers

在示例2中，我们可以看到状态数字对于Alice是偶数，对于Bob和Server是奇数。我们通常以这种方式分配状态编号，以反映发送和接收事件的预期顺序。但是，这不是强制性的，而是一种方便的建模约定，可以在读取HLPSL和后端打印的迹线时使事情保持清晰。

个人理解 ：之前纠结过一会，不知道状态值是什么意思。经自己研究发现，状态值是针对每个角色自己的与其它角色无关。用CAS自动转换就可以发现状态值都是从0开始，单独看每个角色就是每个角色的状态。只是用奇偶分别对应两个角色确实能够更直观的感受协议交互的顺序流程。

6.Executability

不可执行情况，详见3.9。不可执行性的另一个潜在来源是入侵者的知识不足。特别是当他扮演诚实代理人的角色时。因此，请确保在环境角色的intruder_knowledge = {...}声明中包括所有相关值。

2.2.2 讨论与分析结果

角色的参数定义了信息的开头，并作为组成角色的参数传递。例如，会话角色用于描述协议的单个执行。会话角色将三个角色组合在一起，并通过将每个角色作为参数传递来定义每个角色的信息。

environment role是顶级角色，它描述了三个并发会话（针对本例子）。第一个是与合法代理a，b和s进行的典型会话。请注意，在环境角色中，所有参数均小写。这是因为它们是常量而不是变量。

第二和第三次会话是入侵者冒充爱丽丝或鲍勃的行为。从这些会话的参数中可以看出，入侵者（i）扮演着合法用户的角色，目的是攻击协议。他甚至与服务器（ki）都有一个共享密钥，可以与之定期进行通信。

使用AVISPA工具分析协议的此模型时，以下输出结果（此处显示的输出已格式化为适合页面的格式）：

工具输出显示已发现该协议不安全，并且已发现攻击。可以安全地忽略大多数输出​​，但是最有趣的输出是攻击跟踪本身。在“攻击跟踪”标题下显示，它显示了导致攻击的消息交换：即，违反了给定目标“ authentication_on alice_bob_na”。现在，我们将更详细地检查攻击踪迹。入侵者通过发送特殊的启动消息来发起与代理a的第一次会话。由于与hlpsl2if转换器和A VISPA后端的内部工作相关的原因，每个角色实例均分配有一个会话号：在这种情况下为“ 3”。

i->（a，3）： 回复入侵者。请注意，因为我们假设入侵者是网络，所以所有消息都会通过入侵者，即使他可能不是预期的收件人。在这里，我们从消息的第二部分可以看到a实际上希望与代理b交谈。我们还注意到，新生成的术语用其变量名和用于唯一标识它们的数字表示。在这种情况下，这是任何代理首次生成一个称为Na的随机数，因此该值由Na（1）表示。 （a，3）-> i：a.b. {Na（1）} _ ka

然后，入侵者将消息转发到s（更确切地说，已分配了会话号7的s的实例）。但是，入侵者已在消息的第二部分中插入了自己的名字，告诉s a希望与i交谈而不是与b交谈。请注意，入侵者并没有破坏加密，只是将加密的数据复制到了新消息中。 i->（s，7）：a.i. {Na（1）} _ ka 此处b已经被替换为i了 答复入侵者具有适当的响应，包括用s和入侵者之间共享的密钥ki加密的随机数。入侵者现在已经知道了这些随机数以及K（2），这是会话密钥，a会相信a可以用来与b对话。 （s，7）-> i：a.i. {K（2）.Na（1）.Ns（2）} _ ka.{K（2）.Na（1）.Ns（2）} _ ki

入侵者偷偷地将对应方的名称切换回b，以便a都不是更明智的选择，并将从s接收到的消息部分转发到a。消息的最后部分x61是与OFMC后端的内部工作有关的变量，尤其是与称为惰性入侵者的技术有关的变量[6]。直观地讲，变量的存在意味着入侵者为该消息部分发送什么都无所谓，因为接收代理实际上不会检查其中的内容。 i->（a，3）：a.b. {K（2）.Na（1）.Ns（2）} _ ka.x61 入侵者偷偷地将对应方的名称切换回b 现在，a将使用入侵者密钥加密的随机数发送给b ，但它们再次被入侵者拦截。请注意，a仍然认为她用于加密的密钥K（2）实际上与b共享。 b，但是，甚至还没有参加。 （a，3）-> i：abx61。{Na（1）.Ns（2）} _ K（2） 现在，入侵者可以轻松地解密这些值并将其发送回加密状态使用新的会话密钥K（2）。这使协议运行结束，并且她发出了她的“请求”事实（在下一个示例中讨论），该事实断言她认为自己正在与b对话，而实际上她正在与入侵者对话！

i->（a，3）：ab {Ns（2）.Na（1）} _ K（2） 因此，很明显，上述安全目标“ authentication_on alice_bob_na”确实遭到违反。

2.3示例3-安全目标

下一篇我们将讨论第三个例子

现在我们转到第三个示例，在该示例中我们将讨论如何指定协议的安全目标。