加密协议的自动安全验证的Java实现模型

理论计算机科学电子笔记250（2009）123-136www.elsevier.com/locate/entcs加密协议实现的自动安全验证：Jessie项目JanJürjens1开放大学英国摘要在构建安全系统时，一个重要的缺失环节是找到一种实用的方法来建立软件规范及其实现之间的对应关系。我们解决这个问题的情况下，基于密码的Java实现（如加密协议）的方法使用自动定理证明一阶逻辑，通过链接的实现到一个规范模型。 在本文中，我们将详细介绍这种方法的应用程序的开源Java实现杰西的SSL协议。我们还简短地评论了如何将这些结果转移到最近由Sun开源的标准Java安全套接字扩展（JSSE）库中。关键词：自动安全验证，加密协议实现，Java安全套接字扩展（JSSE）1引言许多软件层面的安全事件已被报告，有时可能会造成相当严重的后果。因此，迫切需要对安全系统开发的任何支持。关于基于密码的软件（例如密码协议或使用密码签名的软件），已经做了很多非常成功的工作来正式分析这些 协 议 的 抽 象 规 范 ， 以 确 定 安 全 设 计 的 弱 点 ， 包 括 [14 ， 15 ， 1 ， 16]（cf.[18，10]概述）。最近，已经有一些工作朝着验证安全关键软件的一般实现[8]，并且特别是加密协议的实现[13，7，12，4]。虽然[7，4，6]中报告的方法旨在验证研究小组自己编写的实现（并且[8]不涉及加密协议），但该行1 http://www.jurjens.de/jan。这项工作部分由英国皇家学会资助的项目“基于模型的加密协议实现的形式安全分析”。1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.08.009124J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123当前论文中报告的工作（始于[13，12]）针对的是加密协议的遗留实现。这是因为到目前为止，基于密码的软件通常不是从正式规范自动生成的，甚至不是在安全分析师的控制下创建的。因此，即使相应的规范得到正式验证，实现仍然可能包含与加密算法的不安全使用相关的漏洞。在[17]中可以找到一个密码协议的例子，其设计已经过形式上的安全验证，但后来发现其实现在使用密码算法当前的论文使用一种方法来分析基于密码的实现的安全要求，使用一阶逻辑（FOL）的自动定理证明器（ATP），这是基于[11]中报告的早期工作安全需求可以在FOL中直接形式化，而ATP可以提供高效的推导算法。Java代码链接到一个规范模型，其中密码运算表示为抽象函数，并转换为FOL中的公式。与安全需求的逻辑形式化一起，它们然后作为输入提供给支持TPTP输入符号的任何ATP（这是用于为ATP制定FOL公式的标准），例如e-SETHEO[19]或SPASS [20]。该方法通过在源代码中使用断言来支持模块化的安全如果验证失败是因为实现中包含了安全漏洞，那么可以使用Prolog引擎来生成相应的攻击跟踪。我们的目标不是提供Java代码的完整形式化验证，而是以尽可能自动化的方式增加对加密协议实现所强制执行的安全属性的理解。目前，我们假设在加密协议实现中调用的加密算法已经正确实现（我们的目标是验证它们在加密协议中正确使用）。此外，由于出于效率原因而引入的抽象（如下面所解释的，例如从消息的发送者的身份进行抽象），该方法可能产生假警报（然而，其在实际示例中尚未出现）。目前的文件的目标是报告的方法的应用程序的开源Java实现杰西的SSL协议。我们还简要说明了如何将这些结果转移到Sun最近开源的标准Java安全套接字扩展（JSSE）库2代码分析这里使用的分析方法与著名的Dolev-Yao对手模型进行安全分析。这个想法是，对手可以读取通过网络发送的消息，并将其收集到他的知识集中。攻击者可以合并和提取知识集中的消息，并可以在通信链路上删除或插入消息。然后，可以使用这个对手模型来形式化安全需求。例如，数据值对对手保持秘密，如果它J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123125•enc（E，K）（加密）•dec（E，K）（decryption）•hash（E）（hashing）•sign（E，K）（签名）•ver（E，K，EJ）（签名验证•kgen（E）（密钥生成）•inv（E）J（逆键）•conc（E，E）（concatenation）•头（E）和尾（E）(head和concat的尾部）。图1.一、 a）工具-JavaSec套件的流程;b）抽象加密操作永远不会出现在对手的知识集中。我们解释了如何将Java程序链接到指定模型，以及如何生成FOL公式，这些公式作为ATP的输入。相应的工具流程如图1a）所示。由于篇幅限制，我们无法解释将Java代码链接到规范模型所需的所有步骤。我们的解释仅限于对数据保密性的分析。这里的想法是使用一个谓词knows，它定义了对手在与协议参与者交互时通过在易受攻击的通信线路（如互联网）上读取、删除和插入消息而可能获得的知识的界限。确切地说，知道（E）意味着对手可以在协议执行期间知道E。对于任何假定保持机密的数据值s，必须检查是否可以导出knows（s）。从逻辑的角度来看，这意味着人们考虑使用符号运算从诸如变量、键、随机数和其他数据之类的数据生成的项代数-包括图1b中的那些。这里，符号E、EJ和K表示以这种方式归纳构造的项。例如，术语ver（E，K，EJ）表示布尔值，其表示信号的验证是否为使用密钥K对纯文本EJ的真实E是成功的。这些符号运算是JavaTM Cryptography Architecture（JCA）[9]。注意，JCA中的加密函数是作为几个方法实现的，包括对象创建和可能的初始化。与我们的分析相关的是由digest（）、sign（）、verify（）、generatePublic（）、generatePrivate（）、nextRecorder（）和doFinal（）方法执行的实际密码计算（以及预先给定的参数，可能使用update（）方法），因此其他方法基本上被抽象掉了。还要注意，密钥和随机生成方法generatePublic（）、generatePrivate（）和nextKey（）不是图1b）中的密码项代数的一部分，而是通过引入表示密钥和随机值的新常数（并且在generateKeyPair（）的情况下使用inv（K）操作）在代数这个术语中，我们定义了方程dec（enc（E，K），inv（K））=E和ver（sign（E，inv（K）），K，E）=true，对于所有的项E，K，以及关于连接、head（）和tail（）的通常定律。数据流“使用”JavaAnnota−代码代码tions关于Assert文本报告攻击跟踪断言生成器控制流图攻击发生器FOLPrologfmla方案式发生器JavaSec套件自动定理证明器Java编辑器CFG发生器分析仪126J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123输入公式（construct_message_1，axiom，（！ [E1，E2]：（（知道（E1）知道（E2））&=>（knows（conc（E1，E2））knows（enc（E1，E2））knows（sign（E1，E2）。&&输入公式（construct_message_2，axiom，（！ [E1，E2]：（knows（conc（E1，E2））=>（knows（E1）&knows（E2）。图二. 一些一般的密码公理见[10]关于这一点的更多细节。定义为适用于给定系统的谓词定义如下。对于每个公开已知的表达式E，给出语句knows（E）。为了模拟这样一个事实，即对手可以通过从他所知道的表达式中构造新的表达式来扩大他的知识集，包括使用密码运算，为这些运算生成公式，图2中给出了一些示例。我们对FOL公式使用TPTP符号，这是许多ATP的输入符号，包括我们使用的（e-SETHEO [19]）。这里的意思是逻辑连接和！[E1，E2]对于E1，E2上的所有量化。我们解释了一个Java程序如何与一个规范模型相关联，该模型产生了一个逻辑公式，描述了对手和协议参与者之间的交互（图1a的左下部分）。我们首先解释没有循环和并发的Java简化片段的翻译。此外，为了简化变量的处理及其赋值，我们首先使用标准变换来简化从程序到逻辑的转换。它们是必要的，因为在编程语言中，程序变量有状态，而在经典逻辑中变量是无状态的。方法调用中的副项通过遍历方法定义来处理。当这变得不可行时，可以向方法声明添加注释，抽象地捕获方法（及其副作用）的计算。静态单赋值程序像往常一样转换为静态单赋值（SSA）格式。下面，将变量a设置为值v将被形式化为模型上的逻辑约束a=v（任何有效的公理模型都必须满足这一约束，因此它相当于一个赋值）。从变量a中获取值是通过使用该变量来建模的。我们可以忽略变量数据定义，因为它们在ATP的TPTP输入符号中是不必要的。类似地，我们可以将变量初始化视为赋值。在全局变量的局部重定义的情况下，我们假设使用适当的重命名来避免混淆。为了得到程序的FOL公式，我们首先构造捕获程序抽象行为的规范模型。 例如，这可以在生成控制流程图的工具（如Code Logic）的帮助下完成，或者通过从协议的文本规范手动构建它。我们构造的模型是一个状态机，其转换带有形式为await消息e如果符合其输入模式的消息到达（或如果输入模式为空）并且满足其条件，则执行状态当过渡J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123127图三. 加密协议（如SSL）中的通信被执行，它的动作将被执行，然后在状态机中评估下一个转换。在标签await消息e中，表达式e由消息名msg和变量列表组成，当通过网络接收到名为msg的消息时，这些变量类似地，输出消息e为了确定发送和接收的数据，我们首先处理实现发送或接收过程的机制。我们假设每个消息都由一个消息类表示。它存储要写入通信缓冲器的数据。相反，这个类也可以从通信缓冲器读取消息（图3中显示了这种通信原理）。我们发现这种机制经常（特别是在第3节讨论的Jessie项目中）使用方法write（）（用于发送消息）和read（）（用于接收消息）来实现。此外，方法write（）（resp. read（）），它们在类java.io.OutputStream（resp.InputStream）用于以传递的参数或进行的分配的形式标识通信过程中的各个消息部分。更详细地说，通信实现如下：使用方法调用msg。write（dout，version），消息msg被写入输出缓冲器dout。这样一个方法调用的每一次出现都可以被识别，并与指定模型中的抽象函数send（msg）相关联。方法调用dout。后来的人会说，msg=Handshake。read在协议的握手部分期间从缓冲器读取消息。作为一个示例，图4中给出了初始化和发送ClientHello消息的代码片段。最后，我们将表达式到Java中变量的每个赋值assgmt映射到相应逻辑变量上的逻辑谓词passgmt消息e的参数列表可以是空的，并且在不需要它们的情况下条件g等于真对于从上面定义的状态机到FOL公式的映射，我们将Java语法中的布尔表达式映射到TPTP格式的逻辑语法例如通过用二进制布尔函数equal（）替换相等测试==，见图4。 初始化并发送ClientHello消息128J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123“PRED（1）= Δexp1，. ..，expn.knows（exp1）.. . 已知（expn）已知（exp1，.. .，实验，实验”knows（exp（exp1，.. .，expn）预测（lJ）图五.变迁谓词其他布尔连接词也是假设现在我们被给定一个转换l=（source（l），event（l），guard（l），msg（l），target（l）），其中guard（l）为arg1，.，argn），和msg（l）exp（arg1，...，argn），其中保护和消息的参数argi是存储在协议过程期间交换的数据值的变量。假设转移LJ是状态机中的下一个转移。 对于每一个这样的转换，我们定义一个谓词PRED（l），如图1所示五、如果下一个转变lj不存在时，PRED（l）通过在图5中将PRED（lJ）替换为true来定义。式形式化的事实，如果对手知道表达式exp1，.，expn验证条件cond（exp1，.，expn），则他可以将它们发送到协议参与者之一以接收消息exp（exp1，. ，expn）作为交换，然后协议继续。通过这种形式化，如果无法从协议定义的公式中导出已知信息，则数据值s为了构造上面的递归定义，我们假设状态机是有限的。和无周期。该构造可以被细化为允许循环（通过使用无限数组来更新循环中的变量），递归和并发线程。对于要分析的系统中的每个对象O，这给出了谓词PRED（O）=PRED（l），其中l是O的状态机中的第一个转换。 给定协议的整个FOL公式中的公理则是表示公知表达式的公式的合取，图2中的公式，以及协议中每个对象O的公式PRED（O）上面定义的公式作为公理写入TPTP文件。要检查的安全性要求被写入TPTP文件作为推测（例如，如果要检查值秘密的秘密性，则为knows（secret）然后ATP将检查猜想是否可以从公理推导出来在秘密的情况下，结果解释如下：如果知道（秘密）可以从公理中导出，这意味着对手可能会知道秘密。如果ATP返回不可能从公理中推导出已知（秘密），这意味着对手将无法获得由秘密表示的数据（相对于我们的系统和对手模型）。3示例应用程序：SSL项目JESSIE我们将上面概述的方法应用于项目Jessie中Internet安全协议SSL的实现，该项目是Java安全套接字扩展（JSSE）的开源实现SSL是保护http连接的事实上的标准，然而，它在过去一直是几个重大安全漏洞的来源[2]，因此是安全分析的一个有趣的目标。在本文中，我们集中J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123129见图6。 在SSLSocket.java中实现的加密协议使用RSA作为加密算法并提供服务器身份验证的SSL片段（参见图（六）。整个JESSIE项目目前包含大约5 MB的代码，但与SSL直接相关的部分包含不到700 KB的大约70个类。因此，它是具有挑战性的，但可管理的正式分析。为了将代码与图6中的规范联系起来，我们首先解释模型级别的重要元素如何在实现级别实现。这是通过以下三个步骤完成的：• 第1步：在执行一级确认发送和接收程序中传输的数据。• 第2步：解释传输的数据并与序列图进行比较。• 步骤3：在实现级别识别和分析加密保护。在步骤1中，检查实现级别的通信，并确定如何在源代码中找到发送和接收的数据。然后，在步骤2中，将含义分配给数据。然后将各个消息的解释数据元素与适当的元素130J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123见图7。 握手消息在模型中。在步骤3中，描述了如何从源代码中的模型中识别防护。步骤1：在我们的特定协议中，建立连接是通过两个方法完成的：客户端的doClientHandshake（）和服务器端的doServerHandshake（），它们是jessie-1中SSLsocket类的一部分。0。1/org/metastatic/jessie/provider.在一些初始化和参数检查之后，这两种方法都执行客户端和服务器之间的交互，如图6所示。每个 消 息 都 由 一 个 类 实 现 ， 其 主 要 方 法 由 doClientHandshake （ ） rp 调 用 。doServerHandshake（）方法。相关数据见图7。步骤2：为了能够将实现与抽象模型进行比较，我们必须首先确定单个数据如何在代码级别上实现，然后能够验证这是否正确。我们以ClientHello方法向消息缓冲器写入的变量random为例来解释这一点。通过检查变量写入的位置（类Random中的方法write（randomparameter）），我们可以看到randomparameter的值由该类构造函数的第二个参数确定（参见图8）。因此，变量的内容取决于当前随机对象的初始化，因此也取决于程序状态。 因此，我们需要追溯对象的初始化。在当前程序状态下，随机对象由构造函数传递给ClientHello对象。 这再次在SSLSocket中初始化Handshake对象时交付。doClien-tHandshake（）到Handshake的构造函数。在这里（在doClientHandshake（）中），我们可以找到传递的Random对象的初始化。第二 个 参 数 是 www.example.com 包 中 SecureRandom 类 的 generateSeed （ ）java.security。这个调用决定了当前程序状态下random的值因此，值random被映射到MES中的模型元素RC见图8。 random的构造函数J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123131见图9。 ClientHello消息中的数据sageClientHello在模型级别上 为此，方法java.security.SecureRandom.generateSeed（）必须正确实现。为了增加我们对实现与模型一致的假设的信心在图9中，列出了模型的ClientHello消息的元素。这里显示了第一个消息通信的哪些数据元素被分配给doClientHandshake（）方法中的哪些元素例如，在握手之前插入JessiedoClientHandshake（）方法中阶段已成功完成：.断言是的。equal s（finis. 给MD5H一个小时，很快。（gtMD5Hash（h））&&阵equals（finis. getSHAHash（），验证。getSHAHash（））请注意，对接收到的消息类型是否正确的检查也作为断言生成，如下所示，尽管这只是隐式包含的在我们的抽象规范中。断言.ΣMSG. getType（）= Handshake。类型. 服务器问候第3步：我们现在通过一个例子来解释如何在代码级别上识别图6中SSL规范中的保护，以及如何检查这些保护实际上是否正确实现。为了解释这个想法，我们集中在图6中的检查证书保护上。通过手动检查源代码，可以直接在以下点之后找到checkServerTrusted方法的调用：132J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123见图10。 调用checkServerTrusted方法消息Certificate和Finished被接收，其对应于在模型中选中Certificate guard（相关程序片段的摘录见图10）。对于检查证书守卫，我们现在解释如何在语义层面上建立它与守卫ver（证书S）的对应关系，以及如何在每个程序运行中达到它。图11所示的调查显示，首先查询证书链peerCerts随后，验证证书链中具有前任密钥的每个证书对于这些，它是检查是否是由一个推力锚。如果没有，则抛出一个CertificateException，这将导致中止握手对话。函数doVerify（Signature sig，PublicKey key）用于验证证书。J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123133见图11。 确定checkServerTrusted方法的执行我们现在将解释该工具如何使用上面定义的注释自动验证代码强制执行必须根据协议规范执行的检查同样，设p为接收协议消息的程序点，q为发送下一个消息的点设g为根据规范必须在程序点p和q之间检查的条件。然后，该工具验证条件g在执行点p和q之间被程序强制执行。为了验证这一点，我们的工具检查p和q之间的条件和异常，以确定g是否被强制执行，基于使用控制流图的控制流分析，其中必须检查代表程序点p和q的节点之间的所有路径，以查看它们是否强制执行g。作为一个例子，我们考虑由客户端根据图1中的规范执行的保护g=ver（certS）第六章我们将详细解释我们的工具如何自动验证Jessie实现正确地执行此保护。该工具利用控制流程图，可以使用可用于此目的的工具（在我们的情况下使用工具CodeLogic）从源代码12个。根据基于文本规范定义的注释，检查g由方法调用session.trustManager实现。checkServerTrusted（peerCerts，suite. getAuthType（））（如果检查失败则抛出异常）。通过跟踪各种写和读调用，该工具还可以确定程序分别指向何处。q位于最后一条消息被接收134J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123图12个。CheckServerTrusted的控制流图resp.下一个消息被发送出去。在这种情况下，应该检查接收使用命令MSG=握手在图12中标记为p的程序点读取（din，certType）。这对应于图6中序列图中客户端接收到消息证书（X509CertS）的点。 在应该检查保护之后的下一条消息使用msg命令发送。在图12中的程序点q处写入（dout，version）。这对应于在图6中的序列图中在客户端侧发送消息ClientKeyExchange（encKS（ PMS ） ） 的 点 。 因 此 ， 该 工 具 必 须 检 查 程 序 的 每 次 执 行 ， 方 法 调 用session.trustManager.checkServerTrusted（peerCerts，suite.getAuthType（）将在程序点p和q之间执行。 该工具证明了这一点-主要是利用程序推理规则。非正式地，在这个简单的例子中，通过检查图12中的控制流程图，可以看出这确实是这种情况，其中可以看出，除了检查g的路径之外，没有从p到q的路径，因为跳转到catch块导致程序的终止然后，我们使用我们的工具根据相关的安全要求（如保密性和真实性）验证了抽象的控制流程图。在每一种情况下，这些性质都在不到一分钟的时间内得到了证明。例如，验证SSL协议中通信的主密钥的保密性需要2秒J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123135并通过e-SETHEO套件中包含的eprover实现。4Java安全套接字扩展（JSSE）在研究了JESSIE1.0.1中加密协议的一个实现之后，我们的目标是在J sse中相同协议的参考实现中重用我们的验证工作，JSSE是标准JDK 1.4版以来的库。幸运的是，Sun已经将JDK 1.6+实现作为一个名为OpenJDK的开源项目发布。最新的Jsse 库 的 源 代 码 可 以 从 下 面 的 Subversion 存 储 库 中 查 看 ：https://openjdk.dev.java.net/source/browse/openjdk/jdk/trunk/jdk/src/share/classes/sun/security/ssl. 为了评估我们的结果从Jessie到JSSE的可移植性，我们比较了JESSIE和JSSE的握手协议的实现。虽然在JSSE中 实 现 不 同 ， 但 我 们 能 够 确 定 握 手 协 议 模 型 中 所 有 符 号 的 相 应 实 现 。doHandshake协议主要在JESSIE1.0.1库的org.metastatic.jessie.provider.SSLSocket类中实现，而在OpenJDK 1.6的JSSE库中，该协议主要在sun.security.ssl.HandshakeMessage类中实现。然而，符号的命名可以追溯到实现。我们计划在将来的工作中利用这些相似性来验证JSSE库。5结论我们详细介绍了一阶逻辑自动定理证明器的应用，以验证SSL协议的开源Java实现我们还解释了如何将结果传输到新的开源JSSE库。虽然我们的方法不是完全自动的，并且需要一些插入断言到源代码中的插件，但事实证明，即使在工业使用的软件项目中，它也可以通过合理的插件来应用，正如JSSE实现所证明的那样。我们正计划使用模式识别方法使该方法更加自动化，以实现诸如发送和接收消息之类的重复功能。未来的工作包括计划研究基于算法游戏语义的组合验证技术的使用[3，5]。确认感谢David Kirscheneder、Haoyang Lin和Chang Li在Jessie的实现细节方面提供的帮助，以及评审人员对演示文稿的建设性意见。136J. Jürjens/Electronic Notes in Theoretical Computer Science 250（2009）123引用[1] Abadi，M.和A. Gordon，A calculus for cryptographic protocols：The spi calculus，Informationand Computation148（1999），pp. 一比七十[2] Abadi，M.和R. Needham，Prudent engineering practice for cryptographic protocols，IEEETransactions on Software Engineering22（1996），pp. 6比15[3] Abramsky，S.，D. Ghica，A. Murawski和C. Ong，将游戏语义应用于组合软件建模和验证，在：TACAS，计算机科学讲义2988，2004年，pp.421-435[4] Bhargavan，K.，C.Fournet，A.D.Gordon和S.Tse，VerifiedInteroperableImplementationsofSecurityProtocols。，in：CSFW（2006），pp. 139-152.[5] Dimovski，A.，D. Ghica和R. Lazic，一个用于开放过程程序的反例引导的精化工具。SPIN，LectureNotes in Computer Science3925，2006，pp. 288-292。[6] 戈登A. D、安全协议的可证明实现。，in：LICS（2006），pp. 345-346[7] Goubault-Larrecq，J.和F. Parrennes，Cryptographic protocol analysis on real C code，in：VMCAI363-379.[8] Heitmeyer，C.，M. Archer，E. Leonard和J. McLean，嵌入式系统分离内核中数据分离的形式化规范和验证，CCS（2006），第10页。346-355[9] JavaTM密码体系结构，http://java.sun.com/j2se/1.5.0/docs/guide/security/CryptoSpec.html。[10] 我是J. ，“SecurreSystemsDevelopmentwithUML“，Springer-Verlag，2004年。[11]Jurje ns，J.，2005 年，美国软件工程师学会第27届国际软件工程会议（ICSE 2005），IEEE ComputerSociety，2005年，第102 - 104页。322-331.[12] Jurje ns，J.，安全性分析是将Javaprogramanga neremp r ang a n e r emp rang an er emp r a n e r e m pranganer e ne r a n e r e ners，其中：S. Easterbrook和S. Uchitel，editors，21st IEEE/ACM International Conference on AutomatedSoftware Engineering（ASE 2006），ACM，2006，pp. 167-176。[13] 我是J. 和M. 你很幸运，我们的安全分析是有问题的。，n：D. R edmile s，T. EllmanandA. Zisman，editors，20th IEEE/ACM International Conference on Automated Software Engineering（ASE 2005），ACM，2005，pp. 392-395.[14] Lowe，G.，使用FDR打破和修复Needham-Schroeder公钥协议，软件概念和工具17（1996），pp.93比102[15] Lowe ，G. 和B. Roscoe ， Using CSP to detect errors in the TMN protocol， IEEE Transactions onSoftware Engineering23（1997），pp. 659-669[16] 保尔森湖验证密码协议的归纳方法，计算机安全6（1998），pp. 85比128[17]Ryan，P. and S. Schneider，对递归认证协议的攻击，信息处理快报65（1998），pp. 七比十[18] Ryan，P.，S. Schneider，M. Goldsmith，G. Lowe和B. Roscoe，[19] Stenz，G.和A. Wolf，E-SETHEO：An automated3theorem prover，in：R.Dyckho Dyckho，editor，Automated Reasoning with Analytic Tableaux and Related Methods （ TABLEAUX2000 ） ， LectureNotes in Computer Science1847，pp. 436-440[20] 我们在这里，C.， 联合 Brahm，T. Hill enbr andd，E. K ee n，C. 我的天啊。 Topic，Spassversion2.第18届自动演绎国际会议（CADE-18），计算机科学讲义2392（2002），pp. 275比279