具有时间约束的协议的规范和验证

理论计算机科学电子笔记99（2004）205-227www.elsevier.com/locate/entcs具有时间约束的协议的规范和验证1玛格丽特那不勒斯<$米莫帕伦特<$阿德里亚诺庇隆†Dipartimento di Informatica e Applicationazioni，Universtit`adegliStudidiSalerno，I-84041Baronissi（Salerno）.Dipartimento di Scienze Fisiche，Universit`a diNapoliFedericoII，Vi a Cintia，I-8012 6 Napoli.摘要在本文中，我们面临的问题，指定和验证安全协议的时间方面明确出现在描述中。对于这些类型的协议，我们设计了一个规范化的形式主义，它包括一个状态转换图的每个参与者的协议，与触发器/动作子句标记的边缘。协议的规范被转换成一个时间自动机，在这个时间自动机上可以利用模型检查的标准技术（要检查的属性可以用线性/分支非定时/定时时序逻辑来表达）。在所有的演示中，我们使用一个两方不可否认协议作为运行示例，我们展示了我们的框架如何应用于验证协议的公平性（确定是否存在协议的一个步骤，其中两个参与者中的一个可以利用另一个）。保留字：规范，模型检查，时间自动机，不可否认协议1介绍从90年代初开始，形式化方法就被广泛应用于密码协议设计的各个阶段（规范化、构造和验证），因为许多例子表明，它们的非正式设计是容易出错许多作品都致力于形式化的规范化1本工作是由MURST在其出版物“MetodiForormaliperer laSicurezzaedilTempo“（ME FISTO）的第一篇文章中提出的。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.009206M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-和密码协议的分析，导致了许多不同的方法和令人鼓舞的结果（例如，见[8]）。然而，大多数提出的技术考虑密码协议，其中关于事件的定时的具体信息在本文中，我们专注于指定和验证安全协议的问题，其中时间方面明确出现在规范中，并在验证中考虑。 我们使用的正式的基本符号是， 时间自动机[2]的验证方法是模型检验。近年来，人们提出了各种各样的工具来验证用时间自动机描述的实时系统。例如，VERIMAG开发的工具KRONOS [4]支持分支时间需求的模型检查。UPPAAL工具箱[7]允许检查安全性和有界活性属性。不幸的是，时间自动机的形式主义是一种相当低级的形式主义，不适合表达安全协议的高级规范，并且协议设计者很难将其用作规范语言。时间自动机缺乏显式表示并行性和并行组件之间通信的能力（协议的每个参与者自然被描述为与其他组件/参与者并行操作的规范的组件）。此外，安全协议的规范通常需要描述参与者交换的结构化消息，这些消息可能通过使用加密原语（加密，散列，签名等）组成。在本文中，我们提出了一种称为消息传递时间自动机（MTA，简称）的规范形式主义，它保留了时间自动机的图形性质（状态转换图），并允许以非常接近协议设计者习惯使用的方式来规范密码协议。特别地，MTA允许协议各方的显式表示和各方之间的通信。各方通过发送/接收属于术语代数的结构化消息来进行通信，该术语代数适合于表达密码原语和概念（例如，公钥/私钥、加密/解密、散列、随机数等）。 关于时间方面，三种时间约束可以在形式主义中不同地表达：控制流的时间约束（例如，与执行某些动作相关联的通常延迟和超时）、对（传送的）信息段的可用性和可用性的时间约束（即，消息的公开和期满）以及信道传送的持续时间。M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-207与时间自动机更基本的形式主义的联系并没有丢失。事实上，规范语言的语义是根据时间自动机给出的，因此获得了一个可执行和可验证的（在模型检查的标准框架中）规范。通过编译协议规范获得的时间自动机在其状态中编码了证明协议相关属性所需的所有详细信息（包括时间方面）使用时间自动机来指定实时系统和证明安全属性的想法并不新鲜（例如，参见[3，6]）。我们在时间自动机中的方法区分符不是特定语言本身，而是专门用于安全协议的新特定语言的前端。从这个角度来看，我们的工作更接近于[5]，其中指定语言是一个时间进程代数。这两种方法在处理时间（离散与连续）和验证技术方面存在差异。为了支持我们的形式主义，我们提供了一个非常著名的不可否认协议的应用程序，参见[9]。在这个协议中，爱丽丝向鲍勃发送一条消息，最后他们中的任何一个都不能声称没有发送或接收过这条消息。更准确地说，在协议的最后，鲍勃已经收集了足够的信息来证明爱丽丝是消息的来源，爱丽丝也有足够的信息来证明鲍勃确实收到了她的消息。没有人能否认这一点，因为其他人会提供相反的证据。基于这个协议，我们模型检查以下公平性：没有步骤，如果协议将停止，双方中的一方有一个本文的其余部分组织如下：在下一节中，我们重新调用Zhou和Gollmann[9]的不可否认协议。在第3.1节中，我们给出了规范语言以及示例协议的最终MTA，在第4节中，我们展示了到Timed Au- tomata的转换。最后，我们在第5节中对示例协议的公平性进行了验证，并在最后一节中得出了一些结论2Zhou-Gollmann高效的不可否认协议在本节中，我们简要回顾了[9]的Zhou-Gollmann协议。 给定两方，Alice和Bob，不可否认协议旨在向双方提供消息发送和接收的证据更准确地说，当协议运行以将消息从Alice传递到Bob终止时，以下属性被填充：208M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-• 与Alice交互的源不可否认（NRO）Bob收集足够的信息以提供消息的源的证据，并且如果Alice否认发送了消息，则可以使用这样的证据作为证明• 接收不可否认性（NRR）Alice与Bob交互，收集足够的信息以提供消息接收的证据，并且如果Bob否认收到它，则可以使用这样的证据作为证据。为了有效地实现不可否认性，作者考虑了协议中的另一方，即可信第三方，只有当一方无法获得预期的不可否认性证据时才进行干预，为受损方提供所需的证据。公平财产。 该协议满足公平性：它提供了发送方和接收方在协议完成后提供有效的不可辩驳的证据，在协议的任何由于发送的证据是由电文本身（或随电文一起发送的其他东西）提供的，因此发端人需要收到电文的确认。公平性被破坏的原因有两个：要么是通信信道有故障，传输的消息永远不会被传递，要么是一方不遵守协议规则，不公平我们假设通道是弹性的，也就是说，它永远不会出错，并且总是在有限的未知时间内传递消息通过解释[9]，该协议的主要思想是将消息分为两部分，一个承诺和一个密钥K，它被发送到B和TTP。 如果发生争议，双方都有能力收回 从TTP键。让我们首先给出一些必要的符号来描述协议：M是从A发送到B的消息，T是超时，K是A的密钥，C是承诺（即，M密码子与K），L是由A选择的用于标识协议运行的唯一标签，f是指示协议运行的目的的标签。消息，SA和SB是A此外，协议的规范利用了以下速记：EOO=sSA（fEOO，B，L，T，C）EOR=sSB（fEOR，A，L，T，C）EOOK=sSA（fEOOK，B，L，K）EORK=sSB（fEORK，A，L，K）subK=sSA（fE O R，B，L，K）M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-209con K= sSTTP（fCON，A，B，L，K）现具体说明如下：(i) A → B：f EOO，B，L，T，C，EOO(ii) B→A：fEOR，A，L，EOR(iii) A→B：fEOOK，B，L，K，EOO K(iv) B→A：fEORK，A，L，EOR K如果B没有接收到密钥K，则在步骤3，协议停止满足公平属性。另一方面，如果A没有接收到步骤4的消息，则她开始以下恢复阶段：344证据 如果协议合法停止，则A和B得到不可否认证据（A的EOR和EOR K，B的EOO和EOO K）。否则，如果出现问题，A将启动恢复阶段，并在TTP的帮助下获得证据（A为EOO和con K，B为EOR和con K）。让我们注意到，需要参数L来指定一个协议运行（它是由Alice在开始时与T一起选择的）。关于该方案的更详细介绍，读者可参考[9]。3质量标准在本节中，我们首先介绍消息传递时间自动机的形式主义，给出其直观的语义（形式语义在第4节中给出），然后我们在定义的设置中指定Zhou-Gollman不可否认协议。3.1消息传递时间自动机我们首先定义代数，允许将参与者之间通信中使用的结构化消息代数具有对应于最广泛使用的密码原语的操作（例如加密、解密、散列、签名等）。以及用于将时间约束与消息相关联的操作（例如，定时公开、期满等）。设M、K、PK、I和N分别是消息、密钥、公钥、身份和随机数的成对不相交字母表，并且设K =K <$PK<$M <$I<$N。210M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-τ1τ1τ1定义3.1设X是形式参数的字母表。在X和X上的结构化消息的集合，由SM_X，X表示，归纳定义如下：• m∈SMX;• ！X∈SM，X，对任意X∈ X;• （m，MJ）∈SM<$，X，对任意m，MJ∈SM<$，X;• {m}K∈SM<$，X，对任意m∈SM<$，X和K∈ K <$PK;• h（m），f（m），signid（m）∈SM<$，X，对任意m∈SM<$，X和id∈ I;• 对任意m∈φ，τ，τ1，τ2∈ Q≥0，0<τ1≤τ 2。如果m中出现的任何形式参数符号在a的范围内，则结构化消息m是基础的！符号.地面消息的集合将被表示为dySMm，m。 消息在时间上被定义为形式为πτ（m）、Θτ（m）或π2（m）的（子）消息的并发在上述定义中！X可以被解释为与形式参数X相关联的基础消息（如果有的话），{m}K作为使用私钥或公钥K对消息m的加密;h（m）作为消息m的散列;signid（m）作为使用身份id对消息m的签名。消息m和mJ的（m，mJ）配对允许构造结构化消息。 作为关于定时消息，我们有以下内容：m仅在自m的通信起经过时间间隔τ时才被公开，Θτ（m）表示m在时间间隔τ（自m的通信起）之后到期，并且Iτ2（m）表示m在τ1之后被公开并且在τ2之后到期的事实;t（m）表示m到期的事实请注意，时间约束只能与非结构化消息（即，XML中的消息）相关联协议执行中的每个参与者通过接收其他参与者发送的结构化消息来收集证据。在下文中，对于和身份id，我们定义了一个描述证据集（即，身份id的参与者已知或可组合的消息）的关系ID，该证据集可以从结构化消息的集合中导出（或组合）对于一个恒等符号id∈I，证据推导关系id2SM，X×SM，X由以下规则递归定义（为简单起见，我们使用fix表示法）：• 如果m∈Kw，则Kw≠m;• 如果K∈ PK，则Kw=K;• Kw_id_h（m）如果Kw_id_m;M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-211• Kw_id_sign_id（m），如果Kw_id_m;• Kw_id_m，如果Kw_id_sign_id_J（m）;• Kw_id（m1，m2）如果Kw_idm1和Kw_idm2;• 如果Kw_id（m1，m2），则Kw_id_m1和Kw_id_m2• 如果Kw_id_m和Kw_id_K，则Kw_id_{m}K;• Kw_id_m，如果Kw_id_{m}K和Kw_id_K;• Kw_id_m如果Kw_id_Θτ（m）;• 如果Kw_id<$（m），则Kw_idm注意，任何公钥都是已知的;消息可以被散列和签名（使用身份ID）;可以耦合一对消息，并且可以提取一对的组成消息;如果加密密钥是已知的，则可以解密加密的消息，并且可以通过已知的密钥来加密消息;具有到期时间的消息是已知的，而具有（非空释放时间）的消息不是已知的。协议的参与者由状态转换图来描述，其中转换由表示沿信道发送和接收结构化消息的事件来标记，分别称为触发器和动作更正式地，给定通道的集合Γ，在Γ上的触发器的集合，写为触发器Γ，是集合{True}{？α（m）：其中α∈ Γ，且m∈ SM<$，X}.在Γ上的作用的集合，写作ActionΓ，是集合：{Nil}{！α（m）：其中α∈ Γ，且m∈ SM<$，X}.定义3.2一个消息传递时间自动机，简称MTA，在一个字母表上，一组参数X和一组通道Γ上，是一个元组C1，...，Cn，λ，η，其中• λ：Γ→Q≥0×（Q≥0<${ω}）是定时信道函数;• η：{1，. ，n} → I是单位（内射）函数;• 任何序列分量Ci，其中1≤i≤n，是元组Si，Ii，δi，Kwi，其中· Si是状态的（有限）集合（我们假设Si<$Sj=，对于i/=j）;· Ii<$Si是输入状态的集合;·δi<$Si×TriggerΓ×ActionΓ×S×Sθ×Si是转换关系，我我其中，对于一组状态S，Sθ是集合{（s，τ）：s∈S，τ∈ Q≥0}，并且SΘ212M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-是集合{（s，τ）：s∈S，τ∈ Q≥0<${ω}};· Kwi：Ii→2是初始证据函数。在上面的定义中，定时信道函数给出了信道α的区间端点，该区间界定了传递消息所需的时间。例如，如果λ（α）=（2， 5），则α是一个至少需要时间2来传递消息的操作信道，并且已知其在时间5内传递消息;如果λ（α）=（0，ω），则α是一个弹性信道，其在有限但不可预测的时间内传递消息单位函数是一个单射函数，用单位符号命名每个连续的成分。MTA的每个顺序组件是描述协议中的参与者的状态转换图。它由一组有限的状态组成，其中的一个子集是输入状态（即协议执行的初始状态）。初始证据函数Kwi为每个初始状态分配一组证据（即私钥、身份、随机数、非结构化消息），这些证据应该在协议执行开始时被参与者知道。参与者对协议部分已知的实际证据集可以通过接收来自其他参与者的消息来增强（从其初始状态），并且每次达到输入状态时将其重置为初始条件。从状态s1到s2的任何转换都是以下形式trigger，action，delay，timeout，s2超时，标签为• 一个触发事件：如果触发器是一个表达式的形式？α（m），当它沿着通道α接收到消息时，转换被使能以触发;如果触发等于True，则转换无条件地被使能以触发;• 一个动作，它是在过渡触发时采取的：如果这个动作是形式的一种表达！α（m），在信道α中发送消息m;如果动作等于Nil，则不执行动作;• 具有形式（s，τ）的延迟，其中s∈Si，这意味着在最后进入状态s之后仅可以执行转换的时间量τ;• 具有（s，τ）形式的超时，其中s∈Si，意味着转换只能在最后进入状态s之后的时间量τ内执行。请注意，转换的性能取决于两种约束的实现：通信事件的触发，以及延迟和/或超时所施加的时间约束。顺序组件通过同步发送和接收进行通信M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-213亩亩亩亩亩亩亩亩亩通过通道发送消息（一对一握手）。不允许异步通信还必须保持预期信息的结构。消息m发生在接收事件中？α（m）是一个结构化的消息，通常包含形式参数。相反，一个信息mJ发送的一个行动！α（mJ）是地面信息。同步化？α（m）与！α（mJ）只有当m和mJ具有相容结构时才能发生，即它们是唯一的。例如，形式为（X，SignA（X））的消息m，其中X是参数符号，与形式为（m，SignA（m））的消息是可统一的，并且它不是可与形式为（m1，SignA（m2））的消息统一，其中m1m2。 在在前一种情况下，同步的副作用是将实际值m绑定到形式参数X。所概述的项的统一性和将实际值分配给形式参数的概念，通过如下定义的消息统一关系来形式化对于k∈TK和函数ρ：X→SM， ρ，则消息un如果icat ionrel at i on=T ，ρSM，X×SM，×SM，X×2X ×SM，ρasocies，具有一对消息m1和m2（其中m2为基），一对由统一消息mu和从参数到（基）的部分函数σu消息（为了可读性，我们将写为（m1，m2）=T，ρ（mu，σu）（m1，m2，mu，σu）∈=<$T，ρ. 关系式=T，ρ 归纳定义为木木如下所示：• （m1，m2）=ΔT，ρ（m2，n）如果m1是地且m1=m2;• （X，m2）=ΔT，ρ• （！X，m2）= ΔT，ρ（m2，{（X，m2）}），其中X∈ X;（m2，<$），若ρ（X）=m2;• （{m1}K，{m2}K）=<$T，ρ（{mu}K，σu），若K∈T<$PK，且（m1，m2）=<$T，ρ（mu，σu）;• （Signid（m1），Signid（m2））= πT，ρ（Signid（mu），σu）若（m1，m2）=<$T，ρ（mu，σu）;• （（m1，m2），（m3，m4））=<$T，ρ（（MJ，MJJ），σJ<$σJJ）如果（m1，m3）=<$T，ρ（MJ，σJ），MUu u u uMUu u（m2，m4）=<$T，ρ（MJJ，σJJ）且σJ<$σJJ是偏函数.MU U U U U统一关系中的参数T是当消息被统一时应该知道的私钥的集合例如，只有当K是公钥或K是已知私钥时，消息{X}K才能与消息{m}K（请注意，此限制防止通过统一公开加密消息由于同样的原因，消息h（X）不能与消息h（m）统一。一对消息的统一条件确保了两个不同的实际值是214M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-不分配给相同的形参。通常，执行转换不是瞬时的。一个由触发器标记的跃迁t1α（m）和一个动作！β（mJ）可以在与由动作！α（mJJ）是可能的。同步是即时的，并立即释放t2.另一方面，完成启用过渡t1，可能会推迟两个因素，这有助于总的持续时间 过渡：(i)t1可能被迫等待消息mJJ，其花费属于区间λ（α）的时间;(ii) 动作需要同步β（mJ）。这样一种转换语义的结果，是一个由触发器标记的转换吗？α（m）和一个动作！β（MJ）可以等价地用两个跃迁的序列化来代替，前者用？α（m）带有Nil操作，后者由触发器True和action标记！β（mJ）。 为了简单起见，在下文中，我们将考虑顺序组件。具有以这种受限方式标记的过渡。更正式地说，如果转换具有以下形式之一，则它是单向的：• 对于某个γ∈Trigger（Γ）（一个接收跃迁），有εs，γ，Nil，（s1，τ1），（s2，τ2），SJε• s，True，β，（s，0），（s，ω），sj将MTA转换成具有单向传输的MTA是容易的选择。给定一个时序分量C= S，I，δ，Kw，我们用U nidir（C）表示时序机（具有单向转换）S0<$S1，I0，δ，Kw，其中•Si={（s，i）：s∈S，其中i∈ {0， 1}}是S的两个不相交的副本;• I0={（s，0）：s∈I};δ={δ（s，0），γ，Nil，（（s1，0），τJ），（（s2，0），τJ），（s，1）}，•（s，1），True，β，（（s，1），0），（（s，1），ω），（sJ，0）<$s，γ，β，（s1，τJ），（s2，τJJ），sj<$∈δ};• Kw={（（s，0），A））：（s，A）∈Kw}.对于MTA C=100C1，.，Cn，λ，ηπ，U nidir（C）是自动机Unidir（C1），. ，Unidir（Cn），λ，ηπ.M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-2153.2非否认协议MTA在本小节中，我们将介绍MTA，它描述了上一节中介绍的协议。MTA由三个连续的组件组成，每个组件对应一个参与者，如图1、2和3所示。为了描述目的，转换的触发器和动作由形式为Ai（对于图1中的Alice）Bi（对于图2中的Bob）和Ti（对于图3中的TTP）的标签修饰。忽略了无限延迟和无限超时，而标签≤T代表超时（s0，T），s0是初始状态。通道α连接Alice和Bob，通道β连接Alice和TTP，通道γ连接Bob和TTP。我们假设信道是弹性的，也就是说，定时信道函数λ使得λ（α）= λ（β）= λ（γ）=（0，ω）。此外，我们假设恒等函数η将A分配给Alice，B分配给Bob，TT分配给TTP。符号M、L、T和所有形式为fn（n是符号名）的符号都是消息; K是A的键，C是结构化消息{M}K; X、V、Y、Z、W和H是形式参数。让我们更详细地考虑图1中Alice的顺序分量。Alice通过发送证据EOO来开始协议执行（注意触发器A1为True）。对应于EOO的结构化消息是符号A（fEOO，B，L，T，C）（为了简单起见，我们忘记配对，例如，我们写fEOO，B，L，C而不是（fEOO，（B，（L，（T，C）。参考图2，Bob正在等待由B1标记的对应参数消息。请注意，Alice发送的基础消息L和C将分别用形式参数X和Y统一。图1中使用的其他简写列表如下：EOR具有形式符号B（fEOR，A，L，T，C）; EOO K具有形式符号A（fEOOK，B，L，K）; EOR K具有形式符号B（fEORK，A，L，K）; sub K具有形式符号A（fsubK，B，L，K）; con K具有形式符号TT（fCON，B，L，K）。根据协议描述，从现在开始，Alice的所有步骤都必须在时间T内完成。一旦她从鲍勃那里收到了目标证据的第一部分（EOR），她就把证据的最后一部分（EOO K）发送给鲍勃。然后，爱丽丝必须等待最后一部分证据（EOR K）。如果这个证据没有被传递（或者是因为Bob没有发送它，或者是因为通道延迟消息太多），她必须在给定的216M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-停止s0A1A2一个3<= T一个4真（f、B、L、T、C、EOO）EOO（fEOR，A，L，EOR）（f，B，L，K，EOO_K）EOOkA5（f，A，L，EOR_K）提高采收率kA6无<= TA7A8<= T真A，B，L，K，sub_K克<= TA9（fCON，A，B，L，K，con_K）A10零Fig. 1. Alice的顺序组件时间T，在开始协议之前预先选择。这由顺序分量的分支表示：在左侧分支上，Alice等待EOR K，在右侧分支上，她在时间T内调用TTP的干预。Bob和TTP的顺序组件（参见图2和图3）更简单。我们只观察到，Bob的序列分量有一个分支点，用于处理他可能从Alice接收EOO K或从TTP接收con K或两者都接收的情况。在Bob和TTP的顺序组件中使用的简写列表如下：EOO-B具有形式符号A（fEOO，B，X，T，Y）;EOR-B具有形式符号B（fEOR，A，X，T，Y）;EOO K-B具有形式符号A（fEOOK，B，X，W）;EOR K-B具有形式符号B（fEORK，A，X，W）;conK − B具有符号TT（fCON，A，B，！X，W）;停止M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-2172停止停止sub K−T有符号A（fsubK，B，V，H）的形式;con K − T有符号TT（fCON，A，B，V，H）的形式。请注意，Bob的顺序组件在触发器B1的参数X中接收到协议运行L的标识符，然后通过利用！X在触发器B3和B4中。s0B1EOR（fEOO，B，X，T，Y，EOO−B）B（f，A，X，EOR−B）EORB3 （f，B，！X、W、EOO_K−B）EOOk（f，A，X，EOR_K−B）4提高采收率kB5B6<= T（f CON，A，B，！X，W，con_K−B）无<= T图二. Bob的顺序组件s0<= T<= TT1π（f，B，V，H，sub_K−T）克（f，A，B，V，H，con_K−T）2CONT3TrueT4A，B，V，H，con_K−T停止图三. TTP的顺序分量不218M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-−→4从MTA到时间自动机MTA的语义是通过翻译到众所周知的设置中来给出的时间自动机[2]翻译分两步进行：首先，我们将一个顺序组件翻译成一个（开放的）时间自动机，其转换由符号标记，用于不完全通信;然后，我们取这样获得的顺序组件的乘积，并同步不完全通信。一般来说，所得到的翻译不能保证是一个时间自动机，因为从我们的翻译产生的位置集可能是无限的。幸运的是，在感兴趣的情况下，很容易找到足以保证位置有限性的语法约束例如，可以自然地强制执行的一个充分条件是，顺序分量中的每个周期应该至少包含一个输入状态。为了完整起见，我们开始定义时间自动机及其语义。定义4.1字母表S上的时间自动机是元组L，L0，CK，I，δθ，其中• L是位置的有限集合;• L0L是初始位置的集合;• CK是一组有限的时钟;• I：L→Φ（CK）是将时钟约束与每个位置相关联的不变映射，其中时钟约束Φ（CK）的集合由以下语法定义：φ：= True|z≤c|c≤z|z< C|C< z|φ1φ2，其中z是CK中的时钟，c是Q≥0中的常数;• δL× S ×Φ（CK）×2CK×L是跃迁关系。元素s，a，φ，λ，sJ∈δ，也写作sa，φ，λsJ，表示符号a上从位置s到位置sJ的转换;时钟约束φ指定何时启用转换，并且集合λCK给出时钟在执行转换时被重置。现在我们非正式地回顾一下时间自动机的语义，请读者参考文献以获得标准定义。时间自动机A= L，L0，CK，I，δA的语义是通过关联一个转移系统TSA来定义的。TSA的状态是一对s，v，使得s是A的位置，v是CK的时钟估值（即，的映射M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-219CKtoQ≥0）使得ν满足不变量I（s）。对于所有时钟z，如果s是初始位置并且ν（z）= 0，则状态是初始状态。在TSA中有两种类型的转换：由于时间的流逝而引起的状态变化：对于一个状态，v_s和一个时间增加，项γ∈ Q≥0，εs，νγ⟩ −→⟨s，ν+γj，如果对于所有0≤γJ≤γ，ν+γJ满足不变量I（s）（ν+γ）表示映射每个时钟z到v（z）+γ）;由于位置转移引起的状态变化对于状态s，v，和trans-s，sitionns，a，φ，λ，sJsuchth atνsatis f iesφ，s，ν−→as，ν[λ：=0]表示将0分配给每个z∈λ的时钟赋值，并且与其余的时钟）。在下文中，我们假设MTA对于p：X→SM，m，X，p（m）X或X通过ρ（X）。对于MTA的连续分量Ci= I，δ，Kw，i，，Cn，λ，ηπ，我们定义了一个时间分量TC（Ci）= πTS，TSI，CK，TI，Tδπ（即时间自动机），其中TS是位置集，TSI是初始位置集，CK是时钟集，TI是不变函数，Tδ是转移关系。TS中的位置是一个元组KwS，Ch，s，ρρ，其中• KwS是该地点已知的证据（即地面信息）的集合;• Ch跟踪组件从已经建立但尚未完成（由于传输持续时间）的通信接收的消息集;每个不完整的交互由信道名称、（参数）预期消息和地面发送消息描述;预期和发送消息对允许在传输完成时将形式参数与消息绑定;• s∈S是分量Ci的当前状态;• ρ是将参数绑定到消息的部分映射。更正式地，定时分量TC（Ci）如下：(i) TS={<$KwS，Ch，s，ρ<$：KwS<$SM<$，<$，Ch<$Γ×SM<$，χ×SM<$，<$，s∈S，ρ<$X×SM<$，<$};(ii)TSI={<$Kw（s），ε，s，ε ε：s∈I};(iii) CK={cks：s∈S}<${ckη（i），m：m∈ M}<${ckη（i），α：α∈Γ};220M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-−→−→−→−→−→亩−→亩(iv) TI是这样的：TI（φKwS，Ch，s，ρψ）=φ1<$φ2<$φ3，(a) φ1是时钟约束{True}{cks≤τ：cks≤τ发生在从位置<$KwS，Ch，s，ρ<$}出发的跃迁t∈Tδ的时钟约束中。(b) φ2是时钟约束集合的合取{True}<${ckη（i），m≤τ：存在mJ∈KwS<$π3（Ch），其中出现形式为<$（m）或Θ（m）或IτJ（m）的消息}（πττj是标准投影函数沿第j个分量）;(c) φ3是时钟约束集合的合取{真}<${ckη（i），α≤τ2：λ（α）=（τ1，τ2），α∈π1（Ch）};(v) Tδ是以下集合的并集：(a) {KwS，Ch，s，ρ！α（ρ（m）），True，{cksJ}<$KwS，Ch，sJ，ρ：好吧，真的，！α（m），（s，0），（s，ω），SJ∈δ，SJ/∈I，ρ∈（m）是基元年龄，KwS∈η（i）ρ∈（m）};(b) {KwS，Ch，s，ρ！α（ρ（m）），True，{cksJ}<$KwSJ，，sJ，：好吧，真的，！α（m），（s，0），（s，ω），sj<$∈δ，KWSJ=Kw（SJ），SJ∈I，ρ<$（m）是一个广义的m年龄且KwS<$ρ<$（m）};(c) {KwS，Ch，s，ρNil，T rue，{cksJ}KwS，Ch，sJ，ρ：s，True，Nil，（s，0），（s，ω），sj<$∈δ，SJ/∈I};(d) {KwS，Ch，s，ρNil，T rue，{cksJ}Kw SJ，ρ，sJ，ρ：{s，True，Nil，（s，0），（s，ω），sj<$∈δ，KWSJ=Kw（SJ），SJ∈I};(e) {KwS，Ch，s，ρ？α（m），φφΘ，Clocks KwS，ChJ，sJ，ρ什么？α（m），Nil，（s1，τ1），（s2，τ2），SJ∈δ，ChJ=Ch{α，m，MJ}，SJ/∈I，Ch中不存在以α为第一分量的元组t（m，mJ）=πT，ρ（mu，ρu），其中T={K∈ K：KwS<$η（i）K}，在KwS中不存在定时出现的mu的定时原子子消息，如果τ2=ω且φΘ=cks2≤τ2，则φ ε=cks1≥τ1，φ Θ = True，否则，Clocks={cksJ，ckη（i），α}<${ckη（i），m：m∈ M是mJ的定时子消息}}(f) {KwS，Ch，s，ρ？α（m），φ∈φΘ，{cksJ}<$KwSJ，ε，sJ，ε：什么？α（m），Nil，（s1，τ1），（s2，τ2），SJ∈δ，SJ∈I，Ch中没有元组t具有α作为第一分量，（m，mJ）=πT，ρ（mu，ρu），其中T={K∈ K：KwS<$η（i）K}，在KwS中不存在mu的定时原子子消息;KWSJ=Kw（SJ），如果τ2=ω且φΘ=τ1，则φΘ=真否则，cks2≤τ2}M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-221−→(g) {KwS，Ch，s，ρTrue，φφΘ，{cksJ}KwS，Ch，sJ，ρ：222M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-−→亩−→τ−→J−→−→τs，True，Nil，（s1，τ1），（s2，τ2），sJ∈δ，sJ/∈I，如果τ2=ω，则φΘ=真，否则φΘ=cks2≤τ2}(h) {KwS，Ch，s，ρTrue，φφΘ，{cksJ}KwSJ，Ch，sJ，ρ：S，True，Nil，（s1，τ1），（s2，τ2），SJ∈δ，SJ∈I，KWSJ=Kw（SJ），如果τ2=ω，则φΘ=真，否则φΘ=cks2≤τ2}(i) {KwS，Ch，s，ρφ，φ，φ KwSJ，ChJ，s，ρj：⟩ −→ ⟨φ=τ1≤ckη（i），α≤τ2，如果λ（α）=（τ1，τ2）和φ=τ1≤ckη（i），α，如果λ（α）=（τ1，ω），<$α，m，mJ<$∈Ch，KwSJ=KwS<${mu}，其中（m，mJ）=πT，ρ（mu，ρu）和T={K∈ K：KwS<$η（i）K}，ChJ=Ch\{α，m，mJ}，ρJ=ρu <${（X，m）：（X，m）∈ρ，ρu对X没有定义}}，(j) {KwS，Ch，s，ρ，ckη（i），mJ=τ，ρKwSJ，Ch，s，ρ：KwSJ= KwS\ {m}{m [mJ|（mJ），Θ τJ（mJ）|对于某些人来说，τIτ（m）m∈KwS，其中m有一个子消息，其形式为<$τ（mJ）或IτJ（mJ）}(k) {KwS，Ch，s，ρ，ckη（i），mJ=τ，ρKwSJ，Ch，s，ρ：KwSJ= KwS\{m}{m[t（m）|Θ（MJ）]}，对于某个m ∈ KwS，其中mτ具有形式为θτ（mJ）}的子消息(l) {KwS，Ch，s，ρ，ckη（i），mJ=τ，ρKwS，ChJ，s，ρ：ChJ= Ch\{<$α，mJJ，m<$}<${<$α，mJJ，m [mJ|（mJ），Θ τJ（mJ）|τ JJ]}，对于τIτ（m）某个m∈Ch，其中m具有以下形式的子消息：（mJ）或IτJ（mJ）}ττ(m) {KwS，Ch，s，ρ，ckη（i），mJ=τ，ρKwS，ChJ，s，ρ：ChJ= Ch\ {α，mJ，mj}{α，mJ，m[t（mJ）]|（1）对于某些其中m具有形式为θτ（mJ）}的子消息。组件的时钟CK的集合为S中的每个状态、每个接地消息和每个通道名称提供不同的时钟名称。关于跃迁关系Tδ，我们有：a是对应于发送动作并导致一种非输入状态;发送动作不影响证据的收集和参数的绑定;注意只能发送基础（可导出）证据b是发送动作对应的导致输入状态的转换集合，证据收集和参数绑定被重置，并且不完整的消息被丢失;c-d是对应于Nil动作的转换的集合，该Nil动作导致非M. Napoli et al. / Electronic Notes in Theoretical Computer Science 99（2004）205-223输入状态和输入状态;e是对应于接收动作（导致非输入状态）的转换集合;为了组合性，该集合包括转换对于可与m统一的每个地面消息mJ，假设mJ不在忙信道中发送（即，仍然涉及不完整的通信），并且mJ不对已经属于证据集合的定时的地面消息进行重新定时;由于通信可能花费时间，所以将接收到的消息添加到位置的分量Ch，以不影响证据集合或变量的绑定;φθ和φΘ分别将顺序分量转换的延迟和超