串空间模型的分支束理论与事件结构的关系

理论计算机科学电子笔记242（2009）139-159www.elsevier.com/locate/entcs向链空间模型SibylleFroéschle1DepartmentfurInforormatikUniversitaétOldenburgOldenburg，Germany摘要串空间模型是分析安全协议最成功和最广泛使用的形式化模型之一。考虑到模型不能反映协议执行中的选择点，这可能看起来令人惊讶：串空间模型中的关键概念是束，它精确地模拟了安全协议的一种可能执行。受Petri网分支过程的启发，我们证明了分支可以以一种非常自然的方式引入到串空间模型中：束可以被推广到分支束，它能够捕获多个冲突协议执行。 我们的分支束理论的调查将激发的概念，符号分支束，并最终的结果，每个协议有一个最大的符号分支束方面的串空间语义。我们希望我们的研究结果提供了一个强大的理论基础，比较模型和提供安全协议分析中的进程演算语义。总的来说，我们的工作与Crazzolara和Winskel的一系列作品有关，但不同。在整个过程中，我们将从串空间模型与事件结构的密切关系中获益，这一点已经由这些作者指出。关键词：安全协议分析模型，串空间，事件结构，分支过程1介绍串空间模型[6]是分析安全协议的最成功和最广泛使用的形式主义之一例如，它已被用于手工验证安全属性，为协议逻辑提供形式化语义，并作为模型检查工具的基础模型（c.f.[8]）。尽管这一成功的两点批评已经带来了反对它：一个是，在对比模型的基础上多集重写，它是一个特设的模型，而不是植根于丰富的理论。第二个是它不能反映分支的各个方面，例如协议执行中的选择点。为了解释后者，我们回想一下，串空间模型的中心概念是丛。一个bundle只对协议执行的一个快照进行建模：一组链表示到目前为止已经发生的会话，而链的发送和接收事件之间的关系描述了消息如何在它们之间传播1 电子邮件地址：froeschle@informatik.uni-oldenburg.de1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.06.017140S. Fröschle/Electronic Notes in Theoretical Computer Science 242（2009）139Crazzolara和Winksel的结果反驳了这两点批评[2，1，3]。一方面，他们已经表明串空间模型与基于事件的并发模型（如事件结构）密切另一方面，为了获得协议语言的基于组合事件的语义，他们已经展示了串空间模型如何通过constricht的概念进行扩展[3]。他们在串空间的层次上引入了冲突的概念，串空间在概念上比bundle低一个层次：串空间固定了协议分析中要考虑的所有会话;它是bundle被“分割”出来的空间在本文中，我们的论文是，分支可以引入到串空间模型非常直接的概念层次的丛。其思想是以与Petri网理论中分支过程一般化Petri网过程相同的方式将束一般化为分支束。Petri网分支过程[5]被引入作为Petri网运行的初始部分的形式化，其可以包括冲突选择。它们有一个非常令人满意的理论：Petri网的分支过程形成了一个关于自然近似概念的完整格（模同构）这个格的最大元素捕获了Petri网的所有可能行为，称为其展开。在本文中，我们希望调查是否协议满足理论的分支束。如果每个协议P确实有一个最大的分支束，这个分支束将捕获P的所有可能的行为，并因此提供一个自然的串空间语义。这为比较模型和为协议语言提供语义提供了强有力的理论基础。我们的贡献如下：(1) 我们表明，丛确实可以推广到分支丛在一个非常自然的方式。分支束能够捕获多个冲突协议执行。(2) 我们研究分支丛理论我们发现每个分支丛都可以看作是一个标号素事件结构。这将激发一个概念的计算状态的分支束的子束，它们之间的过渡关系。按照[5]的方法，我们将研究一个协议的分支丛是否形成一个关于自然近似概念的完备格然而，我们将得到一个否定的结果：一个协议的分支丛甚至不能形成一个完全的偏序。(3) 然而，通过分析这个否定的结果，我们将得到符号分支丛的概念我们将得到，一个协议的符号分支丛确实形成一个完整的格（模同构）。因此，每一个协议可以被赋予一个最大的符号分支束方面的串空间语义。我们将激励，这种语义是适合于大多数情况下的安全协议分析。在下面的部分中，我们将介绍链空间模型，使用[2]和[7]原始定义的变体。本文的其余部分是根据上述贡献的结构。简单明了的证明已移至附录A。S. Fröschle/Electronic Notes in Theoretical Computer Science 242（2009）1391412串空间模型图形术语一个标记（有向）图是一个元组（E，K，L，l），其中E是节点的集合，在我们的上下文中将描述事件，KE×E是边的集合，L是标签的集合，l：E→L是一个标签函数，它为每个节点分配一个标签。当L在上下文中是明确的时，我们通常为了符号的简单性而保持它的隐式一个标号图（E，K，L，l）是全序的，如果存在一个全序e1e2. 的元素，使得（ei，ej）∈K当且仅当j=i+1。一个标号图（E，K，L，l）是一棵标号树，如果K是无圈的，并且没有向后分支，即，如果（EJ，e）∈K且（EJJ，e）∈K，则EJ=EJJ。树的分支是一个可能为空的、有限的或无限的序列e1e2. 的元素，使得（ei，ei+1）∈K的所有指标i。一个标号双图是一个元组（E，n，→，L，l）使得（E，n，L，l）和（E，→，L，l）都是标号图。消息代数在下文中，我们假设消息由消息代数建模。我们在这里提出的结果是独立于这个代数的实际结构。我们只假设一组消息Mesg，一组原子消息AMesg，Mesg是由Mesg上的一个二元关系±构建的，该关系表示当一条消息包含在另一个。消息和原子消息可以包含变量。如果消息不包含任何变量，则消息是接地的。我们用GMesg表示地面消息的集合。操作、角色和协议在协议执行中，主体可以发送或接收消息。如果发送了一条消息，那么它可以包含刚刚生成的数据，比如随机数。这就产生了以下一系列行动：Act ={+ M中的新鲜N|M∈Mesg&N <$AMesg <&$N∈ N，N±M}{− M|M ∈ Mesg}。在形式为“+ fresh N in M”的动作中我们假设只有原子消息可以新鲜生成。在形式为“-M”的动作中给定一个动作A∈Act的两种形式中的任何一种，我们分别用mesg（A）来描述M，sign（A）来描述“+”或“-”。如果sign（A）= +，我们将进一步使用fresh（A）来描述N。地面动作是不包含任何变量的动作。我们用GAct表示地面作用的集合。在具有标号集GAct我们将以明显的方式将前面的动作概念延续到图中的事件。轨迹是地面作用的有限序列142S. Fröschle/Electronic Notes in Theoretical Computer Science 242（2009）139角色定义了主体在协议会话中可以执行的操作形式上，角色是一个有限的动作序列，R = A1. 这样，R1对于所有i∈[1，n]，对于所有N∈fresh（Ai）(a) N是变量，并且(b) Ai是初始条件，其包含N：Nj0。那么显然深度（eJ）>0。此外，我们有cod（cod）-pred （e））=cod（→-pred（eJ））和cod（→-pred（eJ）