团队自动机：安全领域中的建模与验证

理论计算机科学电子笔记128（2005）105-119www.elsevier.com/locate/entcs团队安全自动机– A Survey莫里斯·HGabriele Lenzinib Marinella PetrocchicaIstituto di Scienza e Tecnologie dell 'Informazione，CNRAreadellaRicercadiPisa，ViaG. Moruzzi 1，56124比萨，意大利maurice. isti.cnr.itb特文特大学计算机科学系P.O. Box 217，7500 AE 荷兰恩斯赫德lenzinig@cs.utwente.nlc信息和电信研究所，CNRArea della Ricerca di Pisa，Via G. Moruzzi 1，56124比萨，意大利marinella. iit.cnr.it摘要在[33]中，Kleijn提出了一项关于使用团队自动机对计算机支持的合作工作领域的现象进行规范和分析的调查，特别是相关概念。群件系统。在本文中，我们提出了一个调查的使用团队自动机的具体化和分析的一些问题，从安全领域。 特别是，我们展示了如何 团队自动机可以充分地用于建模和验证各种访问控制策略、多播/广播通信协议和通用（密码）通信协议。关键词：团队自动机，访问控制，安全性，密码通信协议1介绍团队自动机（TA）最初是在计算机支持的协同工作（CSCW）[5，18]的背景下引入的，但后来证明它们也在安全背景下使用[3，4，6，7]。在[33]中，他们对CSCW的使用进行了调查。在本文中，我们调查了TA的安全使用。TA受到输入/输出自动机（IOA）的启发并形成其扩展[40]。与IOA一样，TA形成了一个灵活的框架，用于对分布式和反应式系统组件之间的通信进行建模他们是模特1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.044106M.H. ter Beek等.理论计算机科学电子笔记128（2005）105系统的逻辑架构，仅用自动机、动作的角色和这些动作之间的同步来描述它。 TA是由组件自动机（CA）组成的，组件自动机是没有最终状态的普通自动机，它们的动作分为输入、输出和输出。和内部行动。 CA和IOA之间的唯一区别是IOA是定义输入启用的：在每个状态下，必须可以执行每个输入操作。组成TA的关键是定义其组成CA通过同步进行通信的方式。 尽管IOA是根据一种非常严格的组成自动机的方法来构造的，从而导致由其组成部分唯一定义的复合自动机，但不存在由其组成的唯一TA。一组CA。相反，整个范围的TA，区分只有他们的同步，可以组成在这一组CA。特别地，与IOA的情况相反，在TA中，输出动作也可以被同步。这些框架的严格设置允许人们以数学精确的方式制定和在实际的大型计算机系统中，安全性是一个大问题，这些框架允许对其设计的正确性进行正式证明此外，这种正式的方法迫使人们明确地描述自己的设计，它可能会建议新的方法，否则看不到。TA在IOA方面的特殊特征在特定情况下是有用的，我们将在下面描述其中的两个 在[4]中，ter Beeket al. 使用输出动作的同步来定义所谓的对等和主从同步。这是两个重要的CSCW现象，因此引入它们是出于明确的实用动机。然而，在IOA中两者都不能区分。在[6]中，ter Beek等人使用在CA集合上选择TA的同步的自由度来定义所谓的多播合成算子Jmj，作为发送者和接收者的总集合的子集J之间的一对J在IOA中无法区分这一概念。本文是对过去四年中使用TA进行安全问题规范和分析的研究的教程概述。 特别是，它涵盖了ter Beek等人 [4]对几种访问控制策略的规范-随后由ter Beek和Bloem在[3]中验证-以及本文作者正在进行的工作，即开发用于分析安全属性的TA框架-在[6]中启动并在[7]中进一步发展。我们现在更详细地描述这些方法中的每一种。11最近，Egidi和Petrocchi首次尝试使用TA分析隐私属性[16]。虽然他们的工作太新，本文无法进行全面讨论，但我们注意到，作者使用TA来建模和验证安全协议M.H. ter Beek等.理论计算机科学电子笔记128（2005）105107在[4]中，ter Beek等人证明了TA在捕获信息安全和保护结构以及这些结构之间的关键协调方面的潜力。在空间访问隐喻的基础上，各种已知的访问控制策略在TA中的同步方面被正式指定。在[3]中，ter Beek和Bloem还尝试使用模型检查器SPIN[32]验证一些结果规范。在[6]中，随后，本文的作者展示了潜在的用于对安全组播和广播通信进行建模。为此，TA被用来对特定流签名协议的实例进行建模。多播和广播通信中典型的一对多和一对所有通信由TA以原生方式捕获为构成TA的CA集合之间的同步最后，本文作者在[7]中提出了一个用TA进行安全性分析首先，他们定义了TA的不安全通信场景，基于向安全通信协议的TA模型添加所谓的最一般入侵者入侵者被建模为一个积极的代理人能够在诚实的代理人之间的通信中断。这种不安全的场景非常普遍，足以包含各种通信协议。其次，根据TA对[26]中的广义非演绎合成第三，该框架被应用于证明完整性是有保证的案例研究中，TA模型的一个特定的实例的高效多链式流签名（EMSS）协议族的[46]。这个案例研究表明了这种TA方法对于一个现实的流签名协议的有效性，从而便于那些熟悉其他方法的人进行简单的比较。在安全领域中使用基于自动机的形式主义来规范和验证属性的方法并不是唯一的，但近年来已经变得非常流行[11，12，29，35，38，44，45，47]。我们简要地描述了一些最接近本文调查的方法Chen等人正在进行的关于软件安全属性的形式化验证的工作在[11]中讨论。他们的具体方法是将待验证的特定软件建模为下推自动机，将安全属性建模为有限自动机，而模型检查技术则用于实际执行验证。他们的方法的应用可以在[12]中找到，其中描述和分析了三种不同的UNIX代理在敌对的环境中，专注于代理的隐私属性。108M.H. ter Beek等.理论计算机科学电子笔记128（2005）105在[47]中，S chneider将所谓的 安 全 自 动 机 定 义 为一种类似于普通（有限）自动机的Bu é c hi自动机，并将其应用于一个简单的 访问控制模型。类似于IOA和TA的合成，定义了所谓的连接安全自动机。还有待观察的是，复杂的访问控制策略与授权和撤销是否可以通过安全自动机或Chen等人的方法进行建模。. 我们预计，在[4]中，ter Beek et al. 对这些政策使用TA。Lynch 在 [38] 中 使 用 IOA 对 涉 及 简 单 共 享 密 钥 通 信 与 Difference-Hellman密钥分发协议[14正如作者自己所指出的，她的方法的一个局限性是，该协议只允许纯粹被动的窃听者监听通信。这种选择简化了合成结果的公式化，因为窃听者不能改变通信的过程，例如。 通过假装是诚实的参与者进行通信。她的方法确实提供了有吸引力的组合推理技术。我们预期我们在[7]中的TA设置中建模一个主动入侵者。最后，另一个相关的方法可以在[44，45]中找到，其中Oheimb等人介绍了交互式状态机（ISM）-IOA的另一个扩展-并将其应用于安全分析。事实上，ISM 被用于建模和分析Lowe [37]修正版本中的经典Needham-Schroeder公钥认证协议。这种方法的一个优点是，它允许通过定义ISM和证明定理来自动验证，在定理证明器Isabelle/HOL [42]中。缺少的是在更复杂的通信协议上进行组合推理的可靠技术。我们预计在[7]中我们定义了TA的成分分析策略本文的结构如下。在第2节中，我们非正式地描述了如何使用TA，之后在第3-5节中对上述论文进行了综述。第六节是论文的总结。2团队自动机在本节中，我们将非正式地描述TA的主要特征以及如何使用它们，而不是在所有技术细节中定义框架。有关TA的更多信息，读者可参考[2，33，50]。要将系统建模为TA，首先必须识别组件。它们中的每一个都应该以自动机的形式给出一个描述-一个易于理解的状态转换模型，它构成了许多模型检查工具中系统描述的基础[32，34]。基于公共动作同步的思想，这些组件可以M.H. ter Beek等.理论计算机科学电子笔记128（2005）105109为了合作而连接。在每个组件中，必须区分内部操作（不能与其他组件同步）和外部操作（可用于同步组件，并可能受到同步限制）。通过将这些不同的角色分配给行动，可以描述许多类型的协作。因此，对于每个外部动作，单独地做出关于组件应该如何以及何时同步于该动作的决定。如果该动作被认为是可能不在组件的本地控制下的被动动作如果这种角色之间的区别外部行为是不必要的，那么选择是任意的。一个自然的选择是将其作为所有组件中的输出操作。一旦已经确定了每个外部动作的同步约束，就可以应用例如利用极大性原理构造出满足所有约束条件的唯一TA。IAO中使用的组合物，例如由所谓的max-aiTA在CA集合上镜像。在这样的max-ai TA中，对于所有动作，所包括的CA之间的同步是所有且仅是所有CA参与的在其字母表中具有动作的那些转换。因此，TA框架支持基于组件的系统设计，使明确的作用的行动和选择的过渡，管理组件之间的合作。关键的特点是自由选择的同步收集在过渡关系的TA和同步输出动作的可能性。事实上，为了使TA能够通过公共动作的同步来对其组件之间的各种类型的协作进行建模，其组件的输出动作之间的同步不应被先验地排除，同步集合也不应被先验地固定。由于这两个特征允许定义上述对等和主从同步，它们被[18]作为引入TA来建模群件系统而不是使用IOA的主要原因TA与IOA的最后一个区别是TA不需要输入使能。这一特点也是从实践中激发出来的。无论对反应系统建模时输入启用多么方便，它确实阻碍了涉及人类的协作的现实建模-事实上，Tuttle在[49]中引入IOA时是第一个承认这一点的人-而对此类协作建模是[18]中引入TA的主要原因之一110M.H. ter Beek等.理论计算机科学电子笔记128（2005）1053访问控制策略任何（计算机）系统或环境安全的重要组成部分是 信息访问控制，但这有时是在一个相当特设或者是不适当的时尚，没有潜在的严格的，正式的模型。在典型的电子文件系统中，诸如读访问和写访问之类的访问权限是根据诸如所有权或访问者的特设在群件系统中，通常需要更精细的访问权限，例如滚动正在被同步编辑的文档的权限。一组实时。此外，在许多情况下，访问的粒度必须更细，更灵活，例如在软件开发团队中。 最后，重要的是控制Meta访问权限。 例如，作者可以向另一个团队成员授予对非团队成员的文件访问（即，代表团）。在[4]中，ter Beek等人基于Bullock等人的工作使用了空间访问隐喻。[9，10]-其中访问控制由主体和对象居住的房间或空间以及主体穿越空间以接近对象的能力来管理。虚拟现实被认为是用户可以通过使用键盘键、鼠标或更高级的设备从一个房间到另一个房间。这是一个自然和简单的扩展，假设访问控制检查发生在空间（房间）之间的边界（门），当用户试图从一个房间移动到另一个。 如果访问是OK，则用户可以进入并使用与新进入的房间相关联的资源。通过采用空间方法进行访问控制，可以利用环境的自然部分，从而可以通过环境的自然空间构成向最终用户隐藏明确的技术安全机制。然后，这些用户可以利用他们对环境的了解来理解隐含的安全策略。因此，用户可以避免理解访问控制矩阵等技术概念，这有助于避免误解。在安全文献中，身份验证处理用户是否真正是所代表的人的验证，而授权处理用户是否可以访问给定资源的验证。 在[4]中，只有授权考虑了我们的目标是将空间访问控制的隐喻与TA框架联系起来，并展示这种结合如何促进访问控制的一些关键问题的识别和明确描述。为了这个目的，它表明某些空间访问控制机制可以精确，并给出了一个正式的描述使用TA。首先介绍了通过授予和撤销访问权限来建立信息访问模型，显示了即时撤销与延迟撤销的对比（用户在被撤销时是否立即失去其访问权限-即使它当前处于活动状态M.H. ter Beek等.理论计算机科学电子笔记128（2005）105111使用该文件-或者当用户的权限已被撤销时，用户可以继续其当前活动，直到它想要重新启动该活动-此时进行授权检查以决定它是否有权重新启动该活动？）可以制定。随后，研究扩展到更复杂的Meta访问控制问题。这意味着诸如授予和撤销访问权限之类的特权本身可以被授予和撤销。Meta的概念显然扩展到任意层。在期刊评审过程中可以看到这样一个多层Meta结构的例子。 造物主文章的作者可以将发表责任委托给共同作者，共同作者可以选择期刊并授予主编阅读访问权限，主编可以授予助理编辑阅读访问权限，助理编辑可以授予和撤销审稿人的阅读访问权限。但是，撤销Meta权限是否也应该撤销传递给其他人的权限？ 在这里，人们触及的问题，浅与深撤销。浅撤销意味着撤销操作不会撤销先前传递的任何权限浅撤销通常是最容易建模的，而深度撤销由于可能出现的复杂（递归）情况而被认为是建模和实现的巨大挑战[13]。然而，在[4]中，演示了如何使用TA来明确和简洁地对浅层、深层甚至混合撤销进行建模。在[3]中，ter Beek和Bloem开始尝试使用模型检查器S引脚[32]来验证[4]中的一些TA规范。模型检查是一种自动技术，通过彻底检查其行为来验证系统设计是否满足其规范，即。考虑所有可能的输入组合和状态。设计是要给根据（有限）自动机和属性，应持有的是根据逻辑公式。模型检查算法然后检查特定模型是否满足特定属性。SPIN是一个最著名和最成功的模型检查器，在过去的二十年里，贝尔实验室[32]。在[3]中，TA规范[4]的翻译成PROMELA，这是S引脚的输入语言。因此，作者验证了这些TA规范是否确实对深度撤销进行了建模。事实证明，需要一个额外的公平概念，指定某些州为“非法”，即不允许TA在这些州停留超过一段有限的时间。 进一步研究 目前正在朝这个方向努力。112M.H. ter Beek等.理论计算机科学电子笔记128（2005）1054多播/广播通信协议多播/广播通信技术诞生的目的是相对于称为单播的标准点对点连接节省带宽和CPU时间。实际上，单个虚拟连接对数千个用户使用的带宽和资源并不比然而，多播和广播通信呈现实质性的差异。向一组接收器发送数据流的发送器可以将该流广播给所有连接的接收器（例如，TV广播）或仅将该流多播给指定的接收器（例如，按次付费TV）。多播和广 播 数 据 分 组 通 常 通 过 不 可 靠 的 传 输 协 议 （ 诸 如 用 户 数 据 协 议（UDP））发送。这可能导致分组丢失，即，该流被一部分接收者不完整地接收。在[6]中，本文的作者证明了TA非常适合于对可能发生数据包丢失的安全多播/广播通信进行建模，因为他们使用TA对高效多链流签名（EMSS）多播协议族的实例进行建模[46]。在这种情况下，TA的有用性是自然方式的结果，在这种自然方式中，典型的多播（广播）会话的一对多特别地，定义了多播组合算子Ctj，其使得能够将涉及一个发送者和n个接收者的多播协议建模为TA的组件之间的一对J回想一下，这样的操作符不能在IOA中定义。作为最后的考虑，我们观察到，另一方面，大多数CCS类进程代数中的基本通信机制是两个进程之间的成对同步（以输入/输出握手的形式）。这示出了为什么在[41]中，使用类似CCS的进程代数以利用完善的分析框架，成对同步的复制用于模拟多播/广播通信。此外，通过考虑非确定性地选择是否接收分组的接收器过程来对分组丢失进行建模。在TA框架中，也可以通过改变每个动作的一对多类型的同步以自然的方式对分组丢失进行建模。5一种分析证券属性的TA框架在[7]中，本文的作者定义了TA的不安全通信场景。它们的场景可用于分析M.H. ter Beek等.理论计算机科学电子笔记128（2005）105113不不不不{T T}断言不S公共发送/接收TIC公共发送/接收不R不断言P我不窃听注入TX涉及两个角色的密码通信协议，即，发起者TA_T_S和响应者TA_T_R。不是TS和TR之间的直接通信，而是假设所有通信都通过不安全的信道TATIC进行。这个不安全的通道可能会向入侵者TAX释放一些消息，而入侵者TA X又可以监听或修改（伪造）通过这个通道的消息。 当验证密码通信协议的安全属性时，确实很常见的是包括附加的入侵者（a`laDolev-Yao[15]）组件，其被认为是恶意的并且其目的是破坏协议的正确行为。因此，如果一个协议规范在存在入侵者的情况下仍满足安全属性，则该协议规范就安全属性而言被认为是安全的。从有关操作的密码学细节中抽象出来，根据这些操作，消息可以被加密、解密等，不安全的场景由图1中描绘的TA交互非正式地描述1.一、Fig. 1. TA的不安全通信场景P表示TA，表示在不存在的情况下的协议规范入侵者。因此，它通过隐藏通过不安全信道的所有公共发送/接收动作，然后在{TS，TR，TIC}之间强制最大同步来定义。TP被称为在隐藏所有公共发送/接收动作之后获得的{TS，TR，TIC}上的max-ai TA。P似乎作为一个黑盒，可能有一些输出动作（断言），表示成功接收到消息。通常，此类信号仅用于验证目的。I表示TA，代表协议规范，入侵者的存在。所谓的窃听和注入操作充当入侵的后门。 这正是保证入侵者可以仅通过不安全信道与TP通信。 所以TI被定义为P上的最大ai TA，X这是在隐藏了入侵者可以从其窃听并注入回不安全信道的所有动作之后获得的。以这种方式，最大的同步也被强制执行之间的入侵者和协议。这通过与入侵者组成安全通信场景来定义TA在文献中，已经进行了几项工作来防止多级计算机系统中的未经授权的信息流[8]，即：的系统114M.H. ter Beek等.理论计算机科学电子笔记128（2005）105一进程和对象被绑定到特定的安全级别。军事术语的一个例子是，文件通常从未分类到最高机密分级。[28]中提出的无干扰的开创性思想旨在确保信息只能从低水平流向高水平，而不是相反。这一概念在[43]中得到了完整的建模。就自动机而言，其（输入）动作集被分成低级和高级类。 这种形式化还满足了贝尔和拉帕杜拉的条件，即禁止所谓的另一方面，在类CCS进程代数的上下文中，非干扰类属性的第一个分类已在[20，21，22]中统一定义。特别是，代数中的进程根据它们可以执行的操作的级别被分为高级进程和低级进程。为了检测是否发生了不正确的信息流（即从高到低），定义了一种特定的非干扰性质，即所谓的非演绎成分（NDC）。NDC本质上说，如果一个过程孤立地表现出低行为，与任何高级进程交互时的低级行为相同。NDC可以从多级系统的世界转化为网络安全的世界。另见[24，26]，其中低级过程成为加密通信协议的规范，并且将孤立运行的协议的行为与与任何可能的对手并行运行的协议的行为进行比较。作为进一步的步骤，在[26]中已经制定了广义NDC（GNDC） 非正式地说，一个规范P满足GNDCα（P）当且仅当P，尽管事实上，它运行在一个敌对的环境中，似乎与α（P）不可区分（关于外部观察的概念a）。这个α（P）表示P的正确行为。通过改变α（P），可以在这个广义模式中定义和分析几个安全属性。2为了嵌入TA在刚刚描述的成熟的分析框架中，本文的作者在[7]中根据TA制定了GNDC模式基于GNDC模式的TA，上述不安全场景的组合分析策略进行了描述。此策略可用于验证由场景建模的通信协议中的安全属性。事实上，在[7]中，根据TA的GNDC模式，以及TA的不安全通信场景，用于表明EMSS协议的确定性（1，2）模式中的完整性得到了保证。虽然这已经在[41]中得到了验证，其中类似CCS的进程代数是[2]最近定义了一个稍微扩展的GNDC模式[25]，其中包含了P的不良行为集可能取决于P本身和所审查的属性这一事实M.H. ter Beek等.理论计算机科学电子笔记128（2005）105115这个特殊的案例研究确实显示了TA在分析证券属性方面的有效性。请注意，该案例研究还表明，第4节和第5节中描述的方法可以结合起来，以便提供一种组合分析策略，用于验证具有多播/广播通信的密码协议中的安全属性。有人可能会评论说，[7]测试了一种基于协议的理论方法，其中要验证的安全属性已经知道是有保证的。然而，这个案例研究已经调查测试的方法。然而，TA的使用不仅限于证明完整性，还可以验证其他安全属性，如保密性和实体身份验证6结论和今后的工作在本文中，我们提出了一个调查的使用TA的规格并对安全领域的一些问题进行了分析更确切地说，我们已经展示了TA如何能够充分用于建模和验证访问控制策略，多播/广播通信协议和（加密）通信协议。在许多方面，本文伴随着[33]，在那里提出了一个调查使用TA的CSCW。越来越多的论文证明了TA在分布式和反应式系统的早期设计阶段的有用性。这些例子并不局限于CSCW [5，17，18，36]和安全[3，4，6，7，16]等领域，而是扩展到软件工程[19，30，31]等领域事实上，从硬件组件到用于交互人群的协议的范围现在已经由TA建模。TA框架通过明确动作的作用和控制通信、协调、合作和协作的转换的选择来支持反应式和分布式系统和协议的设计。此外，模块化设计的形式设置和可能性为验证复杂计算机系统的期望特性提供了分析工具模型检查技术，如[3]中所采用的技术，因此可以用于验证所得到的系统。未来的一个目标是尝试自动化TA框架中由于TA是IOA的扩展，IOA语言和工具集[27]可能有助于实现这一目标。该框架为定义IOA以及验证其属性（通过定理证明，模型检查和仿真）提供了工具支持。未来的另一个目标是用时间、概率或两者来扩展TA框架。 这种基于自动机的形式主义的扩展已经在文献中得到了很好的研究，例如。 [39]第48话。在这方面，也需要提到发展良好的时间自动机理论[1，35].喜欢他们的116M.H. ter Beek等.理论计算机科学电子笔记128（2005）105IOA对应物，定时TA可以考虑它们建模的系统中的时间流逝，而概率TA可以允许下一个状态的概率选择这两种方法都被广泛地用于描述各种基于时间的算法和概率密码协议，并证明它们的性质。鉴于这些现有的自动机理论的结果，TA的时间和概率的扩展预计是一个可行的。7确认Ter Beek和Lenzini得到了MIUR“战略研究发展特别基金”的支持，该基金此外，Lenzini还得到了“PAW ：环境中的隐私”的部分支持，这IGC03001。Petrocchi得到了MIUR项目的支持：“Strumenti ， Ambienti e Appli-cazioni Inn o v ati v e p er la S o cie t a ` dell'Informazione” ，sottoprogettoSP1：RetiINTERNET：“einstancienza，integrazione e sicurezza”。最后，我们感谢三位匿名推荐人的建议，这些建议帮助我们改进了论文的介绍引用[1] 巴尔河，D. L。Dill，时间自动机理论，理论计算机科学126（1994），183[2] 特尔·贝克，M.H.，“Team Automata-A Formal Approach to the Modeling of CollaborationBetween 论文，莱顿大学高级计算机科学研究所，2003年。[3] 特尔·贝克，M.H.，Bloem，Model Checking Team Automata for Access Control，未出版的手稿，2003年。[4] 特尔·贝克，M.H.，C.A. Ellis，J. Kleijn，and G. Rozenberg，Team Automata for Spatial AccessControl，Proc.ECSCW[5] 特尔·贝克，M.H.，C.A. Ellis，J. Kleijn，and G.团队自动机中的同步对于群件系统，参见ComputerSupportedCooperativeWork-TheJournalofCollaborativeComputing 12，1（2003），21-69。[6] 特尔·贝克，M.H.，G. Lenzini和M. Petrocchi，多播/广播通信安全分析的团队自动机，技术。Rep.2003-TR-13 ， Istituto di Scienza e Tecnologie dell'Informazione ， Consiglio Nazionale delleRicerche，2003.在WISP[7] 特尔·贝克，M.H.，G. Lenzini和M. Petrocchi ，Team Automata for Security Analysis，Tech。众议员TR-CTIT-04-13，大学电信和信息技术中心M.H. ter Beek等.理论计算机科学电子笔记128（2005）105117Twente，2004年。在DIMACS协议安全分析研讨会上发表，2004年（无正式会议记录）。[8] 贝尔，D.E.，和L.J. La Padula，Secure Computer Systems-Uni Fied Exposition and MulticsInterpretation，Tech.众议员ESD-TR-75-306，MITRE MTR-2997，1976年。[9] Bullock，A.，和S.陈文辉，虚拟环境中的访问控制，[10] Bullock，A.，和S. Benford，多用户协作环境的访问控制框架，Proc.GROUP[11]陈洪，和D. Wagner，MOPS：用于检查软件安全属性的基础设施。CCS[12] 陈洪，D. Wagner和D. Dean，Setuid Demystified，Proc. Security'02，USENIX，2002，171-190。[13] Dewan，P.，和H.沈，灵活的Meta协作应用程序的控制，Proc. CSCW[14] Die ， W. ， 和 M. Hellman ， New Directions in Cryptography ， IEEE Transactions onInformation Theory22，6（1976），644[15] Dolev，D.，和A. Yao，关于公钥协议的安全性，IEEE Transactions on Information Theory2，29（1983），198[16] 埃吉迪湖和M. Petrocchi，Modeling a Secure Agent with Team Automata，Tech。Rep. TR-INF-2004-07-08-UNIPMN，DipartimentodiInformatica，Universita`degliStudidelPiemonteOrientaleAmedeo Avogadro，July 2004.[17] 埃利斯，CA，K.- H.王文，“协同系统的[18] 埃利斯，CA，群件系统的团队自动机，1997年集团会议，ACM出版社，415-424。[19] Engels ， G. ， 和 L.P.J. Groenewegen ， Towards Team-Automata-Driven Object-OrientedCollaborative Work，Formal and Natural Computing，LNCS2300，Springer，2002，257[20] 福卡尔迪河，和R. Gorrieri，A Classi fication of Security Properties for Process Algebras，Journal of Computer Security3，1（1994），5[21] 福卡尔迪河，和R. Gorrieri，The Compositional Security Bioker-a Tool for the Verification ofInformation Flow Security Properties ， IEEE Transactions on Software Engineering23 ， 9（1997），550[22] 福卡尔迪河，和R.Gorrieri，安全属性的分类-第二部分：信息流，Proc.FOSAD 2001- 2010讲座，LNCS2171，Springer，2001，331[23] 福卡尔迪河，R. Gorrieri和F. Martinelli，Non Interference for the Analysis of CryptographicProtocols，Proc.ICALP[24] 福 卡 尔 迪 河 ， R. Gorrieri 和 F. Martinelli ， Secretariat in Security Protocols as NonInterference，ENTCS32，2000。[25] 福卡尔迪河，R. Gorrieri和F. Martinelli，安全属性分类-第二部分：网络安全，Proc. FOSAD2001/2002，LNCS2946，Springer，2004，139-185。[26] 福卡尔迪河，和F. Martinelli，A Uniform Approach for the Definition of Security Properties，Proc. FM[27] 加兰，S.J.，和N.A. Lynch，IOA语言和工具集-支持设计，分析和构建分布式系统，技术。Rep.MIT/LCS/TR-762，MIT，1998.118M.H. ter Beek等.理论计算机科学电子笔记128（2005）105[28] Goguen，J.A.，和J. Meseguer，Security Policy and Security Models，Proc. SP[29] Gürgens，S.， P. O chsens chlager和C. 鲁道夫，使用异步乘积自动机的密码协议的RoleBasedSpefication和安全性分析，Proc. DEXA[30] 特霍恩，PJ “Towards Distributed Development of Large Object-Oriented Models-Views论文，莱顿大学莱顿高级计算机科学研究所，2001年。[31] ’t 和M.H.张文，基于团队模型开发的无冲突策略，中国科学院学报，2000年，第720-725页[32] Holzmann，G.J.，[33] Kleijn，J.，陈晓，陈晓明，陈晓明，等[34] Kurshan ， R.P. ， “Computer-Aided Verification of Coordinating Processes-The Automata-Press，1994.[35] 拉诺特河，A. Maggiolo-Schettini，和A.张文，概率时间自动机的弱互模拟及其在安全中的应用，2003年第3期[36] Lavana，H.，“A Universally Configurable Architecture for Taskflow-Oriented Design of a毕业论文，北卡罗来纳州立大学电子与计算机工程系，2000年。[37] Lowe，G.，使用FDR打破和修复Needham-Schroeder公钥协议，Proc. TACAS[38] 林奇，N.A.，I/O Automaton Models and Proofs for Shared-Key Communication Systems（共享密钥通信系统的I/O自动机模型和证明）CSFW[39] 林奇，N.A.，输入/输出自动机：基本，定时，混合，概率，动态，... ，Proc. CONCUR[40] 林奇，N.A.，和M.R. Tuttle，An Introduction to Input/Output Automata，CWI Quarterly2，3（1989），219Tech. 备忘录MIT/LCS/TM-373，1988年。[41] Martinelli，F.，M. Petrocchi和A. Vaccarelli，安全流式数据的组成验证：EMSS案例研究，Proc.ICTCS[42] Nipkow，T.，L.C. Paulson和M.王文，有关最新说明，请参阅http://isabelle.in.tum.de/。[43] 莫斯科维茨，I.S.和O.L. Costich，A Classical Automata Approach to Noninterference TypeProblems，Proc.CSFW[44] von Oheimb，D.，交互状态机-一种有状态的安全证明方法。FASec[45] von Oheimb，D.，和V.Lotz，Formal Security Analysis with Interacting State Machines，Proc.ESORICS[46] Perrig，A.，R. Canetti，J.D. Tygar和D.X.宋，多播流在有损信道上的有效认证和签名，Proc. SP[47] 联邦调查局施耐德可强制执行的安全策略，ACM信息和系统安全事务3，1（2000），30[48] 塞加拉 R.， 一 组成 基于跟踪 语义 为概率自动机，Proc. CONCURM.H. ter Beek等.理论计算机科学电子笔记128（2005）105119[49] 塔特尔，M.R.，“分布式算法的层次正确性证明”，硕士论文，系。电气工程和计算机科学，麻省理工学院，1987年。Tech.报告MIT/LCS/TR- 387，1987年。[50] TA网页：http://fmt.isti.cnr.it/mtbeek/TA.html。TA参考书目：http://liinwww.ira.uka.de/bibliography/Theory/TA.html。