理论计算机科学电子笔记135（2005）59-77www.elsevier.com/locate/entcs面向HLPSL规范语言阿列克谢·戈茨曼1 法比奥·马萨奇1马尔科·皮斯托雷1文凭Informatica e Telecom.Universit`adiTrentoTrento，意大利摘要我们提出了一种算法，用于将在AVISPA项目框架内开发的HLPSL语言中的安全协议规范翻译为应用pi演算的方言。该算法为我们提供了两个有趣的科学贡献：首先，它提供了HLPSL规范语言的独立语义，其次，可以使用基于pi演算的ProVerif工具验证HLPSL中指定的协议。我们的技术已经在各种安全协议上实现和测试。该翻译可以处理HLPSL中建模的大部分协议。关键词：安全协议，验证，规范语言，进程代数1介绍在过去的几十年里，人们对安全协议的验证非常感兴趣。在几乎每一个理论计算机科学会议上，都有关于（不）可判定性结果的论文，自动推理和安全会议显示，关于将这种或那种验证技术应用于这种或那种安全协议的论文源源不断。这一稳定的结果流与一个同样混乱和不守规矩的协议规范语言家族相匹配。这些建议1电子邮件：{gotsman，massacci，pistore}@ dit.unitn.it1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.06.00460A. Gotsman等人理论计算机科学电子笔记135（2005）59基本上是出于共同的关注[2]：... 在过去十年中，安全协议的形式化验证成为密集研究的主题. .然而，很明显，形式化过程本身是设计过程中的一个严重瓶颈。首先，形式化协议很难由不同于形式化方法本身的提出者的人来实现。第二，协议目标的模糊性使得有可能用安全分析师永远不会认为是正式的方法来发现“攻击”。].事实上，安全分析师可以很容易地根据发送，接收和丢失的消息来定义因此，规范语言的目的本质上是缩小安全研究论文和标准机构中指定协议的非正式语言与正式验证专家使用的正式语言之间的差距。在文献中提出的数不清的规范语言中，我们引用了ALSP [2]，BRUTUS [11]，CAPSL及其变体[8，9]或其中间格式CIL [12]，CASPER [19]，CVS [14]，HLPSL[10]，NAPTRL [21]，应用的基于pi演算的规范语言，包括ProVerif [6]，只是基于不同目标验证技术的几个建议。回顾这些规范语言，公平地说，除了提出者或他们的密切科学合作者之外，他们很少享有广泛的分歧。起初，人们可能会认为这是由于各种语言的不同表达能力。然而，这只适用于一般的编程语言。相反，在这里，我们有许多不同的语言用于相同的专门应用领域，而且，用于几乎相同的协议集。我们认为，许多特定语言缺乏区分的主要原因是缺乏独立动机和文档化的语义。不严格地说，唯一可用的翻译是（没有很好的记录）翻译成作者 在某些情况下（E。G. CASPER），协议描述需要作者的目标方法的直接知识和结构输入。结果是，使用不同的方法作为目标将是相当困难的。在AVISPA项目2的框架中开发的高级协议规范语言（HLPSL）是一个例外。实际上，虽然它保持了从协议描述语言到2http://www.avispa-project.orgA. Gotsman等人理论计算机科学电子笔记135（2005）5961对于提议者HLPSL语言是AVISPA工具的输入语言。更详细地说，AVISPA工具将HLPSL规范作为输入，将其转换为IF，并通过调用最先进的后端来分析结果，这些后端将攻击（如果有的话）返回给用户。由于不同的工具适用于解决不同的问题，因此将HLPSL与其他工具集成以验证安全协议是相关的。到目前为止，AVISPA工具的可用后端基于三种不同的技术，这些技术覆盖了安全协议验证研究领域的很大一部分：• 有界模型检验和满意度[3];• 在线模型检验[5];• 项重写[17];• 抽象验证[7]。撇开静态验证技术不谈，这个列表中主要缺少的是基于进程代数的方法。在本文中，我们提出了一种将HLPSL子集中的规范转换为ProVerif工具支持的应用pi演算方言的方法[6]。这使得可以通过对转换结果调用ProVerif来验证 HLPSL规范的保密性、弱身份验证和强身份验证属性它完成了一些可用的形式化和技术可用于HLPSL。它还有另一个优点：在现有的TLA规范草案的基础上，我们提供了一个基于HLPSL的应用π演算翻译的独立语义这种独立的语义也可以用来澄清原始规范草案中的一些模糊之处。事实上，我们在热那亚大学AVISPA项目成员的支持下完成的翻译工作，指出了规范中的一些语义问题和临时数新鲜度的初始语义草案中的错误。我们的翻译直接基于源HLPSL语言和TLA语义，而不是“专有”IF语言，因为在翻译到IF语言时可能会丢失一些属性。 这种方法可以独立地检查HLPSL规范中的语义错误以及从HLPSL到IF的转换：协议攻击必须在原始AVISPA工具和我们提出的组合验证技术中得到反映。本文的结构如下。 第2节介绍了62A. Gotsman等人理论计算机科学电子笔记135（2005）59角色B（F）由pldef扮演=角色P（F）def=init初始化常量C局部L合成接受AccR1（A1）指令... Rn（An）过渡端角色lb1.ev1=|>act1lb2.ev2=|>第二幕...磅，磅; evn=|> actn.端角色Fig. 1. HLPSL角色我们使用的HLPSL。在第3节中，我们描述的方言的应用π演算的翻译是执行。第四节描述了翻译的目的.第5节解释了如何ProVerif可以用来验证翻译的结果，而第6节给出了一些细节的实施和实验结果的选择加密协议，在HLPSL的AVISPA项目的框架中建模。2HLPSL语言在本节中，我们简要描述了由我们的翻译算法处理的HLPSL的子集。我们建议读者参考[10]以获得对该语言的更全面的描述。HLPSL中的协议规范分为不同的角色。一些角色（所谓的基本角色）用于描述协议或子协议运行中单个代理的动作。其他的（组合角色）实例化基本角色来模拟整个协议运行、多个代理之间的协议会话或协议模型本身。这个角色被称为主要角色。图1显示了HLPSL中基本角色（用B表示）和组合角色（用P表示）的结构。F是形式参数的集合，L是局部变量的集合，pl是扮演B的主体。 我们要求F L=。在HLPSL中，变量和常量都是类型化的。 我们将使用以下类型：代理、通道、公钥、文本、NAT、布尔、对称密钥、消息、函数、协议ID。某些类型（文本和通道）的属性可能包含在括号内。例如，text（fresh）表示新生成的随机数的类型，channel（dy）表示对应于Dolev-Yao（DY）入侵者模型的通道类型[13]。在我们A. Gotsman等人理论计算机科学电子笔记135（2005）5963t：：=HLPSL术语V变量变量Vc的新值t1.t2t1和t2的级联{t1}通过密钥t2 对消息t1进行t2f（t）将存储在变量或常量f中的函数（函数类型）应用于项tinv（t）对应于公钥t图二. HLPSL术语HLPSL的子集，我们只考虑DY通道，因此默认情况下，所有通道都隐式具有dy属性。HLPSL中的术语如图2所示。这里VJ是用于表示执行转换后变量V的值，而V表示执行前变量的值。此外，对于具有新鲜属性V的变量V，J表示针对这个变量。还请注意，{t1}t2被认为是公钥加密，如果t2是x或inv（x），其中x是公钥类型的变量或常数，否则是共享密钥加密。在前一种情况下，t2被称为公钥表达式。init部分将初始值分配给局部变量，并具有以下结构：ΔnInit=i=1（Vi=ci）其中Vi是变量，ci是常数。设I为init部分中赋值的变量集我们要求我去。转换由标签lbi、触发事件evi和动作acti定义。每次转换在其守护事件谓词满足时触发，并立即触发在满足少数事件的情况下，非确定性地选择并执行对应于它们的转换之一我们要求每个基本角色都有一个nat类型的局部变量State直观地表示协议参与者的状态，64A. Gotsman等人理论计算机科学电子笔记135（2005）59我evi和acti具有以下形式Δ动作 状态J=sΔevi=State=sCompRMsg∧SMsg ∧Ass ∧W itness ∧W Request ∧Request ∧Secreti=1(the而《易经》中的卦序，则是没有定数的，而是定数的。我们还要求State ∈I。值得注意的是，HLPSL规范并没有对跃迁的形式做出这样的限制，但我们发现这个假设非常有用。每个角色都有自己的状态显式声明的要求允许我们优化HLPSL规范的转换，并将验证结果映射回协议域。此外，我们发现所有公开可用的HLPSL规范都是以刚才所说的方式使用状态变量现在让我们描述一下过渡的各个部分一种是比较，一种是比较，ΔnComp=（ti=mi）i=1其中ti和mi是不带素变量的HLPSL项。RMsg和SMsg分别是接收动作和发送动作的集合。它们具有以下形式：ΔnRMsg=i=1Δnci（ti）SMsg=i=1di（mi）其中ci和di是通道类型的变量或常数，ti和mi是HLPSL项。Ass是新值到变量的赋值集合，具有以下结构：Δn屁股=i=1（VJ=mi）其中Vi是变量，mi是HLPSL项。Witness、W Request、Request和Secret分别是witness（a，b，p，m）、wrequest（a，b，p，m）、request（a，b，p，m）和secret（m，a）形式的表达式的合取。这些表达式被称为目标事实，A. Gotsman等人理论计算机科学电子笔记135（2005）5965用于表示正确性要求。直觉上，一个进球事实是一个预言，当他出现在右手边的那一刻，这个预言就变成了现实正在执行的过渡。这里a和b是代理类型的变量或常量，m是HLPSL项，p是协议标识符-在主角色中声明并使用的协议id类型的实例以确定对应于目标事实的正确性要求。直观地说，witness（a，b，p，m）意味着代理a希望使用m作为身份验证标识符的值与代理bp. wrequest（a，b，p，m）或request（a，b，p，m）意味着代理a接受值m，现在依赖于b存在的保证，并同意他对认证标识符p的这个值。使用wrequest还是request取决于正确性需求的类型（参见第5节）。我们在验证弱认证时使用wrequest，在验证强认证时使用request。secret（m，a）意味着角色的诚实参与者声称项m是代理a被允许知道。accept部分的格式为ΔAcc=State=sa其中SA是对应于角色参与的协议的成功完成的状态。在组合角色中，我们没有过渡部分。相反，我们有一个名为复合的部分，它实例化并行运行的其他角色Ri（带有参数集Ai）此外，一个组合角色可以定义一组常数C。此外，主角色必须声明了代表入侵者的类型代理的常量i它还可以有一个形式为knowledge（i）=K的声明，它描述了入侵者的初始知识。这里K是HLPSL项的集合。协议的正确性要求，称为目标，在它们自己的部分中给出。支持三种类型的目标• HLPSL术语m的保密性：m的保密性。这意味着m必须不为入侵者所知。• 弱认证：A在p上弱认证B。 这意味着每当扮演角色B的代理b执行wrequest（b，a，p，m）时，a=i或a是扮演角色A的代理并且witness（a，b，p，m）之前已经执行过这对应于Lowe• 强认证：A在p上认证B。相对于66A. Gotsman等人理论计算机科学电子笔记135（2005）59t：：=项x变量f（t1，.，tn）构造函数应用程序P：：=进程零死锁x的！直流电压输出x？（y）.P输入如果t1=t2则P，否则Q比较ift1t2thenPelseQ比较P1|P2并行合成P1+P2选择（v x）P限制令x = g（t1，.，tn）在P else Q 析构函数应用程序中事件e（t1，. ，tn）.P事件e事件exe（t1，. ，tn）执行的事件e图三.目标语言前面的目标增加了这样的要求，即由扮演B的代理执行的每个wrequest对应于由扮演A的代理执行的唯一见证。这对应于Lowe3目标应用Pi演算作为我们翻译的目标语言，我们使用与[1]中提出的类似的应用pi演算的方言。这种方言通过归约关系扩展了经典的定义密码原语的pi演算其语法如图3所示。变量x在过程x？（y）.P，（νx）P，和令x = g（t1，.，tn）inPelse Q我们将使用（νM），其中M={x1，.，xn}，作为（νx1）的语法糖... （vxn）A. Gotsman等人理论计算机科学电子笔记135（2005）5967元组构造函数：tuple，n tuple（t1，...，tn）析构函数：投影，i th n（n tuple（t1，.，tn））→ ti共享密钥加密构造函数：用密钥t2加密t1，sencrypt（t1，t2）析构函数：解密，sdecrypt（sencrypt（t1，t2），t2）→t1公钥加密构造函数：用公钥t2加密t1，pencrypt（t1，t2）私钥，对应于公钥t，inv（t）析构函数：decryption，pdecrypt（pencrypt（t1，t2），inv（t2））→t1单向散列函数构造函数：函数f对项t的应用，hashfun（f，t）见图4。构造函数和析构函数并且令x = g（t1，.，tn）inP as syntax sugar for令x = g（t1，.，tn）inPelse nil语法假设定义了一组构造函数、析构函数和事件。构造函数用于构建术语。析构函数在进程中用于操作术语。它们是过程可以应用的条件上的部分函数。该过程令x = g（t1，.，tn），否则Q尝试评估g（t1，.，tn）;如果成功，则x绑定到结果，并执行P，否则执行Q。g的求值由一组形式为g（t1，.，tn）→ t.我们使用析构函数，而不是应用函数的等式理论，因为这种方法允许更有效的验证，并且在ProVerif工具中使用，我们的翻译结果被验证。为了我们的翻译，我们定义了构造函数和析构函数来表示数据结构和加密原语，如图4所示。我们定义let（x1，.，xn）= tinP作为语法糖，设x1= 1th n（t）in. 设xn=n thn（t）在P此外，我们将对n元组（t1，...，tn）到（t1，.，tn）。68A. Gotsman等人理论计算机科学电子笔记135（2005）59（P|Q）|RP|（Q|R）P| 0元（νa1）（νa2）P（νa2）（νa1）P！PP|！P（P+Q）+RP+（Q+R）P+0P（νa）（P|Q）可持续发展|（νa）Q，如果a在P中不是自由的图五.结构叠合一个！⟨t⟩.Q|是吗？（x）.P→ Q|P {t/x}P→QP|R→ Q|RPJ<$P，P→Q，Q<$QJ<$PJ→QJP→Q<$（νa）P→（νa）Q如果t=t则PelseQ→P令x=tinP→P{t/x}如果t1=t2则P，否则Q→Q，如果t1如果ti=t，则P，否则Q→Qt2P→Q→P+R→Q+R如果t1 t2则P，否则Q→P，如果t1/=t2令x = g（t1，.，tn），否则Q→P{tJ/x}，如果g（t1，.，tn）→ tJ令x = g（t1，.，tn）inPelseQ→ Q如果不存在tJ使得g（t1，.，tn）→ tJ事件e（t1，.，tn）.P→事件exe（t1，.，tn）|P见图6。减少事件用于身份验证目标。eventex结构用于记住执行了哪些事件。我们定义了三个事件（witness、wrequest和request），每个事件有四个参数，它们对应于具有相同名称的HLPSL目标事实此外，我们定义事件参与者（a，r）意味着代理人a扮演角色r。这些事件的作用将在后面几节中变得清楚。形式语义的应用π演算给出的结构一致性和减少。所应用的picalculus的结构同余是满足图5中的方程的最小同余。图6列出了约简的公理。我们也让inv（inv（t））=t。4翻译算法HLPSL规范中的组合角色的翻译是通过从主要角色开始关注其结构来这样，我们得到A. Gotsman等人理论计算机科学电子笔记135（2005）5969仅使用常量作为参数的基本角色的实例化。我们对基本角色的转换使用State变量。一个基本角色被转换为一组进程，每个进程在特定状态下充当角色关于翻译算法，有两个重要的细节需要注意。首先，由于我们使用DY入侵者模型，因此我们从哪个通道接收消息或向哪个通道发送消息是无关紧要的。因此，在接收和发送动作的转换中，我们从预定义的通道c接收消息和向预定义的通道c发送消息，这是一个未知的自由常数。入侵者其次，我们将使用pi演算的限制运算符来模拟具有fresh属性的变量的新值现在我们将描述翻译算法。我们将HLPSL规范的片段R的翻译表示为（R），并将使用第2节中介绍的HLPSL规范的部分表示法。首先，我们描述了HLPSL术语的翻译。它们的翻译是根据它们的结构来定义的：Δ j Δ（五）= V，<$V）= V，<$c）= c，<$t1. ... .tn）=（<$t1），.，tn））⎧如果t是公钥表达式，则为Δpencrypt（<$m），<$t）<${m}t）=sencrypt（<$m），<$t）），否则Δ Δ<$f（t））= hashfun（<$f），<$t）），<$inv（t））= inv（<$t））HLPSL规范中组合角色的实例化形成了一棵树，以main role作为根。为了翻译组合角色，我们通过重复地将组合角色的文本替换为它们的实例化，将实际参数替换为形式参数，并使用pi演算的并行组合运算符来翻译角色实例化的并行组合此外，为了避免名称冲突，我们将组合角色中声明的所有常量重命名，并将它们声明为入侵者未知的自由此外，对于每个基本角色实例化，我们引入一个常量，表示该实例化的标识符我们为每个基本角色添加一个形式参数SID，并在每个实例化中为该参数分配实例化我们在翻译强身份验证目标时使用实例化标识符完成这些初步步骤后，我们可以通过以下方式生成主角色（以及所有组合角色）(i) 首先，我们生成一个输出初始知识的过程，70A. Gotsman等人理论计算机科学电子笔记135（2005）59频道C上的入侵者：其中{t1，.，tk}= K。c！快一..... 点！tk(ii) 其次，对于每个基本角色R，我们引入一个未知的自由常数，代表这个角色的标识符。由于在重新分配后，我们只获得了基本角色的实例化，并将常量作为参数，因此我们可以为每个基本角色确定（使用played by声明）扮演该角色的代理集。 对于每个基本角色标识符r和每个代理a扮演用r表示的角色，我们生成以下形式的过程：事件播放器（a，r）并将它们（以及上一步中获得的过程）与。操作符.(iii) 最后，我们使用let操作符为基本角色的形式参数赋值，输出组合角色树的重命名结果。一个基本角色B被转换为以下过程：ΔB =（VL I）（Bs0{c1/V1，.，cn/Vn}）其中s0是在init部分中给State变量的值，Vi是在init部分中由ci初始化的变量。对于状态变量的每个值s，在角色的HLPSL文本中分配给它，我们创建一个进程Bs，作为状态s中的角色。 让Tr（s）是在其左手侧具有合取State=s的所有转换的集合，并且令Nk是由第k个转换更新的新鲜变量的集合（i.e.具有fresh属性并且在转换的右侧被启动的然后ΔBs= Σk∈Tr（s）<$evk）（νNk）<$actk）事件和行动的转换定义如下：Δ<$State=sCompRMsg）=<$Comp）<$RMsg）Δ状态=s1（SMsg消息）（Ass）（请求）（秘密）=（Witness）。<$Ass）<$SM sg）。请求）。请求）。加密状态=s1）此外，我们定义Bsa=nil，其中sa是accept部分中State变量的值A. Gotsman等人理论计算机科学电子笔记135（2005）5971我我让我们来描述一个过渡部分的翻译。 Comp的翻译如下：Δ<$Comp）=如果<$t1）=<$m1）那么. 如果<$tn）=<$mn），则在我们对接收动作的翻译中，我们首先接收到新创建的变量的消息这个过程的后一部分由映射M（·，·）定义，其中第一个参数是接收项所绑定的名称，第二个参数是描述其结构的HLPSL项。I. e.△c？（t）。... .c？（t）。M（t，t）. ... . M（t，t）=1n1 1nn如果ti是一个带素数的变量，那么ti就是这个不带素数的变量。另一方面，它是一个新的变量，以前在翻译过程中没有使用过。M（·，·）根据HLPSL项的结构定义如下：M（m，m....... mΔM（m，V）=如果m=V，则ΔM（m，c）=如果m=c，则Δm，. ，m）= m in M（m，m）. M（m，m）1n）=let（1n11nnΔM（m，{t}x）=如果x是公钥表达式，则在M（t，t）中，设t= pdecrypt（m，inv（x））在M（t，t）中，设t= sdecrypt（m，x），否则m和t的定义与之前相同（关于mi和t）。此外，M（m，VJ）产生空公式并被丢弃。SMsg的翻译定义如下：Δ<$SMsg）=c！.............. 好吧！mn）我们将驴的翻译定义为Δ<$Ass）=令V1=<$m1）in. 设Vn=（mn），witness和wrequest目标事实按以下方式Δ事件见证（a，b，p，m））=事件见证（a，b，p，<$m））Δ<$wrequest（a，b，p，m））=事件 wrequest（a，b，p，<$m））72A. Gotsman等人理论计算机科学电子笔记135（2005）59请求目标事实具有以下翻译Δ请求（a，b，p，m））=c！sencrypt（（a，b，p，m，SID），sencrypt key）.eventrequest（a，b，p，m））这里的keys是入侵者未知的自由常数一个连词G1... 证人、wrequest和request目标事实的证据Gi被翻译成<$G1）<$Gn）。转换的其余部分的平移由以下递归方程定义：Δ秘密（m，a1）secret（m，an）=如果1我就。 如果ani= i，则（c！sencrypt（rm，<$m））。（R））否则R）. 否则（R）Δ状态=s1）=Bs1这里R是HLPSL表达式的合取，rm是为每个消息m创建的特殊常数，该消息m被声明为秘密的，并且用于制定保密目标。在翻译Secret时，我们通过正在被秘密化的表达式来分组秘密目标事实。请注意，我们必须保护每个事件，并限制参与者都不是入侵者i，因为正确性要求在这种情况下毫无意义。我们可以创建一个额外的进程，定义为（R），以避免代码的重复。值得注意的是，目前HLPSL的语义没有明确定义。因此，在某些情况下，我们必须决定如何解释HLPSL结构。在这种情况下，我们试图遵循AVISPA工具中实现的语义。例如，在我们的HLPSL子集中，不可能对角色通过通道接收私钥然后使用该私钥解密消息的情况进行e.角色具有静态知识。这是因为私钥必须在角色执行之初就为角色所知，并使用inv构造函数写入角色的文本中。这与AVISPA工具兼容，AVISPA工具目前不支持处理此类情况。我们必须解决的另一个问题是，是否应该在每次执行包含变量的转换时或每次实例化角色时生成具有fresh属性的变量的值在我们的翻译中，每次执行转换时，我们都会在应用的pi演算中创建新名称的值。A. Gotsman等人理论计算机科学电子笔记135（2005）59735ProVerif验证上一节中描述的翻译结果可以使用ProVerif工具[6]进行验证，ProVerif工具是一个定理证明系统，它基于一组Horn子句（逻辑程序）对协议的中间表示。ProVerif的输入语言与第3节中描述的输入语言相似。这两种语言之间的差异如下。ProVerif不支持+运算符，但支持let运算符中的内置unification。此外，ProVerif允许在规范中声明自由名称，这些名称可以是公共的（入侵者已知）和私有的（入侵者未知）。ProVerif中入侵者的模型是DY，但有些构造函数可以声明为private，这样入侵者就不能使用它们来创建新消息。此外，ProVerif允许指定项之间的等式。然而，ProVerif中对方程的处理仍然是初步的，这可能导致在某些情况下该工具无法终止。ProVerif允许指定不同类型的目标（称为查询）。在我们的翻译中，我们将只使用其中的一部分。数据库是根据事实建立的，可以有以下形式：• 攻击者：t-为真，当且仅当入侵者可能知道t。•t1=t2• ev：f（x1，.，xn）为真，当且仅当事件f（x1，.，xn）已被执行。给定事实F和Fi，j（1≤i≤k，1≤j≤ki），我们可以构造一个查询F==>（F1，1&. & F1，j1）| ... | (Fk,1&... &Fk，jk）这是真的当且仅当，当F是真的，那么对于某些i Fi，m是真的，对于所有m使得1≤m≤ji.查询也可以是事实F。例如，查询查询攻击者：t当入侵者可能知道t和查询时，查询ev：f1（x1，.，xn）==>ev：f2（y1，.，yn）如果事件f1（x1，. ，xn）已被执行，则事件f2（y1，.，yn）必须在它之前执行。在我们的翻译中，我们将inv声明为私有构造函数，方程为inv（inv（x））=x，通道c为公共自由名称，所有其他常量为私有自由名称。74A. Gotsman等人理论计算机科学电子笔记135（2005）59HLPSL中m的保密目标保密被翻译为查询攻击者：rm因为根据转换算法，当且仅当入侵者知道m时，它才能知道rm。需要rm是因为在查询中需要一个自由名称，而声明为secret的术语不能用于此目的，因为它们是在进程内部创建的。在HLPSL中，弱认证目标A在p上弱认证B被转换为以下形式的查询集：query ev：wrequest（b，y，p，x）==>（ev：witness（y，b，p，x）&ev：player（y，aid））|y = i。对于扮演角色B的每个代理B。在这里，援助是角色的角色标识符，A.扮演角色的主体和角色标识符在翻译组合角色时确定。在这个查询中，我们必须将变量y作为wrequest的第二个参数，而不是代理扮演角色A，因为我们必须考虑wrequest是用不存在的代理（由入侵者创建）作为其第二个参数。强认证目标A在p上认证B被转换为查询集合，该查询集合包括用于对应的弱认证目标的查询（其中request代替wrequest）和以下形式的queryattacker：（sencrypt（（b，a，p，x，y1），sidkey），sencrypt（（b，a，p，x，y2），encrypt key））==> y1= y2.对于每个代理b扮演角色B和代理a扮演角色A。由于sencrypt（（b，a，p，x，y），sencrypt key）形式的消息仅在执行相应的请求事件时发送，因此这些额外的查询确保在两个不同的会话（由不同的SID值y1和y2定义）中没有数据会被用于身份验证两我们必须使用queryattacker：t形式的查询，因为ProVerif不允许在==>操作符. 我们必须使用私钥加密请求不为入侵者所知，因此入侵者无法使用它们。我 们 的 实 现 将HLPSL 规 范 从 第2 节 中 描 述 的HLPSL 子 集 转 换 为ProVerif语言。由于ProVerif不支持+运算符，因此只能对最多在一次转换中具有联合状态的角色，S. 然而，这足以验证所建模的大多数协议在HLPSL。A. Gotsman等人理论计算机科学电子笔记135（2005）59756实施和实验我们已经实现了前面章节中描述的翻译，并使用ProVerif来验证生成的规范。我们的实验结果总结在图7中。作为AVISPA项目的一部分，在HLPSL中建模的一些协议上测试了该实现[4]。 对于每个协议，该表显示了其短名称（如[4]中所示），将其转换为应用的pi演算并使用ProVerif进行验证所需的时间，验证的属性数量，身份验证目标的类型（弱或强）以及是否发现任何攻击。测试在运行Red Hat EnterpriseLinux 3.0的2个Intel Xeon 3.2Ghz处理器的计算机上进行。我们的翻译器是用GNU C++ 实现 的， 我们 使用的 是用Ocaml 3.08 编译 的ProVerif1.13。ProVerif尚未根据ISO 3协议的规定终止。 对于所有其他协议，我们发现了已知的攻击，并证明了正确的。这些攻击与AVISPA工具发现的攻击相同（使用OFMC作为后端）。从图7可以得出结论，除了ISO 3之外，验证对所有协议都非常有效。ProVerif在ISO 3上的非终止性是由于ProVerif是一个定理证明系统，在某些情况下可能不会终止。7结论和今后的工作我们已经描述了一种算法，用于将HLPSL规范翻译为ProVerif工具支持的应用pi演算的方言，并给出了其实现。我们通过对各种HLPSL规范的推理说明了算法和实现的可用性。该算法为我们提供了两个有趣的科学贡献：首先，它提供了HLPSL规范语言的独立语义，其次，它可以使用ProVerif工具验证HLPSL中指定的协议。我们目前的研究工作正朝着以下方向进行。首先，我们扩展了翻译器来处理整个HLPSL。特别是，我们打算增加对复杂类型的支持，角色的顺序组合，以及在计算中使用fork的角色转换其次，我们将正式证明我们的翻译算法是正确的。由于HLPSL的语法和语义目前都在开发中，因此目前还不可能我们打算提供这样的证明，76A. Gotsman等人理论计算机科学电子笔记135（2005）59议定书时间（秒）性能攻击发现保密Auth.身份验证类型NSPK0.0422弱是的NSPK-Lowe0.0722强没有分享0.0912弱是的EKE0.0812弱是的Chapv20.0812强没有ISO10.021强是的ISO20.041强没有ISO3–2弱–ISO40.032强没有UMTS-AKA0.0512强没有见图7。实验结果这是目前正在开发的动作时序逻辑[18最后，我们正在努力识别更复杂的协议，以评估我们方法的可扩展性，并使用其他验证引擎来应用pi演算。一种可能的方法是使用HAL模型检查器[16，15]。这种方法特别方便，因为HAL可以有效地处理新名称的生成。引用[1] M. Abadi和B.布兰切特用保密类型和逻辑程序分析安全协议J. ACM，52（1）：102[2] L. C. Aiello和F.马萨奇 将安全协议作为逻辑编程中的规划。ACM Trans. Comput. Logic，2（4）：542 -580，2001.[3] A. Armando和L.康帕尼亚SATMC：一个基于SAT的安全协议模型检查器第九届欧洲人工智能逻辑会议论文集（JELIA 2004），LNCS第3229卷，第730-733页。Springer-Verlag，2004.[4] 阿维斯帕。D6.2：高级规范语言中问题的规范，2005年。 http://www.avispa-project.org/d6-2.pdf。A. Gotsman等人理论计算机科学电子笔记135（2005）5977[5] D. Basin，S. Modersheim和L.维加诺用于安全协议分析的在线模型检查器。第八届欧洲计算机安全研究研讨会论文集，第253-270页，2003年78A. Gotsman等人理论计算机科学电子笔记135（2005）59[6] B. 布兰切特密码协议的自动验证：逻辑编程方法。PPDPACM Press，2003.[7] Y. Boichut，P.-C. Heam，O.Kouchnarenko和F.哦改进Genet和Klay技术，自动验证安全协议。第三届国际无限状态系统自动验证研讨会论文集（AVIS'04），第1-11页，2004年[8] S.布拉金角Meadows和J. Millen。NRL协议分析仪的CAPSL接口。IEEE Symposium onApplication-Specific Systems and Software Engineering Technology（ASSET-99 ）IEEEComputer Society Press，1999.[9] S. H.布莱金一种用于自动分析密码协议的接口规范语言。 网络和分布式系统安全研讨会论文集，第40-51页，1997年。[10] Y.谢瓦利埃湖Compagna，J. Cuellar，P. Hankes Drieslma，J. Mantovani，S. Modersheim和L.维涅隆一种用于工业安全敏感协议的高级协议规范语言。2004年，安全要求的规范化和自动化处理研讨会论文集[11] E. M. Clarke，S. Jha和W.马雷罗与布鲁特斯解除安全协议。ACM Trans. Softw.工程师，Methodol。，9（4）：443[12] G. Denker，J. K. Millen，A. Grau，and J. Kuster Filipe. 优化协议重写规则CIL规格。第13届IEEE计算机安全基础研讨会论文集（CSFW-13），第52-62页，2000年[13] D. Dolev和A.耀公钥协议的安全性。IEEE Transactions on Information Theory，2（29）：198[14] A.杜兰特河Focardi，和R. Gorrieri。CVS：一个用于分析密码协议的编译器。第12届IEEE计算机安全基础研讨会论文集，第203-212页，1999年[15] G. Ferrari，S.格内西U.Montanari和M.皮斯托雷移动进程的模型检查验证ACM Trans. Softw.工程师，Methodol。，12（4）：440[16] G. Ferrari ， S. 格 内 西 U. 蒙 塔 纳 里 湾 Pistore 和 G. 里 斯 托 里 HAL 环 境 中 的 可 移 动 进 程 在Proceedings CAVSpringer Verlag，1998年。[17] F. Jacquemard，M.Rusinowitch和L.维涅隆编译和验证安全协议。在Proceedings of 7thInternationalConferenceonLogicforProgrammingandAutomatedReasoning（LPARSpringer-Verlag，2000.[18] L.兰波特动作的时间逻辑。ACM Transactions on Programming Languages and Systems，16（3）：872[19] E. G.洛Casper：一个用于分析安全协议的编译器。J.计算机Security，6：18 -30，53-84，1998.[20] G.洛身份验证规范的层次结构。在CSFWIEEE计算机学会，1997年。[21] P. Syverson和C.梅多斯密码协议要求的一种形式语言Des. Codes Cryptography，7（1-2）：27 -59，1996 .
我的内容管理
展开
