Maude-NPA的图形用户界面

理论计算机科学电子笔记258（2009）3-20www.elsevier.com/locate/entcsMaude-NPA的图形用户界面S.圣地亚哥，2C。塔尔科特湾，3南。埃斯科瓦尔，4C。梅多斯c，5J. Meseguerd，6aUniversidadPolit'ecnicadeValencia，Valencia，SpainbSRI International，Menlo Park，USAc美国华盛顿特区海军研究实验室d伊利诺伊大学厄巴纳-香槟分校，厄巴纳，美国摘要本文提出了一个图形用户界面（GUI）的Maude NPA，密码协议分析工具，考虑到代数性质的密码系统不支持其他工具，如取消的加密和解密，阿贝尔群（包括异或），和模幂运算。Maude-NPA在重写逻辑、统一和缩小方面有理论基础，并从最终攻击状态执行向后搜索，以确定它是否可以从初始状态到达。GUI可对Maude-NPA验证过程进行动画演示，显示完整的搜索树，并允许用户显示搜索树的最终和中间节点的图形表示这项工作中最有趣的一点是，我们的GUI是使用与Maude相关的声明性图形交互框架开发的，其中包括IOP，IMaude和JLambda。该框架促进了形式化推理工具（在我们的例子中是Maude NPA）之间的交互和互操作，并允许Maude轻松地与其他工具进行通信。保留字：图形用户界面、Maude-NPA、IOP、IMaude、JLambda、Maude1S. Santiago和S.Escobar得到了欧盟（FEDER）和西班牙MEC/MICINN（赠款TIN 2007-68093-C 02 -02 ）以及Generalitat Valenciana （赠款GVPRE/2008/113 ）的部分 支持Carolyn Talcott由美国国家科学基金会资助，资助金额为IIS-0513857。2电子邮件地址：ssantiago@dsic.upv.es3电子邮件地址：clt@csl.sri.com4电子邮件地址：sescobar@dsic.upv.es5电子邮件地址：meadows@itd.nrl.navy.mil6电子邮件地址：meseguer@cs.uiuc.edu1571-0661出版社：Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.12.0024S. Santiago等人/理论计算机科学电子笔记258（2009）31介绍Maude-NRL协议分析器是一种用于分析加密协议的工具，它考虑了所涉及的密码系统的等式属性。这些包括，例如，独家或和迪尼斯-赫尔曼博览会。但Maude-NPA的一个关键属性是可扩展的，也就是说，该工具使用的程序和技术是通用的，因此它们可以很容易地扩展到包括新的方程理论。一个好的图形用户界面可以帮助Maude-NPA的可扩展性和可用性。对于一般用户，它可以提供成功和失败的攻击路径的图形表示，帮助用户了解协议成功或失败背后的原因。对于可能正在尝试新的等式理论的高级用户，它可以提供对搜索树的更近距离的观察，指示在哪里发生状态爆炸，这可能指示必须通过新理论的更好机制来解决的问题。对于工具开发人员来说，仔细观察完整和部分搜索树上的问题节点可以深入了解为什么会发生状态爆炸，以及需要设计或改进什么机制来解决问题。但是，为了提供所有这些服务，GUI必须不仅支持成功的攻击，而且支持整个Maude-NPA搜索过程。因此，它提供的服务必须远远超出通常的GUI所提供的服务。Maude-NPA GUI的上述理想特性不是通过遵循GUI开发的标准方法获得的。事实上，我们严重怀疑使用传统编程语言的标准方法是否能够为我们提供GUI特性的简单性、抽象层次和可扩展性，以及我们在Maude-NPA（其设计仍在发展）等工具中所需的易于发展性。相反，我们的GUI设计方法是基于一种哲学观点，将GUI交互视为另一种形式的重写;具体来说，它是基于一种声明性的、基于重写的GUI设计。我们可以将这种声明性方法总结如下。首先，并发对象交互的重写逻辑方法[20，21]，其中对象转换由重写规则指定，被采用作为Maude-NPA的语义框架，其中加密协议确实以这种方式指定，以及Maude-NPA也就是说，工具的GUI及其与用户的交互也由重写规则指定，其中代理GUI对象与用户交互，并通过消息传递封装Maude-NPA。其次，通过映射这些代理对象，从其重写逻辑规范导出GUI实现S. Santiago等人/理论计算机科学电子笔记258（2009）35对应的图形对象，看起来像Maude基础设施支持的内置外部对象[8]。图形对象的实现和与这些外部对象的消息传递通信是使用支持角色模型的互操作性平台（IOP）及其相关的IMaude库[18]（参见第3节）实现的。用于构建Maude-NPA GUI的基础设施非常通用，扩展Maude以提供一个框架，在该框架之上可以构建许多有趣的应用程序和图形界面。1.1相关工作密码协议的形式化分析一直是一个活跃的研究领域一个是从80年代中期开始的。 其思想是验证使用加密来保证保密性并使用数据认证来确保安全性的协议，以对抗攻击者（通常称为Dolev-Yao攻击者），该攻击者完全控制网络，并且可以拦截，更改和重定向traffic ，自己创建新traffic，执行合法参与者可用的所有操作，并且可以访问合法主体的长期密钥的某些子集。在最简单的情况下，假设密码系统的行为就像黑盒子：攻击者对加密数据一无所知，除非它有适当的密钥。在更复杂的分析中，密码系统可以被假设为服从一组方程性质，就像我们自己的工具Maude-NPA一样，或者甚至可以在密码学家使用的计算模型类型中完全指定。无论采取何种方法，形式化方法的使用都有着悠久的历史，不仅用于提供安全性的形式化证明，而且用于发现在某些情况下在原始协议发布后很久仍然未知已经采取了许多方法来正式验证密码协议。其中最流行的是模型检查，其中协议与攻击者的交互是象征性地执行的。事实上，在有界会话模型（其中会话是代表诚实主体的过程的单次执行）中的协议中的保密性（以及稍后的认证）的模型检查已被证明是可判定的[24]，并且存在许多有界会话模型检查器。此外，一些无界模型检查器，Maude-NPA是其中之一，要么利用抽象来加强可判定性，要么允许非终止的可能性最 早的 工 具， 如 Interrogator [16] 和 NRL Protocol Analyzer （ NPA ）[19]，虽然不是严格意义上的模型检查器，但依赖于状态探索，并且在NPA的情况下，可以用于验证时序逻辑语言中指定的安全属性。后来，研究人员使用通用模型检查器来分析协议，例如FDR [17]和后来的Murphi [22]。6S. Santiago等人/理论计算机科学电子笔记258（2009）3最近的重点是专门为加密协议分析开发的专用模型检查器，例如Blanchet使用模型检查器的优点之一是，它们给出了明确的反例，可以深入了解系统无法满足其规范的原因。在密码协议分析工具的情况下，这样的反例非常适合图形表达：每个进程（包括攻击者进程）可以被写为一系列节点，它们表示发送或接收消息。如果一个进程向另一个进程发送一条消息，则可以将其写为从发送节点开始的箭头到接收节点。流行的串空间模型[27]，包括Maude-NPA在内的许多工具都基于此模型，使用这种符号并将其形式化。因此，协议分析工具的GUI界面传统上集中在模型检查器上。它们通常分为两类：帮助用户指定输入到工具中的协议的界面，以及帮助用户理解输出的界面。后者最早的案例可能是开发的第一个协议分析工具之一，询问器[16]。询问器从不安全状态执行深度优先向后搜索每当它不能沿着一条路径继续前进时，无论结果是否成功，它都会以图形形式显示结果，从而提供该工具搜索过程的动画正常执行的图形表示也被用来帮助用户指定要搜索的攻击状态。最近的一个图形输出界面的例子是Scyther工具[9]。它从角色的实例中进行搜索，生成与之一致的所有跟踪模式。Scyther工具输出这些跟踪模式的图形表示然而，与Interrogator不同的是，它不会输出部分或不成功的模式。关于帮助协议规范的GUI，一个突出的例子是SPAN [7]，AVISPA的配套工具。SPAN是一个图形协议动画器，允许用户检查以AVISPA输入语言HLPSL编写的规范的有效性。SPAN允许用户在没有入侵者的情况下逐步执行协议，确定它是否按照预期的方式运行。SPAN也可以在入侵者在场的情况下用于构建对协议的攻击，尽管它不会自动找到它们;用户必须从工具提供给他的集合中选择执行的每一步另一个以非常不同的方法帮助协议规范的GUI示例是协议推导助手（PDA）[3]。PDA al-S. Santiago等人/理论计算机科学电子笔记258（2009）37允许用户不仅指定单个协议，而且指定协议族，使用图形技术从旧协议中构建新协议PDA还支持与不同规范和分析框架的集成，因此它可以用作与不同正式工具的接口上述所有GUI，除了在一定程度上询问器之外，都有一个共同点。它们帮助用户指定输入到协议分析工具或解释工具的输出。 但他们确实不能提供对分析工具本身的工作的深入了解。但这可能非常有帮助，特别是在Maude-NPA这样的工具中，它采用可扩展的方法来合并新的方程理论。能够检查部分和失败搜索的结果可以帮助用户理解为什么特定协议或新的方程理论会产生状态爆炸或无限循环，以及需要做些什么来解决这些问题。它还可以帮助调试协议规范，类似于SPAN工具。最后，了解部分和失败的搜索可以用于识别协议安全性所依赖的关键假设由于这些原因，我们决定为Maude-NPA开发一个界面，该界面超出了协议分析工具通常提供的GUI，并为用户提供了Maude-NPA搜索树生成过程的完整动画，用户可以随意搜索1.2本文结构本文的其余部分组织如下。在第2节中，我们将介绍Maude-NPA工具及其使用。第3节介绍了IOP、IMaude和JLambda框架的一些背景。在第4节中，我们详细介绍了如何使用IOP-IMaude 框架实际实现Maude-NPAGUI。第5节详细描述了Maude-NPA GUI的功能，包括一些图片。在第6节中，我们总结了一些结论和未来工作的计划。2莫德-NPAMaude-NPA是一种在密码协议中发现攻击或证明其不存在的工具它使用不安全状态的向后搜索它分析有限状态系统，包括一个活跃的入侵者，不抽象或近似的nonces，并与一个无限数量的会话。为了减少搜索空间，它使用各种优化技术，以防止无限循环，并避免无用的过渡到不可达的状态。工具8S. Santiago等人/理论计算机科学电子笔记258（2009）3是公开可用的7，包括用户手册和一些协议示例。该工具的一个主要特点是它支持密码算法所遵循的代数恒等式，如异或、幂运算和加密/解密消去。然而，最终的目标是方程理论oerred的Maude-NPA是用户可扩展的，使新的方程理论落入一个广泛的类可以引入。Maude-NPA使用的协议模型基于Thayer、Herzog和Guttman在[27]中介绍的流行串空间模型。诚实主体的每个本地执行或会话由称为串的正项和负项的序列表示。这些术语由变量、函数符号和常量构成。否定项表示接收到的消息，肯定项表示发送的消息。下面给出了一个链的示例：[pk e（B，NA;A）+，pke（A，NA;NB）−，pke（B，NB）+]这个链告诉我们，主体A首先发送一条消息，该消息带有一个与她的名字（A）连接在一起的随机数（NA），该名字（A）是在B然后，她收到一条用她的公钥加密的消息，其中包含她之前发送的与随机数（NB）（可能来自B）连接的随机数。最后，她发送在B的公钥下加密的随机数NB每个入侵者操作也由一个链表示。以下入侵者链[X−，Y−，（X;Y）+]表明入侵者一旦了解了两条消息，就有能力将它们连接起来。串可以包含变量，除了类型Fresh的项，其总是被视为常量（即，它们被用于随机数）。Strand使用该主体生成的Fresh类型的变量进行注释。以下示例是Maude-NPA中指定的诚实主链，并使用用于随机数n（A，r）的新变量“r“进行注释：：r：：[pk e（B，n（A，r）;A）+，pke（A，n（A，r）;NB）−，pke（B，NB）+]作为避免无限循环的技术之一，Maude-NPA依赖于攻击者永远不会学习一个术语超过一次的假设，因此该工具必须跟踪在向后搜索期间学习了什么术语以及何时学习。向后搜索意味着我们知道入侵者在未来知道什么，但我们对入侵者在过去学到的东西有一个不完整的了解。我们需要确定入侵者得知信息的具体时刻。串空间模型的这种扩充包括状态7在http://maude.cs.uiuc.edu/tools/Maude-NPA/S. Santiago等人/理论计算机科学电子笔记258（2009）39∈|∈/∈∈/∈并不是新的（参见例如[23]，其中包括每个主体的知识的显式表示），但Maude-NPA要求有点不寻常，因为使用向后搜索需要显式表示未来将发生什么。因此，原始的串空间模型被扩展到包括“过去”，“未来”和“现在”方面的时间概念。Maude-NPA中使用的链包括表示执行的当前状态的标记。这个标记将链的过去和未来消息分开，并允许Maude-NPA从最终状态到初始状态通过链执行向后搜索。现在的概念告诉入侵者在现在知道什么，这是由形式t I的表达式表示的。未来的概念意味着入侵者在现在不知道，但在未来肯定会学到的东西未来，其中h由形式t∈/I的表达式表示。在我们的工具中，状态由一组链加上入侵者知识表示，看起来像这样：[m±11，. . . |.... . . 这 是 什 么 ？ ，m±k11]&。 . &[m±1n，. . . |.... . . 这 是什 么 ？ ，m±knn]&{t1/∈I，. ，tm/∈I，s1∈I，. ，smJ∈I}其中：(i) 每一条ch链被分为过去和未来[m±1， … ，m±i|m±i+1， . ，m±k]，其中m±1， . . . ，m±i 是过去，m±i+1是现在，m±i+2. ，m±k是未来。(ii) 初始串是其中过去部分为空的串：[nilm±1， . . . ，m±k]。另一方面，final strand指的是未来部分为空的那一条[m±1， . ，m±k|零]。(iii) 入侵者的知识包含形式为m I和m I的项，其中m I表示入侵者现在知道的m，m I表示入侵者现在不知道但将来一定会学习的项(iv) 初始入侵者知识是没有m∈I项的集合，即，一个形式为{t1/∈I，...，tn/∈I}，而最终入侵者知识是没有m/∈I项的集合，即，一个形式为{s1∈I，...，s m∈ I}。如果可能的话，Maude-NPA从给定的最终攻击状态返回到初始状态执行协议。在实际开始向后搜索之前的第一步是通过生成协议的语法来证明关于不可达状态的引理。 这些语法有助于减少搜索空间（参见[11]），并由工具自动生成。对于在向后执行中发现的每个中间状态，该工具将检查它是否10S. Santiago等人/理论计算机科学电子笔记258（2009）3∈∈∈IJJ/∈∈/∈使用这样的引理（和其他技术，见[12]）无法到达，如果是，则丢弃它。分析必须从描述攻击状态的最终状态开始，并包括一些最终链和一些入侵者知识，通常具有m I形式的术语。最终攻击状态中的变量通过向后缩小进行适当的设置。链和入侵者事实的数量通过向后缩小而增加。让我们简单解释一下如何执行向后收缩分析。给一个状态，我们在状态中固定一个具体的链，并在该链的过去部分中固定一个消息m±ij。如果m±ij是一个非线性n o de（m-ij），那么它（i）或者用入侵者已知的项skE-统一（即，事实SK我出现在给定状态的入侵者知识中），或者（ii）作为新的挑战mij I被包括到给定状态的入侵者知识中，但是仅当它还没有出现在入侵者知识中时。动作（i）意味着由一个链接收的消息m-ij来自i-truder，他知道，留言该动作（ii）意味着入侵者必须知道消息mij，并且我们将其包括在用于该入侵者的挑战集合中。 如果m±ij是一个positi ven o de（m+），则它（iii）被接受但不增加i_truder_kn o_de，或者（iv）E-与入侵者已知的项s_k统一（即，一个事实s k∈I出现在给定状态的入侵者知识中），并且事实s k∈I被转换成s kI. 动作（iii）意味着由一条链与入侵者无关。动作（iv）意味着由一个串输出的消息m ij被入侵者用来学习它，实际上描述了他是何时学习它的。为了允许无限数量的串，tool添加了包含形式为m+such的消息的新串，使得mjE-具有入侵者已知的消息Sk的unifies（即，sk∈I出现在入侵者的知识），并将事实s k我进s kI. 进一步细节和协议示例可以在[13]中找到3互操作性平台（IOP）和IMaude互操作性平台（InterOperability Platform，IOP）[18]是为了促进形式推理工具之间的交互和互操作而开发的。特别是，IOP使Maude能够与其他工具进行通信，从而使其成为为Maude-NPA开发GUI的良好起点IMaude是一组Maude模块，提供在Maude中编程交互式助手所需的基本功能。IOP和IMaude的组合已经在几个项目中使用，包括远程代理（为简单远程机器人的可执行规范提供交互式图形界面）[10]和路径逻辑助手[26，25]（用于可视化的交互式图形界面S. Santiago等人/理论计算机科学电子笔记258（2009）311化和分析细胞信号传导过程的形式模型）。下一小节将更详细地解释用于开发Maude-NPA GUI的主要组件：IOP交互模型、交互式Maude（IMaude）和图形交互包g2 d。3.1IOP交互模型IOP交互模型基于分布式计算的参与者模型[14，15，5，1，2]。Actor模型是一种分布式计算模型，基于独立计算代理（称为Actor）的概念，它们仅通过消息传递进行交互。一个参与者可以创建其他参与者;发送和接收消息;修改自己的本地状态。一个参与者只能通过向其他参与者发送消息来查看他们的本地状态，并且它只能向它的参与者发送消息--要么是在创建时被赋予名称的参与者，要么是它在消息中收到的名称，要么是它创建的参与者的名称。Actor语义只允许公平的计算，在最简单的情况下，这意味着可靠的消息传递。在IOP体系结构中，有一个动态的参与者池，因为可以创建新的参与者，也可以销毁现有的参与者。还有三个独立的进程管理这些参与者：（i）Main，创建和确认系统;（ii）Registry，也称为系统参与者，跟踪当前参与者并维护通信线路;(iii)IOP GUI编辑器，其允许用户与任何参与者8通信。IOP参与者是在系统中注册的一个或多个UNIX风格的进程。每个都有三个FIFO（即，UNIX样式管道）。它的stdin、stdout和stderr文件描述符被重定向到其中一个FIFO。参与者可以在启动时创建（这些是参与者的首字母），以响应某个事件，或者由用户或其他进程要求系统参与者这样做IOP带有一组基本的参与者。对于我们的目的来说，最重要的是：（ i ） System actor ， （ ii ） GUI.editor ， （ iii ） Maude actor ， （ iv ）Graphics2D actor。 Maude参与者是封装在一种能够与其他参与者进行交互的包装器参与者之间的通信是通过IOP注册中心传递的异步消息来执行的，IOP注册中心充当一个邮局，将消息从每个发送者参与者路由到所需的目标参与者。存在几种形式的通信：（i）互动者，即，从一个演员到另一个演员;（ii）元演员，即，从参与者到注册表;以及（iii）接口，即，编辑器和参与者（注册表或任何其他参与者）之间的关系8这不应该与Maude-NPA GUI混淆，因为它们并不相同。12S. Santiago等人/理论计算机科学电子笔记258（2009）33.2互动Maude（IMaude）交互式Maude（IMaude）是一个Maude模块的集合，支持编写交互式Maude应用程序，其中重写与环境通信交错，并且IMaude应用程序IMaude状态具有以下形式[input，st（control，wait4s，requests，environment，log），output]其中符号在Maude中（参见[8]中的LOOP-MODE），每个IMaude组件描述如下：• 控制：它包含当前正在处理的请求或常量就绪（如果没有）。• wait4s：一组等待处理传入消息的挂起任务。• requests：等待IMaude处理的请求队列• environment：包含一组将标识符映射到数据值的条目。• component：一个日志项列表，用于调试，允许在处理请求时记录IMaude提供了接收、应答和调度请求（由传入IOP消息或内部重写生成）的规则，定义了接收对传出IOP消息的回复的持续时间。它提供了确保在需要时进行顺序处理的机制，并支持反应式响应。内置请求包括保存和恢复状态，以及访问文件系统。3.3g2d包和Graphics2d actor图形交互包g2d是一个Java包，旨在简化形式模型和推理系统的交互式可视化开发。它由两个主要组件-JLambda编程语言和解释器以及Glyphish层次结构-以及用于组织窗口元素的其他类组成。JLambda是一种非类型化的Scheme类的词法作用域解释语言，它使用Java的内置响应能力为可用的Java类提供运行时接口。因为它是解释的，所以JLambda表达式可以在运行时计算。Glyphish层次结构是一个Java类层次结构，它为创建交互式图形对象提供了抽象，包括指定它们的形状，S. Santiago等人/理论计算机科学电子笔记258（2009）313颜色、位置和行为（对事件的反应）。多组字形对象可以封装为单个字形对象。g2d包还提供了用于定义和显示节点和边是字形对象的图形的类。4IOP-IMaude中的Maude-NPA GUI我们使用IOP-IMaude开发的Maude-NPA图形界面是公开可用的9，包括安装和用户手册以及一些协议示例。使用IOP-IMaude开发交互式图形助手有两个关键方面也就是说，模型的什么对象（在我们的例子中是Maude-NPA）要表示（以及如何表示），以及通过这些对象可以对模型发出什么请求。一旦这两个方面的决定，有两个部分来实现：扩展IMaude来处理这些输入请求，并产生结果，这样的输入请求作为图形对象的描述呈现给用户。通常，输入请求作为IOP消息从graphics2d actor发送到Maude actor（作为图形界面中的Java事件的结果，例如单击按钮），每个请求的输出作为IOP消息从Maude actor发送回graphics2d actor。请注意，作为请求的输出生成的图形对象的描述是JLambda函数，它实现了IMaude NPA Assistant生成的描述，包括其他必要的操作，如组织窗口元素、菜单和菜单。有多少细节是由IMaude填充的，有多少是在JLambda中完成的，或者换句话说，有多少接口是由IMaude动态生成的，有多少是在设计阶段静态创建的图1总结了Maude-NPA GUI基础设施。现在让我们详细解释一个具体的动作和事件序列，即生成Maude-NPA向后搜索空间的更多级别。如下面第5节所述，通过单击“下一步”按钮激活 此 操 作 。 首 先 ， 在 设 计 阶 段 ， 我 们 创 建 了 一 个 JLambda 函 数nextClosure作为“Next”按钮的事件侦听器。单击时，此JLambda函数将检索要生成的级别数，并按要生成的级别数依次调用另一个JLambda函数nextClosureRec。此函数最终负责将请求发送到IMaude：（sinvoke“g2d.util.ActorMsg”）“send”“maude”gname（concat“nextLevel“（int 1））9在http://www.dsic.upv.es/grupos/elp/Maude-NPA_GUI14S. Santiago等人/理论计算机科学电子笔记258（2009）3Fig. 1. Maude-NPA GUI概述。它调用Glyphish类ActorMsg的方法send，以便使graphics2d actor代表搜索树图对象（由变量gname表示）向Maude actor（由字符串maude在IMaude侧，接收到的IOP消息被添加到请求队列，并使用以下（部分描述的）Maude重写规则进行处理：crl[nextLevel]：[nil，st（processing（reqwait4s，reqQ，es，log），outQ]=>[nil，st（ready，wait4s，（reqQ reqQ1），es'，log），outQ] if es'：= nextLevel（.）/\ reqQ1：= reqreq（'redisplayNPATree，.，reqQ 0））。其中Maude操作符nextLevel最终负责调用Maude-NPA并生成新的环境es'，该环境es在这个重写规则中，另外两个请求reqQ1被添加到IMaude请求队列reqQevel，即extendTree和redisplayNPATree。这两个请求将由IMaude重写规则处理，如下所示。extendTree的规则：（i）扩展搜索树的IMaude本地副本，（ii）向graphics2d actor发送包含存储在es'中的字符 串 的 请 求 extendNPATreegraphics2d actor 来 确 认 。 作 为 响 应 ，graphics2d actor应用定义的JLambda函数extendNPATree来处理字符串，提取新树节点的描述，将信息添加到搜索树图，并向IMaude发送确认。当S. Santiago等人/理论计算机科学电子笔记258（2009）315IMaude 收到确认后，将处理redisplay NPATree请求，并向graphics2dactor发送redisplay NPATreeExp请求，这将强制其重新显示搜索空间的图形表示。然后用户看到扩展的搜索树。5使用接口为Maude-NPA开发的GUI的当前版本允许用户通过显示Maude-NPA获得的搜索空间树来分析密码协议规范。除了将搜索空间显示为树之外，用户还可以获得树中每个状态的文本信息，并且作为新的特殊功能，可以获得状态链的图形表示。让我们考虑著名的Needham-Schroeder公钥协议（NSPK）来演示该工具。我们回顾NSPK的非正式规范，如下：A→B：pk（B，NA;A）B→A：pk（A，NA;NB）A→B：pk（B，NB）其中NA和NB是由相应主体生成的随机数。使用链的NSPK方案的描述如下：：：r：：[pk e（B，n（A，r）;A）+，pke（A，n（A，r）;NB）−，pke（B，NB）+]：：rJ：：[pk e（B，NA;A）−，pke（A，NA;n（B，rJ））+，pke（B，n（B，rJ））−]第一步是选择要分析的协议。用户可以加载他/她自己的协议规范文件或选择提供的示例之一。如第2节所述，Maude-NPA必须生成与攻击状态相关联的语法。如果用户以前分析过相同的协议规范，则可以提供语法文件，以避免生成语法文件。否则，Maude-NPA将生成它，从而增加加载时间。在协议规范中可以定义多个攻击状态，用户必须选择一个。选择协议、攻击状态和（可能）语法后，将出现一个新窗口，其中包含初始化的搜索空间树。 这个初始树包含一个称为“根节点”的节点可以通过GUI告诉Maude-NPA将一个或多个级别添加到树中。有一个名为“Next”的按钮的每个节点 树表示向后搜索的状态它的背景颜色是16S. Santiago等人/理论计算机科学电子笔记258（2009）3如果是常规节点则为淡紫色，如果是初始状态则为绿色，即，解决方案节点。如果一个状态没有子状态（前趋状态），那么它在搜索空间树中的对应节点将被赋予白色。图2显示了找到解决方案节点时NSPK协议图二. NSPK协议的搜索空间树。如第2节所述，对于每个状态，Maude-NPA给出：（i）当前链，（ii）入侵者知识，（iii）消息序列，以及（iv）一些附加数据。存在与搜索树的每个节点相关联的上下文菜单，其允许用户查阅Maude-NPA给出的文本状态信息，或者获得Maude-NPA给出的链和入侵者知识信息的图形表示对于股线的图形显示，我们遵循了股线形状的原始图形表示[27]，但经过修改以表示Maude-NPA的时间概念。图3显示了Maude-NPA状态的图形表示。一条线被画成一系列垂直的点，它们之间由一条双垂直线连接。每个点对应于串中的一个输入或输出消息，也称为节点。正如第2节所解释的，入侵者和诚实主体的行为都是用链表示的，因此在图形表示中显示出来。为了区分入侵者和诚实链，我们使用灰色和黑色表示诚实链，使用浅绿色和深绿色表示入侵者链。目的是为每种类型的股有两种颜色S. Santiago等人/理论计算机科学电子笔记258（2009）317/∈∈∈/∈图三. Strands表示。是代表时间的概念：过去和现在的颜色较浅，未来的颜色较深。Maude-NPA中用于表示时间位置的垂直条在这里由斜线表示入侵者的知识（t I和t I）被集成到图形表示，通过使用不同的颜色的消息附加到每个节点。如果入侵者知道消息（t I），则使用红色;如果消息未知（t I），则使用黑色。 对于还不属于具体链的消息，我们使用单个点而不是垂直的点序列我们希望结束本节，展示与NSPK协议相关的初始状态如何分别由图4和图5中的文本和图形表示来表示见图4。 为NSPK协议找到的初始状态的文本信息。18S. Santiago等人/理论计算机科学电子笔记258（2009）3图五. NSPK协议初始状态的图形显示。6结论和今后的工作我们已经提出了一个图形用户界面的Maude-NPA协议分析工具。Maude-NPA是一个基于不同方程理论的协议模块化推理框架，也是该框架在Maude中的一个实现，其中包含了其中的几个理论。Maude-NPA GUI允许用户以不同的详细程度可视化Maude-NPA的输出出现在搜索空间中的链可以显示为术语或通过使用图形表示来显示，该图形表示以自然的方式显示不同协议消息之间的排序这些特性使得对Maude-NPA产生的结果的分析更容易理解，并简化了分析密码协议的任务GUI的未来工作包括改进Maude-NPA链的图形可视化，并扩展GUI以允许用户使用图形输入指定加密协议，并进行有用的语法检查。一个长期目标是从Maude-NPA分析中自动提取和可视化信息，不仅可以告诉用户他/她的协议不正确，还可以告诉用户安全漏洞的位置以及如何修复。引用[1] G.啊哈Actor：分布式系统中的并发计算模型。麻省理工学院出版社，马萨诸塞州剑桥，1986年。[2] G. 啊哈并发面向对象编程。Communications of the ACM，33（9）：125S. Santiago等人/理论计算机科学电子笔记258（2009）319[3] M. Anlau，D. 帕夫洛维奇河 Waldinger和S. 西谷验证身份验证属性在协议推导助理中。2006年，计算机安全基础和安全协议分析自动推理[4] A. Armando，D.Basin，Y.Boichut，Y.谢瓦利埃湖Compagna，J.奎利亚尔山口汉克斯·德里斯玛，P.C. Heam，O.Kouchnarenko，J.曼托瓦尼，S.Moedersheim，D.von Oheimb，M.Rusinowitch，J. Santiago，M.图鲁阿尼湖Vigano和L.维涅隆Avispa工具用于自动验证互联网安全协议和应用程序。在CAV05的诉讼中。Springer-Verlag，2005.[5] 显利贝克和卡尔·休伊特。 并行进程通信法则。 在Bruce Gilchrist，编辑，IFIPProceedingsof the International Federation for Information Processing Congress 77 ， Toronto ，Canada，August 8-12，1977，pages 987[6] 布鲁诺·布兰切特。基于Prolog规则的高效密码协议验证器。第14届IEEE计算机安全基础研讨会（CSFW-14），第82-96IEEE计算机协会。[7] Y. Boichut，T. Genet，Y. Glouche和O.嗨 使用动画来改进安全协议的形式化规范。在SAR-SSI2007会议记录中，第二届网络架构和信息系统安全会议，2007年6月12日至15日，法国，2007年6月[8] 马努埃尔·克莱拉维尔、弗朗西斯科·杜兰、斯特·冯·埃克尔、帕特里克·林肯、纳西索·马尔·奥列特、乔·梅塞格尔和卡罗琳·L.塔尔科特编辑们关于Maude的一切-一个高性能的逻辑框架，如何在重写逻辑中指定，编程和验证系统，计算机科学讲义第4350卷。Springer，2007年。[9] C. 克莱姆斯Scyther-安全协议的语义和验证。博士论文，埃因霍温理工大学，2006年。[10] G. Denker和C. L.塔尔科特远程代理可靠性的正式检查表。在第五届重写逻辑及其应用国际研讨会（WRLAElsevier，2004年。[11] 蒂亚戈·埃斯科瓦尔，凯瑟琳·米德，还有乔·梅斯格。NRL协议分析器的基于重写的推理系统及其元逻辑属性。Theor. Comput. Sci. ，367（1- 2）：162[12] 蒂亚戈·埃斯科瓦尔，凯瑟琳·米德，还有乔·梅斯格。Maude-NRL协议分析器中的状态空间缩减。在SushilJajodia和JavierL'opez，编辑，计算机安全-ESORICS2008，第13届欧洲计算机安全研究研讨会，西班牙马拉加，2008年10月6日至8日 。 Proceedings ， Volume 5283 of Lecture Notes in Computer Science ， pages 548-562.Springer，2008.[13] Santiago Escobar，Catherine Meadows，and Jose Meseguer.Maude-NPA，版本1.0，2009年3月。可在http://maude.cs.uiuc.edu/tools/Maude-NPA上查阅。[14] C. Hewitt ， P. Bishop ， and R. 史 泰 格 A Universal Modular Actor Formalism for ArtificialIntelligence. 1973年国际人工情报联合会议论文集，第235-245页，1973年8月[15] 卡尔·休伊特。将控制结构视为传递消息的模式。《人工智能杂志》，8（3）：323[16] S.B.弗里德曼南卡罗来纳州米伦克拉克询问者：协议安全性分析。IEEE软件工程学报，13（2）：274[17] G.洛 使用FDR破坏和修复Needham-Schroeder公钥协议。软件-概念和工具，17（3）：93[18] 伊恩·A Mason和Carolyn L.塔尔科特IOP：互操作性平台IMaude：Maude的交互式扩展。电子笔记理论Comput. Sci. ，117：315[19] 凯瑟琳·梅多斯NRL协议分析器：概述。逻辑程序设计杂志，26（2）：11320S. Santiago等人/理论计算机科学电子笔记258（2009）3[20] 乔是梅瑟格尔。 条件重写逻辑作为并发的统一模型计算机科学，96（1）：73 -1 5 5 ，19 9 2 .[21] 乔是梅瑟格尔。重写逻辑和Maude：一个用于基于对象的分布式系统的宽频谱语义框架。在Scott F. 史密斯和CarolynL.塔尔科特，编辑，基于开放对象的分布式系统的形式方法IV，IFIF