基于SAT的安全协议模型检测的优化入侵者模型：命题满足性序列在协议攻击中的应用

理论计算机科学电子笔记125（2005）91-108www.elsevier.com/locate/entcs基于SAT的安全协议模型检测的入侵者优化模型Alessandro Armando1 Luca Compagna2AI-Lab，DIST摘要在以前的工作中，我们表明，自动SAT为基础的模型检查技术的基础上减少协议（中）的安全性问题的命题满足性问题的序列可以用来有效地发现对协议的攻击。在本文中，我们提出了一个优化的入侵者模型，在许多情况下，可能会导致较短的攻击，可以在我们的框架中检测到生成较小的命题公式。 其关键思想是假设入侵者的某些能力具有瞬时效应，而在以前采用的方法中，入侵者的所有能力都被建模为状态转换。这需要非平凡的扩展SAT-减少技术，正式描述的文件。实验结果表明了所提出的优化的优点。关键词：安全协议，有界模型检测，SAT，重写。1介绍在过去的十年中，我们见证了SAT求解器的显着加速：现在，最先进的SAT求解器可以在毫秒内解决数千个变量的这导致了在规划和模型检查等重要领域的突破。受这些结果的启发，在[1，2，3]中，我们提出了将协议（不）安全问题简化为命题逻辑中的可满足性问题，可用于有效地发现攻击 在协议上。我们已经开发了一个模型检查器，SATMC，基于这些1 电子邮件地址：armando@dist.unige.it2电子邮件：compa@dist.unige.it1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.05.02192A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91-108通过对来自Clark-Jacob库[ 9 ]的安全协议运行SATMC获得的想法和实验结果证实了该方法的有效性在本文中，我们提出了一个优化的入侵者模型，导致在许多情况下，在我们的框架中，可以通过生成较小的命题公式检测到较短的攻击其关键思想是假设入侵者的某些能力具有瞬时效应，而不是先前采用的这需要非平凡的扩展SAT-减少技术，正式描述的文件。我们已经实施了建议的优化SATMC内。在Clark-Jacob库中的协议上的实验结果清楚地表明了所提出的优化方法的优点。论文概要。我们在第2节开始，通过一个众所周知的认证协议，我们的模型，特别强调了优化的入侵者模型的基础上的概念公理。在第3节中，我们用公理定义了协议不安全问题的概念。第4节致力于协议不安全性问题与公理的自动编译成一组命题满足性问题的形式化描述。第5节讨论了实验结果和一些实施细节。我们在第6节中结束了一些最后的评论和对未来工作的讨论。2安全协议虽然一般的验证问题-证明安全协议满足安全保证，它已经被设计在一个场景与任意数量的并行会话-是不可判定的[12，13]，对于许多协议，验证可以减少到验证有限数量的会话。 此外，即使对于那些应该根据 无限数量的并发协议执行，违反其安全要求往往只利用少量的并行会话。由于这些原因，在许多感兴趣的情况下，考虑有限和少量的并行会议就足够了。例如，对Clark-Jacob库中的协议的所有已知攻击最多涉及两个我们通过基于多集重写的IF [4]声明性语言中指定的状态转换系统对安全协议的并发执行进行建模，该声明性语言特别适合形式化分析[7，15]。状态由称为事实和转换的排序的一阶语言的原子公式集表示，并通过在A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）9193事实在我们的设置中，我们假设网络由非常一般的Dolev-Yao入侵者控制[11]。[3]在这个模型中，入侵者有能力窃听和转移消息，也有能力编写、分解、加密和解密消息（假设加密密钥是已知的）。最后，他可以用假身份将这些消息发送给其他参与者。除此之外，我们还做了完美密码学的标准假设，即：一个加密的消息只能通过使用适当的解密密钥和强类型来解密，即代理只接受类型正确的消息，因此不允许类型混淆。4为了阐明我们的介绍，让我们考虑Needham-Schroeder公钥（NSPK）认证协议[16]的例子。在常见的Alice Bob符号中，NSPK协议看起来如下：（1）A→B：{A，Na}Kb（2）B→A：{Na，Nb}Ka（3）A→B：{N b}Kb其中A和B是协议中涉及的角色;Ka和Kb分别是A和B的公钥;Na和Nb分别是由A和B生成的随机数。注意，上述高级协议规范描述了一种模板NSPK（A，B，Ka，Kb，Na，Nb），该模板由其中出现的一些自由变量6参数化。NSPK协议的成功执行应该使A和B都相信他们一直在互相交谈。理由是只有B和A才能分别对（1）和（2）中发出的信息作出适当的反应。事实上，一个恶意的代理人I可以欺骗bob（B的一个实例），让他相信他在和爱丽丝说话，而他在和我说话。这是通过并发地执行协议的两个会话NSPK（alice，1，ka，ki，na，ni）和NSPK（alice，bob，ka，kb，na2，nb）并使用来自一个会话的消息在另一个会话中形成消息来实现的，如下面的程序所示3值得指出的是，该模型并不局限于Dolev-Yao入侵者，但是，相反，它的表达能力足以得到适用于各种通信网络（例如安全信道、无线信道等）的通用入侵者模型。[4]正如[14]中所指出的，在许多感兴趣的情况下，类型攻击可以通过用指示其预期类型的信息标记消息的字段5随机数是由主体随机生成的数字，它们旨在用于只有一次6自由变量用大写字母表示，但I除外，I用于表示恶意代理。94A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91-108母育酚跟踪：（1.第一章爱丽丝→我：{alice，na}ki（2.第一章我（爱丽丝）→鲍勃：{alice，na}kb（2.（二）鲍勃→我（爱丽丝）：{na，nb}ka（1.（二）我→爱丽丝：{na，nb}ka（1.第三章爱丽丝→我：{nb}ki（2.第三章我（爱丽丝）→鲍勃：{nb}kb其中I（alice）表示假装是alice的入侵者。在上述跟踪结束时，鲍勃认为他一直在与爱丽丝交谈，但事实显然并非如此。让我们在我们的设置中描述上述示例的状态转换系统和安全要求。事实 以下是描述NSPK协议的有用事实• ik（T），意味着入侵者知道消息T;• fresh（N），意味着临时数N尚未被使用;• m（J，S，R，T），这意味着主体S已经（假定）7发送了消息T在方案步骤J处向主体R提供;以及• w（J，S，R，[T1， . . ，Tk]，C），表示主R的执行状态在会话C的步骤J;特别地，它意味着R知道消息T1，.，T k，并且-如果J0-还可以确定来自等待会话C的步骤J被执行。A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）9195初始状态。 系统的初始状态表示两个并发的7正如我们将看到的，由于入侵者可能伪造其他主体96A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91-108全国妇女委员会的会期为：8次w（0，a，a， [a，i，ka，ka−1，ki]， 1）（1）. w（0，a，a，[a，b，ka，ka−1，kb]，2）. w（1，b，a，[b，a，kb，kb−1，ka]，2）（2）. fresh（nc（n 1，1））（3）. fresh（nc（n 1，2））. fresh（nc（n 2，2））（4）. ik（i）. ik（a）. ik（b）. ik（ki）。 ik（ki−1）. ik（ka）。国际会议中心（kb）（5）事实（1）表示诚实代理a的初始状态，诚实代理a在会话1中扮演发起者的角色，并且在开始时知道她的身份、入侵者的身份（她想要与之交谈的代理）、她的公钥和私钥9以及入侵者公钥。事实（2）表示在会话2中分别作为发起者和响应者涉及的诚实代理a和b事实（3）和（4）陈述了随机数nc（n1， 1）、nc（n1， 2）和nc（n2， 2）的初始新鲜度。请注意，由于我们限制了并行会话的数量，因此可以提前计算和限制事实（5）表示入侵者最初知道的请注意，根据标准的封闭世界假设，所有没有出现在表示初始状态的集合中的事实都被认为是假的。目标谓词。安全协议旨在享有特定的安全属性。在我们的示例中，此属性是验证响应方与发起方的能力，反之亦然。安全属性可以通过提供表示一组“坏”状态的目标谓词来指定。例如，可以立即看到，b认为已经完成了与a的会话而a还没有开始与他的会话的任何状态都表示违反了b与a之间的预期认证属性。a. 这组坏状态可以很容易地用目标谓词w（1，a，b， [b，a，kb，kb−1，ka]，s（2））<$w（0，a，a， [a，b，ka，ka−1，kb]， 2）.108为了提高可读性，我们使用“。“操作符作为集合构造函数。例如，我们写“x。y. z9 注意，我们用ka-1表示公钥ka的逆。10注意，s（C）表示会话C的下一次执行。A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）9197−−−−−−−−−−−→−−−−−−−−−−−−−−→−−−−−−−−−−−−−−−−→标签重写规则。如上所述，事实集上的标记重写规则用于指定转换系统如何演变。特别地，我们区分了对诚实代理的行为建模的规则（所谓的协议规则）和代表Dolev-Yao入侵者的规则（所谓的入侵者规则）。这些规则将在接下来的部分中描述。关于所使用的符号，假设M1和M2是消息，则项{M1}M2和M1，M2，M3表示使用M2作为非对称的M1的非对称加密Ric密钥和M1和M2的配对，分别为112.1诚实参与者诚实的参与者严格按照协议行事。以下重写规则模拟了发送NSPK协议的第一条消息的活动：fresh（nc（n 1，S））. w（0，A，A，[A，B，Ka，Ka−1，Kb]，S）步骤0（A，B，Ka，Kb，S）w（2，B，A， [nc（n1，S），A，B，Ka，Ka−1，Kb]，S）. m（1，A，B，{A，nc（n1，S）}Kb）注意，随机数nc（n1，S）被添加到A的知识中以供后续使用。消息的接收和响应者的回复由下式建模：fresh（nc（n 2，S））. m（1，A，B，{A，Na}Kb）. w（1，A，B， [B，A，Kb，Kb−1，Ka]，S）步骤1（A，B，Ka，Kb，Na，S）w（3，A，B， [N a，nc（n2，S），B，A，Kb，Kb−1，Ka]，S）. m（2，B，A，{Na，nc（n2，S）}Ka）通过增加协议步骤并通过利用所获取的信息（即由发起者发送的随机数和由响应者自身新生成的随机数）扩展知识来更新响应者的状态。该方案的第三步通过以下方式建模：m（2，B，A，{Na，Nb}Ka）. w（2，B，A，[Na，A，B，Ka，Ka-1，Kb]，S）步骤2（A，B，Ka，Kb，Na，Nb，S）w（0，A，A， [A，B，Ka，Ka−1，Kb]，s（S））. m（3，A，B，{Nb}Kb）[11]为了提高可读性，我们用M1，M2代替了M1，M 2，其中配对信息可以很容易地从上下98A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91-108文中显示出来。A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）9199−−−−−−−−−−−−−−−−→...注意，在应用了这个规则之后，A完成了她在会话S中的部分，并且她最终准备好与B开始协议的另一个会话s（S）。方案的最后一步通过以下方式建模m（3，A，B，{Na}Kb）. w（3，A，B，[Na，Nb，B，A，Kb，Kb−1，Ka]，S）步骤3（A，B，Ka，Kb，Na，Nb，S）w（1，A，B， [B，A，Kb，Kb−1，Ka]，s（S））在应用这个规则之后，B也完成了他在会话S中的部分，并且他最终准备好在另一个会话s（S）中与A2.2对入侵者的行为进行与忠实地执行协议规定的每个语句的诚实代理相反，Dolev-Yao入侵者有许多自由度。通过观察网络中的所有流量，它扩展了自己的知识，并从这样的知识，它可以编写和发送欺诈性消息给诚实的参与者。然而，这些消息中的许多消息对于协议的分析可能是不感兴趣的。事实上，如前所述，我们专注于有限数量的并行会话的可达性问题，其中诚实的代理人只对消息做出反应，当且仅当该消息具有接收者所期望的类型和模式。这样一组“有趣”的信息是有限的。例如，以下部分实例化的规则对Dolev-Yao入侵者配对消息配对（a，M）ik（a）ik（M）−→ik（a）ik（M）ik（a，M））可以应用于NSPK的初始状态，通过用a替换M，并且在每个后继状态中，用形式为a，a，a，..的消息扩展入侵者的知识。. 没关系然而，这样的消息对于我们的示例的分析来说不是“内部的”，因此，用于组成它们的规则也是无用的。事实上，转移、模仿和分解规则足以对Dolev-Yao入侵者进行建模，并且很容易看出这种优化是正确的，因为它保留了现有的攻击并且没有引入新的攻击。转移规则。以下规则模拟了入侵者转移诚实参与者交换的信息的能力：转向（A，B，I，M）m（I，A，B，M）−−→ik（M）100A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91-108−−−−−→KK它指出，如果一条消息已经在通信信道上发送，那么入侵者可以读取其内容并将其从信道中删除。模拟规则。观察到由严格遵守的Dolev-Yao入侵者生成的大多数消息被接收器拒绝为非预期或病态的，这表明限制这些规则，使得入侵者仅发送与接收器所期望的模式匹配的消息。对于格式....m（I，A，B，M） .w（I，A，B，Knw，S）步骤I（. ）...并且对于每个可能的消息集合{M1，k，.，M jk，k}（设m是这样的集合的数目，则k = 1，. ，m和j k> 0），Dolev-Yao入侵者将能够根据该消息构建匹配M（并且符合M的类型）的消息Mj，我们添加以下形式的新规则：... . w（I，A，B，Knw，S）. i（A）. i（B）. i（M1，k）. ... . i（Mj，k）模仿I，k（.）J−→........................ m（I，A，B，M）. w（I，A，B，Knw，S）. i（A）. i（B）. i（M1，k）. ......这是什么？ . i（M j，k）. i（M J）该规则规定，如果代理B正在等待来自A的消息M，并且入侵者能够编写与M匹配（并且符合M的类型）的消息MJ，则入侵者可以冒充A并发送MJ。这个选择-在[15]中首次引入的mization通常以戏剧性的方式减少规则实例的数量（更多细节请参见[1]）。值得指出的是，通过应用[5]中提出的步进压缩优化，可以将上述入侵者规则与协议规则合并，从而显著减少要探索的搜索空间的维度。有关在我们的设置中实现此优化的更多详细信息，请参见[1]。分解规则。为了能够应用模仿规则或步骤压缩规则，入侵者必须被提供最小的规则集，该规则集建模其分解每个子消息的能力，A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91101.在协议的并行会话中交换的消息。例如，用于分解NSPK的第一条消息的规则如下：ik（{M}K解密（K，M）−−−−−−−−→ ik（{M}K）的。ik（K−1）. ik（男）分解（M1，M2）ik（M1， M2）−−→ik（M1）ik（M2）第一条规则指出，如果入侵者知道用密钥K和解密密钥K-1加密的消息，则转移系统可以在入侵者的知识被扩展为内容的状态中移动。M的消息。类似地，第二规则规定，如果入侵者知道配对消息M1、M2，则可以应用该规则以达到利用消息M1和M2扩展入侵者的知识的状态。特别是对于工业规模的安全协议，其中消息可能具有复杂的结构，为了找出攻击而应用的分解规则实例的数量可能很大。正如我们将在第4节中看到的，生成的命题公式的大小（以原子和子句为单位）由于SAT问题的复杂性随着原子数的增加而呈指数增长，因此减少这样的长度是至关重要的。本文提出的优化方法是基于公理的概念.公理是一个公式，它陈述了转换系统的事实之间的关系，并且在转换系统的每个状态12.事实证明，公理是平行的。特别适合于表示入侵者知识事实之间的关系为公理（The Axiom）ik（{M}K）ik（K−1）ik（M）每当入侵者知道用密钥K和解密密钥K-1加密的消息时，它也立即知道消息的内容M。 公理与规则事实上，前者必须在转换系统的每个状态下保持，而后者即使满足所有先决条件也不会被强制执行，并且它会花费一个转换来执行。因此，通过用适当的分解公理替换分解规则，我们获得了双重好处：所生成的命题公式的大小可以减小，并且要应用于发现攻击的转换步骤的数量也可以减小。 请注意，给定入侵者分解规则DR_DR_R，[12]请注意，如果一个公理包含变量，那么这些变量是泛量化的。）-1。ik（K）102A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91-1081j1jL可以直接构建分解公理DA的集合：DA={p·· ·pc|（p。.... . . 你 好 。 . . p−→lC）∈ DR，c∈C}可以证明，这种优化是正确的，因为它保留了现有的攻击，不引入新的攻击，并且它导致相等或更短的攻击。3协议不安全问题及其公理化第二节中提出的概念可以转化为带有公理的协议不安全问题的概念 一个带有公理的协议不安全问题是一个元组n = n F，L，R，A，I，G n其中F是一组被称为事实的排序一阶语言的原子公式，L是一组被称为规则标签的函数符号，A是一组形式为p1n的公理。其中p1，...，p j，c在F 中，且dR是f∈L−→R的一组重写规则，其中L和R是F的有限子集，使得出现在R中的变量也出现在L，l是形式l（x）的表达式，其中l∈ L，x是向量通过对变量进行字典排序而获得的变量，L.公理型协议不安全问题的I分量和G分量分别是初始状态和表示协议坏状态的布尔公式在这种情况下，一个状态由在其中为真的事实集S F表示因此，所有不在S中的事实都被认为是假的（封闭世界假设）。此外，所有的状态必须满足公理集A。形式上，状态（S）={S|SF，S| = A}。13LetSbeastateand（L−→lR）∈ R，如果σ是置换，使得Lσ<$S且SJ=（S\Lσ）<$Rσ使得SJ|= A，则一个可能的下一个状态是SJ，我们用S来表示~lσ SJ。 我们假设重写 规则是确定性的，即如果S~SJ和S~lσSJJ，则SJ= SJJ。 的解决方案带有公理系统的协议不安全问题，称为攻击，是一个规则序列l σ，.，l σ使得Sl~iσiS对于i = 1，.，n与SI和S|=G.1 1 nn i i +1 1n攻击的长度是其中发生的规则的数量通过允许规则的并行执行来放松与具有公理的协议不安全问题相关联的转移关系的定义是方便的，尽管保留了模型的交错语义。这意味着，其中一些规则被同时执行的每个跟踪可以被线性化为其中所有规则被顺序执行的更长的跟踪。在13注意，S|对于A中的每个置换σ和（p1<$··<$pk <$c），S| =（p1σ···<$pk σ）<$cσ。lσA.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91103为了保证模型的交错语义，我们将互斥定义为规则之间的互斥（mutex）在协议不安全问题概念中引入公理互斥关系需要构造一个有向图GA=F，E表示事实与公理集之间的依赖关系其基本思想是，对于每个置换σ和（p1<$··<$pj<$c）∈ A，cσ，p1σ，p_cσ，p_j σ_n在边集合E中。 一个事实c依赖于一个事实p，记为c<$→Ap ， i <$GA 中 有 一 条 从 结 点 c 到 结 点 p 的 路 。令 depA （ c ） ={p|c<$→Ap}{c}是一组事实，其中c依赖于wrtA，类似地，令depA（C）=c∈CdepA（c）是C中的事实依赖于A的一组事实。互斥关系所以，它的定义如下：对于每个L1−→l1R1、L2 −→l2 R2在R中，对于每个一对置换σ1和σ2，使得l1σ1l2σ2，则l1σ1<$l2σ2i <$L1σ1depA（（L2σ2\R2σ2））L2σ2≠depA（（L1σ1\R1σ1））- 是的如果l1l2我们说L1和L2是冲突规则实例。的并行执行因此，通过下面的过渡的宽松定义，规则是允许的。 设S在一个状态下，如果其表达式为s{L-→l1}的集合， R， . . . . ， L−l→m R }R和a1 1m m替换集合{σ1，.，σ m}，通过定义L =（mLi σi）和Rmi=1=（i=1R i σ i），（i）对于每个i，j = 1，.，m与i则li σi<$lj σjnot hold（非冲突规则实例），（ii）LR=R，（iii）LS，以及（iv）（（S\L）R）|= A，则S的一个可能的下一个状态是SJ=（（S\L）<$R）。我们用第S~Λ表示这个 其中r∈Λ={1σ， . . ， lσ}。 同样，P11个月M对协议不安全问题的解决方案的定义可以重新转换为偏序攻击的概念。 对协议不安全性问题的偏序攻击是重写规则实例集合Λ 1，. ，Λ n这样所以S是~ΛiP Si+1 对于i = 1，.，n与S1S n和Sn|= G. 的长度偏序攻击对应于序列中集合的数目。可以证明，对伪随机数的偏序攻击对应于一组攻击到了。此外，令reach（S，~）和reach（S，~）的状态集，P通过过渡关系~和~从状态S到达，P分别可以证明reach（S，~）=reach（S，~）。P4基于公理设A = F，L，R，A，I，G是一个协议不安全问题，其公理满足：（i）事实集、公理集和规则集是有限的，（ii）公理集A不包含事实之间的任何命题等价（即，A不包含事实之间的命题等价）。所有104A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91-108ΞΞΞΞ事实p1，.，p j，c在F中，它认为|= A（p1<$··<$p j）<$c），设k为a正整数，则有可能建立一个命题公式Φk等Φk的任何模型都对应于Φ k的长度为k的偏序攻击。值得指出的是，建模入侵者分解消息的能力的公理满足上述要求（i）和（ii）。在以前的工作中，我们描述了如何使用两种编码技术将没有公理的协议不安全问题编译成一组SAT公式：第一种属于所谓的线性编码家族[1，2]，第二种是更复杂的基于图的编码[3]。让我们看看如何扩展我们的方法，使之能够处理第2节和第3节中描述的公理。其基本思想没有改变，而是向规则和事实添加了一个额外的时间索引，以指示规则开始或事实成立的状态。因此，事实由0到k索引，规则由0到k-1索引。如果p是一个事实或规则，i是适当范围内的索引，则p i是相应的时间索引命题变量。然而，随着公理引入到协议不安全问题的概念中，必须对编码方案进行重大修改。在本节的其余部分，我们将正式描述如何使用线性编码技术将带有公理的协议不安全问题编译为SAT。类似的概念也适用于基于图平面的编码技术。还请注意，我们将要介绍的编码技术也可以简单地应用于将没有公理的协议不安全问题编译为SAT，设置A = 0。类似于经典的有界模型检查方法[6]，propo-标准公式Φk定义为：k−1Φk =I（f0）i=0时Ti（fi，li，fi+1）<$G（fk）其中f和l分别是事实和规则的向量14，• I（f0）是对初始状态I进行编码的公式;• G（fk）是对由G表示的目标状态进行编码的k索引公式;• Ti（fi，li，fi+1）是一个公式，它编码了i步可达状态和i+1步可达状态之间的转换关系。我们的编码技术与其他有界模型检查器（例如，[8]是一个公式，14设p是事实或规则的向量，i是适当范围内的索引，则pi是命题变量的对应时间索引向量。A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91105Ξ黎黎li⊃i+1li⊃i+1对转换关系进行编码，即生成Ti（fi，li，fi+1）通过使用线性编码技术，被定义为如下：• I（f0）是公式f0（如果f∈ I）和<$f0（如果f/∈ I）的合取;• G（fn）由G通过用fn替换每个事实f而得到;• T i（fi，li，fi+1）等价于T（fi，li，fi+1）（即编码转换关系的公式与时间步长无关），并且是通用公式、解释框架公式、公理公式和相容性排除公式的结合。为了提高可读性，我们将定义R和A作为规则集instanceancesand a Xiominstanceances，respectively. Clearly，R={Lσ−l→σRσ|L−→lR∈R， σ是一个子位置}，且A∈={p1σ<$· · · <$pjσ<$cσ|p1·· ·pjc∈ A，σ是一个代换}。通用公式。它们表达了过渡关系如何演变，它们被定义为以下的合取：{f|f ∈ L}{f|f∈（R\L）}{f|f ∈（L\R）}对于ea chL−→lR∈R<$。解释框架公式。 它们表达了过渡系统 通过引入公理，这些公式的定义要求定义A的连续向量的集合A。换句话说，<$ba是a的c_n_transp_e_d_x_iom。给定一个ximi nnnph|（p1<$· · <$pj<$c）∈A<$， h=1， . . ，j}。用于显微镜的X线平片框架106A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91-108Ξ因此被定义为以下的结合：. 、（f i<$fi+1）li|（L−→l、R）∈R<$， f∈（L\R） ∨一期+1一期+1一期+1{p 1p2···pj|Σ（<$p1<$p2<$ · ·<$pj <$$>f）∈A<$}. 、（<$f i<$f i+1）li|（L−→l、、R）∈R， f∈（R\L） ∨，pi+1·· ·pi+1|（p1<$· · · <$pj<$f）∈A<$1J对于所有的事实f∈ F。为了将上述公式转换成CNF而不引起子句数量的组合爆炸，它需要用新的变量v替换每个合取p1···pj，并添加式vi（pi···pi）。 可以看出，在最坏的情况下，1Jn=0，n = 0，n =|A.|）.公理公式。它们表达了转换系统的事实之间的性质。它们被定义为（pi··pi）ci的合取，1Jeach（p1<$· · <$pj<$c）∈A<$.相容性排除公式。它们声明哪对规则实例不能并行执行，以保证模型它们被定义为<$（lili）的合取，对于所有的l1l2，1 2那是我的错。可以立即看出，Φk中的原子数时间复杂度O（k）|F|+K|R|+的K|A.|）. 进一步地，由UniversalF或Mulae生成的clau s的数目在O（kP0|R|其中P0是规则实例中的元素的最大数目（通常是一个小数目）;由解释框架生成的子句的数目在O（k）内|F|+kR0|A.|其中R0是最大值，在公理实例的前提条件中提到的事实的数量（通常是一个小数目）;最后，由相容排除法生成的子句的数量在O（k）中|R|2）的情况。A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91107ΞK原子条款9 530,7261,804,0059 995,323 5,736,6629114,530334,08676,61233,32689,15753,7416 481,3942,498,382K原子条款7414,5361,489,1217 776,8054,590,268888,343298,49143,71419,24255,60033,8355409,1142,133,265高雄23 NSCKNSPKNSPK服务器Woo-LamM议定书5实施和实验结果我们已经在SATMC中实现了上述思想，SATMC是一个用于安全协议分析的基于SAT的假设一个协议不安全问题，ioms，SATMC将其编译为SAT公式Φk使用它的一种编码增加k值的技术，并且在每一步生成的命题公式被馈送到最先进的SAT求解器（目前支持Chaim、SIM和SATO）。一旦找到一个满意的公式，相应的模型将被转换回一个报告给用户的偏序攻击SATMC目前实现了两种编码技术，并且都已经扩展为支持公理：第一种属于所谓的线性编码家族，第二种是更复杂的基于图的编码。我们已经针对从Clark/Jacob库中选取的（令人敬畏的）安全协议运行了我们的工具[9]。对于每个协议，我们已经自动生成，通过从IF [4]到SATMC内部语言的翻译器，两个相应的协议不安全性问题建模具有有限数量会话的场景，其中所涉及的主体在分别由Dolev-Yao入侵者和优化的Dolev-Yao入侵者控制的信道上正如第2节所解释的，优化包括通过公理而不是规则来建模入侵者分解消息的能力。表1使用线性编码的DY优化DY表1和表2报告了我们的实验结果，分别通过应用线性编码和基于图平面的编码，在没有优化入侵者（DY）和有它（优化DY）的协议不安全问题。实验已经在具有1.4 GHz CPU和1 GB RAM的PC上进行。对于每个协议和每个协议的不安全问题，有和没有优化的入侵者，我们给出的最小值108A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91-108K原子条款97263,06599905,01994351,39274111,24988472,68864811,518K原子条款74581,78475872,60683481,105419954953801,17753581,137高雄23 NSCKNSPKNSPK服务器Woo-LamM议定书表2使用基于Graphplan的编码的DY优化DY攻击被发现时的k（K），以及SAT公式中命题变量（原子）和子句（子句）的数量。[15]我们可以立即看到，对于这两种应用的编码技术，SATMC能够通过生成高达50%的小命题公式来找出高达40%的短攻击这些结果证实了所提出的基于SAT的模型检查方法的优化入侵者模型的有效性，并为SATMC在工业复杂性协议中的应用铺平了道路，其中攻击最终可能需要相当数量的入侵者知识推理步骤。6结论和展望我们提出了一个优化的入侵者模型，用于基于SAT的安全协议模型检测。我们已经表明，这种优化，基于建模的入侵者知识的分解的思想，通过公理而不是规则，导致发现更短的攻击，通过生成更小的命题公式。我们已经增强了我们的SAT为基础的模型检查器（SATMC），能够分析协议的不安全问题扩展了一组公理（没有等价循环）。通过运行SATMC对从Clark-Jacob库中提取[15]请注意，如果在有和没有优化的入侵者的情况下，对协议不安全问题的攻击长度相同，那么所获得的结果是如此具有可比性，以至于我们避免展示它们。16注意，对于分析的每个安全协议，在相应的协议不安全性问题与优化入侵者和没有优化入侵者是相同的，除了在前者的情况下，我们保存所有那些为分解入侵者的知识而执行的规则。A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91109在实际应用中出现的协议。事实上，在工业规模的安全协议中交换的消息可能具有复杂的结构，因此，对这种协议的攻击可能需要相当多的入侵者知识操纵。由于所提出的优化允许瞬间分解整个入侵者的知识，我们推测，这将是特别成功的协议和实验将在这个方向上进行。另一个有趣的和具有挑战性的未来的方向，我们想调查关注我们的SAT约简技术的扩展，以支持编码的通用公理集，也指定之间的事实等价。这对于表示指定密码运算符的特殊属性的代数方程特别有用，例如Di Blee-Hellman协议中的幂运算[10]。值得指出的是，在这样一个协议，我们已经取得了一些初步的结果，在我们目前的设置。事实上，通过一组公理部分地指定幂运算，我们已经能够发现对Di Vee-Hellman协议的著名攻击。致谢我们非常感谢CristinaFra`为支持这种优化的入侵者而实施的编码。此外，我们还要感谢匿名评论者的有益评论。这项工作得到了欧盟Calculemus培训网络（HPRN-CT-2000- 00102）和FET开放EC项目“AVISPA：互联网安全协议和应用程序的自动验证”（IST-2001-39252）的部分资助引用[1] A. Armando和L.康帕尼亚自动SAT编译协议不安全问题通过减少规划。Forte 2002，LNCS2529，第210-225页。Springer-Verlag，2002.[2] A. Armando和L. 康帕尼亚 抽象驱动的基于SAT的安全协议分析。在SAT 2003会议记录中，LNCS 2919 。 Springer-Verlag ， 2003. 可 在 www.example.com 上 获 得 http://www.avispa-project.org。[3] A.阿曼多湖Compagna和P. Ganty。基于SAT的安全协议模型检验的规划图分析。在FME'2003会议记录Springer-Verlag，2003.[4] Alessandro Armando、David Basin、Mehdi Bouallagui、Yannick Chevalier、Luca Compagna、SebastianMüodersheim、MicaAVISS安全协议分析工具。在CAV'02会议记录Springer-Verlag，2002.[5] D.Basin，S. 我和他。 Vigan`o。一种用于安全协议分析的在线模型.在Einar Snekkenes和Dieter Gollmann，编辑，会议记录110A.阿曼多湖Compagna / Electronic Notes in Theoretical Computer Science 125（2005）91-108的ESORICS'03， LNCS 2808,页253-270. Springer-Verlag，2003.可用 在http://www.avispa-project.org网站。[6] A. Biere，A. Cimatti，E. Clarke和Y.竹 没有BDD的符号模型检查。在W. R. Cleaveland，编辑，《TACAS'99会议记录》史普林格出版社[7] Iliano Cervesato，N. A.放大图片作者：John C.米切尔和安德烈·斯切德罗夫用于协议分析的元符号。见CSFW，第55-69页[8] A. Cimatti，E.克拉克角，澳-地Giunchiglia和M.罗维里NuSMV：一种新的符号模型验证器。LNCS 1633，1999年。[