局部安全属性的新跟踪逻辑与TMN协议设计

--理论计算机科学电子笔记118（2005）129-143www.elsevier.com/locate/entcs一种局部安全属性Ricardo Corin，Sandro Etalle，Pieter Hartel1，2计算机科学学院，地址：P.O.Box 217，7500AE Enschede，The NetherlandsAntonio Durante安东尼奥·杜兰特1，3Universit`adiRoma摘要我们提出了一个新的简单的跟踪逻辑，可用于指定本地安全属性，即安全属性，指的是一个单一的参与者的协议规范。我们的技术允许协议设计者提供所需安全属性的正式规范，并将其自然地集成到加密协议的设计过程中。 此外，逻辑可以用于形式验证。我们说明了我们的技术的实用性，通过暴露新的攻击研究TMN协议。关键词：跟踪逻辑，局部安全性，规范，TMN协议1介绍加密协议通常被设计为满足安全目标，例如身份验证和机密密钥交换。这些目标通常称为安全属性，如果在协议运行期间交换的某些值满足例如真实性、保密性或新鲜性等经典属性，则可以正确地实现这些目标1我们要感谢解百纳和眼睛项目（IST- 2001-34734）对这项工作的支持。2Email：corin，etalle，p ie ter@ cs. 我的天3电子邮件：durante@dsi.uni ro ma1。它1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.12.019130R. Corin等人理论计算机科学电子笔记118（2005）129→通常，安全属性的指定是通过写入“全局”安全属性来实现的这些安全规范不依赖于任何主体因此，为了引用特定的主体，全局安全属性通常使用额外的协议事件来定义[8，11]。在本文中，另一方面，我们提出了一个逻辑，可以用来表达本地安全属性，即。属性指的是一个代理的具体化正如我们在下面的部分中所展示的，本地安全属性具有足够的表达能力，可以断言密码协议通常需要的属性（例如，新鲜度的一个nonce）。本地属性的优点是，它们允许设计者根据每个参与者在每个协议执行点指定应该保持的安全属性。例如，一个nonce的新鲜度这样的属性可以被指定为一个公式，该公式直接连接到接收该nonce的相应参与者。此外，由于这些公式对应于每个主体，因此它们仅依赖于该主体的信息，而不是可以依赖于整个网络状态的全局公式。因此，本地公式可以绑定到每个主体，然后“插入”到任何其他网络规范中。这使得规范具有潜在的可组合性。因此，使用本地属性，可以将协议必须满足的（逻辑）安全属性的规范集成到协议本身的（算法）规范中。这产生了一种用于协议工程的集成技术，该技术紧密结合了设计和分析阶段，从而缩短了设计验证反馈回路。我们通过研究TMN协议[10]来说明我们的方法，我们发现了两种新的攻击。纸的计划。在第2节中，我们描述了我们的安全协议模型。然后，在第3节中，我们介绍我们的跟踪逻辑语言。第四部分研究了TMN协议，并提出了一些新的攻击方法。第5节阐述了相关工作，最后的结论和未来的工作在第6节讨论。2协议模型协议步骤通常使用标准符号A B：M指定。在这里，M是一个消息，由以下内容构建：• 原子术语，即常量（用大写字母表示）和变量（大写字母表示）。常数可以是随机数（例如na）或代理身份（例如a）。一个特殊的常数ε表示入侵者。R. Corin等人理论计算机科学电子笔记118（2005）129131⬦• 构造项，即运算符加密MK，配对M1，M2，哈希h（M）和最终公钥pk（M）在原子项上的有限应用。然而，A→B：M符号不适合于形式验证。事实上，在协议步骤中，发生两个不同的事件：A发送消息M，B接收消息MJ。在存在入侵者的情况下，M可能不等于MJ。此外，甚至对应通信方的身份也不可能相同（即， A发送给BJ，B从AJ接收。）它因此，采取一种单独考虑每个代理人观点的方法是方便的定义2.1一个协议角色是一对协议A，[M1<$B1，.，M nB n]，其中A，B1，...， Bn是可变的s，n∈{a，d}和M1，.， MN是我的年龄。Q给定协议角色A，[M1<$B1，...，M n<$B n] n，A称为角色的身份，而元素M iB i，i= 1. n是角色的动作：M d B是一个发送动作，而M a B是接收动作。安全协议中的协议角色通常会收到（自解释）名称，例如发起方、响应方和服务器。比如说，responder（A，B，Na）=B，[pk（Na）a A]（1）定义了一个只有一个动作的响应者角色，即接收Na从.注意，在（1）中，变量A，B，Na仍然是未实例化的（我们从逻辑编程中借用了这个概念：只要没有值被分配给变量，我们就称之为未实例化的，否则就实例化。事实上，协议角色是参数化的，因此代表一个模板。通过适当地（部分地）实例化有限数量的协议角色，可以获得系统场景定义2.2一个系统场景是一组（部分）初始化的协议角色。通常，系统方案确定存在多少会话以及哪些代理扮演哪些角色。例如，系统场景{responder（A，b，Na），responder（C，d，Nc）}（其中响应者是上面定义的角色）定义了一个有两个响应者的系统场景（注意没有相应的发起者），一个由b扮演，另一个由d扮演。未实例化的变量表示未知值：132R. Corin等人理论计算机科学电子笔记118（2005）129⟨⟩⟨⟩⟨ ⟩·例如，第一响应者角色中的变量A表示b的（未知）通信方。2.1踪迹语义系统场景的执行使用跟踪来描述，跟踪又由事件组成，即由代理人执行的单个动作定义2.3一个事件是一对A：M<$B<$A，其中A，B是代理人且M是m ∈{a，d}。Q事件A：M d B应该被理解为“代理A发送消息M与预期目的地B“。 另一方面，B：M aA代表为了分析该协议，我们将系统场景与通常的Dolev-Yao入侵者[5]结合起来，后者可以执行通常的操作：拦截和学习任何发送的消息，存储拦截消息中包含的信息以供以后使用，并将使用入侵者知道的信息伪造的新消息引入系统。 入侵者获得的信息存储在一组项K中，称为入侵者的知识4现在我们准备好描述一个系统场景的执行，表示为：被跑步的概念所吸引。定义2.4设S是一个系统场景，K是入侵者的初始知识，由代表代理身份及其公钥的常数组成。设tr为初始空迹。S的游程是通过以下步骤的重复序列获得的迹：(i) S中的一个非空角色是非确定性地选择的，它的第一个动作p被从中移除。设a为所选角色的标识。(ii) 如果p=td y，则：(a) t被添加到入侵者的知识中，K：=K<${t}(b) 事件e=a：p被添加到tr，tr：=tr·e(iii) 如果p=ta y，则：(a) 检查入侵者ε是否可以使用知识K5生成t，如果是，则将事件e=a：p添加到迹：tr：=tr e。(b) 如果ε不能生成这样的消息，则运行停止。[4]由于分析器的符号性质，实际上事件可以包含变量，这些变量代表入侵者可以生成的东西（详见[3]）。5我们采用Millen和Shmatikov的约束求解过程[ 13 ]来检查入侵者是否可以使用知识K生成项t。 该过程可以涉及t或K中的变量的实例化;例如，t可以与K中的项统一，表示t已经在K中，即，已被入侵者知道（详情见[13]）。R. Corin等人理论计算机科学电子笔记118（2005）129133≤· ·F× →{}FQ3跟踪逻辑在本节中，我们将介绍一种用于定义本地安全属性的跟踪逻辑语言。定义3.1根据以下语法生成跟踪逻辑公式F：：= 真|虚假|F1∧F2|F1∧F2|F1→F2|e∈tr：F|秘书长：F| €F| e 1 = e2|e1≤ e2|e1 ≤e2其中e、e1和e2是事件。Q两个公式的合取具有通常的意义：如果F1和F2都为真，则F1<$F2为真;析取算子和蕴涵→是类似的。另一方面，构造函数f∈tr：F和f∈tr：F是非标准的。由于一个轨迹公式将在某个输入轨迹上进行计算，构造函数和允许我们推理输入轨迹中的事件：e∈tr：F断言输入轨迹中的每个事件e满足公式F，而e∈tr：F表示输入轨迹中的某个事件满足公式F。 请注意，tr不是变量，它只是运算符名称的一部分，以强调e在系统跟踪上的范围。尽管这给我们的逻辑提供了一个“时间”的解释器，但我们预计这些构造函数只对记录在输入跟踪中的过去事件进行操作（见下文）。公式F具有否定的通常意义。与上面的运算符不同的是，f：F量化所有消息和代理空间。最后，谓词e1= e2和e1e2允许我们比较事件：前者断言相等，后者子项包含。虽然这些构造函数的选择对于我们的目的来说似乎是相当特别的，但我们相信这种逻辑实际上是非常有表现力的，并允许我们断言相当大的一组有趣的安全属性，如稍后所示。接下来，我们定义迹逻辑公式的精确含义定义3.2设是合式迹逻辑公式的集合，TR是迹的集合，则语义函数[]]：TRtrue，false定义如下：134R. Corin等人理论计算机科学电子笔记118（2005）129··Q[[true]]tr=true[[false]]tr=false[[F1<$F 2]]tr=truei <$[[F 1]]tr= [[F 2]]tr=true[[F1<$F 2]]tr=truei <$[[F 1]]tr=true或[[F 2]]tr=true[[F1→F 2]]tr=truei[[F 1]]tr蕴涵[[F 2]]tr[[e∈tr：F]] tr=true 对于tr的每个事件x，[[F[x/e]tr= true[[e∈tr：F]] tr=true i，对于tr的某个事件x，[[F[x/e]tr= true[[t：F]] tr=true i.对于某个消息或代理x，[[F[x/t]tr= true[[<$F]]tr=truei[[F]]tr=false[[e1=e 2]]tr=truei如果事件e 1等于事件e 2[[t1≤ t2]]tr=truei，如果 t1是 t2Q这里，F[x/y]是在F中用x替换每次出现的y的结果。为了符号的简单性代理）。 这大大简化了符号。在未来，我们计划赋予我们的逻辑一个证明系统，使我们能够将公式的证明与[ ]]给出的预期含义联系起来。 在目前的工作中，我们更感兴趣的是探索安全规范的表达能力;我们计划通过解决使用我们的逻辑进行自动形式验证的问题来继续这项工作。3.1将本地安全属性转换为协议角色现在，我们准备将协议角色的定义和本地安全属性结合起来，以获得扩展的协议角色和扩展的系统场景。直观地说，这个想法是将逻辑安全属性嵌入到协议规范中。定义 3.3一个扩展协议角色是一个三 重协议A，[M1] B1： F1， .， Mn<$Bn：Fn]n，其中{A，B1 ，.， Bn}{\displaystyleBn} Mn是m∈{a，d}和F1，.，Fn是迹逻辑公式。直观地说，在协议角色动作之后添加公式Fi意味着Fi必须在动作执行之后保持。请注意，扩展协议角色的实例化也会影响附加的本地安全属性的变量。这将安全属性的概念形式化为同样，Fi的值也是相对于.系统跟踪，它包含在该精确执行时间之前的事件。正如我们已经提到的，这说明了我们的公式的R. Corin等人理论计算机科学电子笔记118（2005）129135--∃⟨ ⟩ ⟨⟩类似地，我们可以将扩展系统场景定义为多组（部分实例化）扩展协议角色。3.2检查本地安全属性为了评估本地安全属性，我们将定义3.4扩展到上一节介绍的扩展系统场景：定义3.4设S是一个扩展的系统场景，K是入侵者的初始知识，由代表代理身份及其公钥的常数组成。设tr为初始空迹。S的游程是通过以下步骤的重复序列获得(i) S中的一个非空角色是非确定性地选择的，它的第一个动作p被从中移除。设a为所选角色的标识。(ii) 如果p=tdy：F，则：(a) 如果[F]]tr成立，则继续。 否则，运行停止。(b) t被添加到入侵者的知识ε，K：=K<${t}(c) 事件e=a：p被添加到tr，tr：=tr·e(iii) 如果p=tay：F，则：(a) 检查入侵者ε是否可以使用知识生成tK（见下文），如果是，则将事件e=a：p添加到跟踪：tr：=tr·e。(b) 如果[F]]tr成立，则继续。 否则，运行停止。(c) 如果ε不能生成这样的消息，则运行停止。Q例如，考虑角色：响应者（B，A，Na）=B，[Na aA：F]其中F = e：e = A：Na d B。在响应者B接收到随机数Na之后，F检查A之前是否向B发送了Na。现在，考虑单例场景响应者（b，A，Na）。在这个场景中，只有一个诚实的响应者角色，由b扮演。现在，假设这个响应者角色从入侵者ε接收到一个随机数ni作为Na。因此，根据定义3.4，我们有迹tr=nε：nid bε。 下一步涉及对[F]] tr的求值，以查看局部安全性质F是否成立：显然，我们可以看到[e：e=A：Nad b]] ε：nid b求值为真，将A与ε和Na与ni统一起来。136R. Corin等人理论计算机科学电子笔记118（2005）129··3.2.1执行。我们有一个[]的（beta版本）实现，编码到我们的验证器[3]中。使用它，我们能够执行TMN协议的验证，如下节所示。4TMN协议我们将我们的技术应用于一个众所周知的案例研究，TMN协议[10]。该协议已被彻底研究，例如见[16，14，9]。然而，在本节中，我们提出了一些我们认为以前没有人注意到的漏洞。4.1原始版本TMN的原始版本是为了实现两个用户之间的密钥分配而提出的：信息1.A→S：A，S，B，{R1}pk（S）信息2.S→B：S，B，A信息3.B→S：B，S，A，{R2}pk（S）留言4.S→A：S，A，B，v（R1，R2）我们用v（t1，t2）6表示Vernam加密.这里，密钥R1和R2分别从A和B发送到S在收到消息4之后，A可以获得R2，从而使R2成为A和B之间的共享密钥。4.1.1 TMN协议角色。我们设计和验证技术的第一步是从标准符号中获得协议角色：• 引发剂：[A，S，B，{R1}pk（S）dS：F1，S，A，B，v（R1，R2）aS：F2]• 应答者：B，[S，B，A a S：F3，B，S，A，{R2}pk（S）dS：F4]• 服务器：S，[A，S，B，{R1}pk（S）aA：F5，S，B，Ad B：F6，B，S，A，{R2}pk（S）a B：F7，S，A，B，v（R1，R2）dA：F8]当协议变得很大时，这种转换可能是繁琐和容易出错的;然而，我们相信这一步可以大部分自动化（例如，通过辅助用户的工具6我们目前将Vernam加密建模为普通的对称加密，而不是完全的异或。R. Corin等人理论计算机科学电子笔记118（2005）129137⬦⟩·⟨原始版本的TMN支持者在上面的R2上受到了几次秘密攻击，例如[9]中公开的。因此，我们将集中讨论协议的两个修改版本。4.2第一修改西蒙斯揭露了对TMN的重放攻击[18]。该攻击利用了从A和B发送到服务器的消息（消息1和消息3）可以重放的事实。为了解决这种不确定性，Tatebayashi和Mat-suzaki在消息1和3中引入了时间戳[10]：信息1.A→S：A，S，B，{TA，R1}pk（S）信息2.S→B：S，B，A信息3.B→S：B，S，A，{TB，R2}pk（S）留言4.S→A：S，A，B，v（R1，R2）在这个新协议中，在接收到TA和TB之后，服务器可以检查这些时间戳的及时性。根据Tatebayashi和Matsuzaki的说法，这个新的协议版本继承了R1和R2的新鲜感。以检查是否这是真的，我们可以将R1和R2的新鲜度要求指定为局部服务器S的安全属性：FreshRi=e∈tr：last event（e）（Ri≤msg（e））（对于i=1，2）其中原始msg（）投射事件的消息，定义为msg（x：m y）= m并且谓词last event（e）是为真的原语，i_e是跟踪tr的最后一个事件。这个原语的定义很简单：[[last event（e）]]tr=true itr=trJ·e。Fresh R1和Fresh R2分别表示R1和R2是新鲜的。最后一步涉及决定将FreshR1和FreshR2放在服务器角色的何处。这很容易：我们决定，一旦接收应该放置用于检查接收值的新鲜度的公式。因此，FreshR1可以作为F5，也就是说，在接收到R1同样，我们将FreshR2设置为F7.4.3第一次小说攻击经过验证，我们发现违反了公式F5（即R1的新鲜度）。表1中报告了该攻击。在这种攻击中，入侵者开始替换消息α。1，α。1 J和α。三是α。3J，最后从消息α中得到r1。4.但是，当它想使用138R. Corin等人理论计算机科学电子笔记118（2005）129表1R 1新鲜度攻击。 ε（s）是ε伪装成s。 α和β表示两个不同的游程。信息α。1.a→ε（s） ：a，s，b，{ta，r1}pk（s）信息α。1J.ε（a）→s：a，s，b，{te1，re}pk（s）信息α。2.s→b：s，b，aMessageα. 3.b→ε（s）：b，s，a，{tb，r2}pk（s）信息α。3J。ε（b）→s：b，s，a，{ta，r1}pk（s）信息α。4.s→ε（a）：s，a，b，v（re，r1）消息β。1.ε（a）→s：a，s，b，{t e2，r1}pk（s）在新的运行β中，即使入侵者使用新的（未过期的）时间戳te2，公式F5也不成立，因为r1不是新的（注意s是同一个服务器，涉及运行α和β ） 。 重 要 的 是 要 注 意 为 什 么 这 种 攻 击 代 表 协 议 的 漏 洞 。 根 据Tatebayashi和Matsuzaki的说法，服务器必须检查时间戳的有效性，以保证R1和R2的新鲜度;正如我们在这次攻击中看到的那样，这是不够的。据我们所知，这种弱点以前从未暴露过。4.4二修改确保发起者和响应者对服务器的认证的修改包括以以下方式使用SA和SB，S A和S B分别在S与A和B信息1.A→S：A，S，B，{TA，SA，R1}pk（S）信息2.S→B：S，B，A信息3.B→S：B，S，A，{TB，SB，R2}pk（S）留言4.S→A：S，A，B，v（R1，R2）在接收到消息1和3之后，服务器可以分别认证A和B，因为（通过假设）秘密SA和SB仅在服务器和相应的代理之间共享为了检查协议是否实现了A和B对S的认证目标，我们将其转换为一个公式，该公式表明，如果S收到了显然来自A的消息M（分别为： B），那么它真的是由A（B）发送的。服务器S在接收到A的请求之后认证AR. Corin等人理论计算机科学电子笔记118（2005）129139--第一个消息，所以在这一点上，我们设置我们的公式：F5= e：e=A：A，S，B，{T A，S A，R1}pk（S）d S。类似地，S在第三消息之后 认 证B： F7= ke：e = kB：B，S，A，{T B，S B，R2}pk（S）d Sk。我们对部分测试场景进行了验证，并未发现任何违反上述安全要求的痕迹。因此，我们可以认为协议对于我们测试的系统场景是安全的;当然，可以测试更大的场景以增加对协议安全性的信心。4.5相互认证尽管馆林和松崎没有说明A和B的相互认证，但考虑这种情况是有趣的（Lowe和Roscoe [9]也讨论了这一点。我们可以通过重新定义两个公式，即F3和F2来解释这个要求。我们定义F3来表示A到B和F2表示B到A的认证•A到B的M真实性：F3=Σe：e=ΣA：A，S，B，{TA，SA，R1}pk（S）dSΣ;•B到A的M真实性：F2= e：e = B：B，S，A，{T B，S B，R2}pk（S）dS。继续验证，我们发现了违反F2和F3的痕迹。F3的攻击轨迹很简单，只包含一条消息，从ε（s）发送到b：s，b，a。 但这足以违反公式F3，因为当b接收到s，b，a时，她想检查a是否发送了a，s，b，t a，s a，r1pk（s），而她没有这样做（这种攻击类似于[9]中的攻击7.1）。4.6新型认证攻击在表2中，我们报告了两个违反F2的攻击.表2B to A认证攻击α。1.a→ ε（ s）： a，s，b，{ta，sa，r1}pk（s）α。1. a→ ε（ s）： a，s，b，{ta，sa，r1}pk（s）α。2.ε（ s）→b： s，b，εβ。1. ε→ s： ε，s，a，{te，se，re1}pk（s）α。3.b→ ε（ s）： b，s，ε，{tb，sb，r2}pk（s）β。2. s→ ε（ a）： s，a，εβ。1.ε（ a）→ s： a，s，b，{ta，sa，r1}pk（s）β。3. ε（ a）→ s： a，s，ε，{ta，sa，r1}pk（s）β。2.s→ ε（ b）： s，b，aβ。4. s→ ε： s，ε，a，v（ re1，r1）β。3.ε（ b）→ s： b，s，a，{tb，sb，r2}pk（s）α。4. ε（ s）→ a： s，a，b，v（ r1，re1）β。4.s→ ε（ a）： s，a，b，v（ r1，r2）α。4.ε（ s）→ a： s，a，b，v（ r1，r2）140R. Corin等人理论计算机科学电子笔记118（2005）129--表2（左侧）的攻击是成功的，因为入侵者可以篡改前三个非加密字段 。 注 意 F2 是 如 何 被 违 反 的 ： 当 一 个 接 收 器 扰 乱 了 一 个 α 。 4 ，bneversentmessageb，s，a，tb，sb，r2pk（b）. 表2（右侧）中报告的atta c k更强，因为主体b在a的运行中不存在。我们相信，这些针对TMN协议修改版本的攻击在文献中从未被报道过。5相关工作在本节中，我们将讨论一些相关的工作。在[16]中，Roscoe确定了两种指定协议安全目标的方法：首先，使用扩展规范，其次使用内涵规范。扩展规范描述了协议在行为等效性方面提供的预期服务[6，1，17]。另一方面，内涵规范描述协议的基本机制，以状态或事件的形式[2，21，16，19，15，7]。本文提出的方法属于内部规范的范围，与[16，19]相关。在[19]中，提出了一种需求规范语言。这种语言对于指定协议类的需求集很有用;这些需求可以映射到特定的协议实例上，稍后可以使用他们的工具NRL ProtocolAnalyzer进行验证。这种方法随后被用于指定GDOI安全多播协议[12]。在[16]中，Roscoe提出了一种使用CSP规范描述协议底层机制的方法。该方法由四个步骤组成：首先，识别协议的一个执行点，如果没有相应的合法运行，就不应该到达该执行点。 第二，描述在这个执行点之前应该发生的可能的消息序列;第三，创建一个规范，将所有建模协议参与者的CSP进程分组（这一步类似于我们的场景设置）。最后，使用FDR验证规范。Lowe在[9]中也使用了这种方法刚刚提到的方法采用语言指定的安全属性，erties在一个全球的时尚，而不是我们的技术，处理本地的安全属性。在[4]中，Cremers，Mauw和de Vink提出了另一种用于指定本地安全属性的逻辑。与我们类似，在[4]中，作者通过引用协议角色中出现的变量来定义此外，在[4]中，定义了一种新的身份验证，称为R. Corin等人理论计算机科学电子笔记118（2005）129141同步化，然后与Lowe的内涵规格进行比较。本文中提出的逻辑不能处理同步认证的指定。事实上，我们无法处理较弱的内射认证概念，因为我们无法匹配跟踪中的相应事件。然而，我们相信我们可以扩展我们的逻辑来支持这些属性。简单地说，这可以通过用标签标识符装饰不同的运行并添加一个原语来推理跟踪中先于其他事件发生的事件来实现。6结论和今后的工作我们已经开发了一个跟踪逻辑来表达本地安全属性。使用这种跟踪逻辑，协议设计者可以精确地指定协议应该满足的（本地）安全属性，以实现它已经设计好了。我们的方法与第5节中提到的方法之间的主要差异可以总结如下：(i) 我们的跟踪逻辑公式是本地的参与者，在这个意义上是依赖于主体 这使我们能够更精确地定义属性，即在每个执行步骤中每个主体应该持有什么。此外，我们的技术可用于将规范集成到加密协议的设计中。从方法上讲，这允许将验证阶段整合到设计阶段，加快验证的反馈，并提供基础用于协议工程的集成环境。(ii) 在不使用时态运算符的情况下，我们提出的逻辑可以表达经典的安全属性，包括协议运行期间交换值的新鲜性和真实性。(iii) 我们的逻辑直接应用于协议消息。这允许我们推理（本地）安全属性，而不必使用人工事件消息。作为未来的工作，我们计划将该方法应用于更复杂的案例研究，例如多播协议，例如LKH组通信协议[20]。我们还计划研究如何编写本地安全规范：我们相信这是我们的方法相对于其他全球方法的一个非常重要的优势。致谢。我们要感谢匿名评论者提供的有用意见。142R. Corin等人理论计算机科学电子笔记118（2005）129引用[1] M.阿巴迪输入安全协议就可以了。Journal of the ACM，46（5）：749[2] M. Abadi 和B.布兰切特非对称通信的保密类型。InFoundations of Software Science andComputation Structures，第2030卷，第25-41页。Springer-Verlag LNCS，2001年。[3] R. Corin和S.埃塔勒一种改进的基于约束的安全协议验证系统。In G.普埃布拉湾Hermenegildo，编辑，第9届国际研讨会，SAS 2002，LNCS第2477卷，第326-342页。施普林格，2002年。[4] C.J.F. Cremers，S. Mauw和E.P. de Vink。 在跟踪模型中定义身份验证。 在2003年安全与信任的正式方面讲习班。[5] D. Dolev和A. C.耀公钥协议的安全性。IEEE Transactions on Information Theory，29（2）：198[6] R. Focardi和R. Gorrieri。 进程代数的安全性质分类。 Journal of Computer Security，3（1）：5[7] J.D. Guttman和F.J. Thayer。验证试验与束的结构。Theoretical Computer Science，283（2）：333[8] G. 洛 Casper ： 一 个 用 于 分 析 安 全 协 议 的 编 译 器 。 在 Proc.10th IEEE Computer SecurityFoundations Workshop（CSFWIEEE，1997年。[9] G. Lowe和A. W.罗斯科使用CSP检测TMN协议中的错误。软件工程，23（10）：659[10] D. B.小纽曼M. Tatebayashi，N.松崎数字移动通信系统密钥分配协议。Advances in Cryptology：Proceedings of Crypto[11] C.梅多斯NRL协议分析器：概述。Journal of Logic Programming，26（2）：113[12] C. Meadows，P. Syverson，and I.啤酒在NPATRL中规范GDOI组密钥管理需求。ACM计算机与通信会议论文集，第235-244页。ACM，2001年11月。[13] J. Millen和V. Shmatikov。有界进程密码协议分析的约束求解。在Proc.2001 ACM计算机和通信安全会议上，第166 - 175页。ACM Press，2001.[14] J. C. 米切尔，M。米切尔和U。胸骨切开术组使用murφ进行密码协议的自动分析。1997年安全和隐私会议记录，第141-153页。IEEE Press，1997.[15] L. C.保尔森验证密码协议的归纳方法。计算机安全杂志，6：85[16] A. W.罗斯科安全协议的内涵规范。第九届IEEE计算机安全基础研讨会论文集，第28-38页。IEEE计算机协会出版社，1996年6月10-12日。[17] S.施耐德安全属性和CSP。IEEEComputer Society Symposium on Security and Privacy，第174-190页。IEEE Computer Society Press，1996.[18] G. J·西蒙斯密码分析和协议故障。Communications of the ACM，37（11）：56[19] Syverson和C.梅多斯 密码协议要求的一种形式语言。Designs，Codes，and Cryptography，7（1/2）：27R. Corin等人理论计算机科学电子笔记118（2005）129143[20] C. K. 黄，M。Gouda和S.S. Lam.使用密钥图保护组通信IEEE/ACM Transaction on Networking，8（1）：16[21] T.Y.C.吴和S. Lam.认证协议的语义模型。在IEEE计算机协会安全和隐私研究研讨会上，第178