基于I/O自动机的密码协议在异步分布式系统中的形式化验证

理论计算机科学电子笔记99（2004）339-359www.elsevier.com/locate/entcs基于I/O自动机C. Blundo，S.西马托河De Prisco，A.L. 费拉拉1Dipartimento di Informatica edApplicationzioniUniversit`adiSalerno84081 Baronissi（SA）摘要异步分布式系统的描述和推理通常是一项困难且容易出错的任务。在本文中，我们实验的输入/输出自动机框架作为一个工具来描述和推理的密码协议运行在异步分布式系统。我们研究了一个简单的认证电子邮件协议[5]，使用IOA模型给出了它的形式化，并证明了一些安全属性在协议的执行过程中得到满足。1介绍随着互联网和万维网的普及，我们的社会越来越依赖于通过计算机网络传输的通信数据。越来越多的人参与的大量交易实际上已经被数字模拟所取代，在数字模拟中，电子“物品”在两方或多方之间交换。一个例子来自电子邮件服务的差异，它允许用户交换包含文本或多媒体文件的消息由于电子邮件服务具有成本低、快捷方便等特点，越来越多地取代了普通邮件。在许多情况下，电子邮件消息被识别为在线交易的收据或证据，1Email：{carblu，cimato，ro bde p，fe rra ra}@ dia. n是a。It1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.015340C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-例如购买飞机票，或者为会议或期刊的出版物提交论文，等等。然而，使用电子邮件带来了一些问题，因为在其最简单的形式中，电子邮件服务不具有在这种情况下通常需要的许多特征。标准的电子邮件服务基于简单邮件传输协议[12]和邮政邮件协议[10]，它们不保证消息的传递和完整性消息通常以纯文本的形式存储和传输，从而允许恶意攻击者在传输过程中窃听连接，并使他能够访问敏感数据。为了提供某种形式的保护，已经采用密码技术来获得对电子邮件服务的附加保证文献中已经提出了许多认证的电子邮件协议，确保消息交换过程为参与者提供不同的安全属性。通常这样的协议涉及一个可信的第三方（简称TTP），它控制参与者的行为，帮助他们进行消息交换，并在必要时解决任何争议根据TTP所扮演的角色，协议被分为内联协议和乐观协议。在内联协议[3，5，14，15]中，TTP积极参与每个消息交换。在乐观协议[1，2，9]中，发送者和接收者在没有TTP干预的情况下执行消息交换，但他们可以调用TTP来解决任何争议，例如由一方的欺骗企图引起的争议本文分析了DengIOA提供了一个框架，允许对代码进行精确的描述，并提供非常详细的证明[6，13]。的工作的目的是使用IOA作为一个工具来描述和推理运行在异步分布式系统中的密码协议。在这个角度来看，执行分析，我们考虑的情况下，参与者的协议被建模为一个分布式系统中的相互作用的节点。然后通过IOA自动机描述它们的行为。然后使用IOA模型来证明在协议执行期间满足某些安全属性。在文献[8]中，IOA形式主义已经被用于安全协议的建模和分析，其中一个简单的共享密钥通信协议和Di Jane-Helmann密钥分配协议的正确性已经被证明。Asokan认证电子邮件协议的安全性[1]已经在[11]中进行了分析，其中采用了依赖于可模拟性和概率状态转换机的正式模型。本文的组织结构如下。在下一节中，我们将介绍C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-341框架，我们认为分析协议，提出的设置和加密的协议执行过程中使用的原语。在第3节中，我们描述了邓最后，在第5节中提供了协议的正确性，其中在不变断言证明的帮助下，证明了源和目的地的不可否认属性以及公平性。结论见第6节。2框架我们考虑一个由n个节点（处理器）组成的分布式系统P={1，2，...，n}和一个特殊的节点，即受信任的第三方（简称TTP），它由参与者委托来控制各方的行为，在消息交换期间协助他们，并在必要时解决任何争议。TTP是完全信任方，意味着接收者和接收者对它有完全的信任。此外，集合P {TTP}中的每个节点之间都有一个通信信道。2.1密码原语本文中使用的加密原语- SigA（m）：表示在公钥签名算法下使用用户A的私钥对消息m- h（m）：指示使用某种抗冲突散列方案的消息m的散列抗冲突哈希函数将任意长度的消息映射到恒定大小的消息，使得在计算上无法找到任何两个散列到相同值的不同消息- P KB（m）：表示在某种公钥加密算法中使用用户B的公钥对消息m进行加密算法应提供不可延展性，即，给定一个密文，不可能生成另一个密文，使得各个明文相关。- Ek（m）：表示在某种对称加密算法下使用密钥k对消息m2.2IOA自动机为了帮助不熟悉IOA的读者理解代码，我们用一个简单的例子简要解释如何阅读IOA代码IOA是一种简单类型的状态机，其中转换与命名操作相关联。图1显示了一个对通道进行342C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-通道i，j州：Msgs，M的一组元素，初始为空行动：input Send（m）i，jE组： 将m添加到Msgs任务：{接收（m）i，j}输出接收（m）i，j上一篇：mis inMsgsE组： 从消息中删除mFig. 1.自动机通道i，j用于从节点i到节点j的通信。状态是描述自动机状态的所有变量的列表。对于此通道，状态完全由一个变量描述，该变量包含仍在通道上传输的消息。通道有一个输入动作Send（m）i，j，它由另一个（在示例中未指定）自动机A（建模节点i）控制，该自动机具有与输出动作相同的动作Send（m） i ， j。每当自动机A执行这个动作时，通道也执行这个动作（同时），我们会说A的动作发送控制通道i，j的动作发送。在这种情况下，在通道自动机中，动作的结果是在传输中消息集合中添加消息。通道有一个输出动作Receive-m， i ， j，它有一个前提条件（布尔条件），指定动作何时被启用，即动作何时可以被执行。 只要启用输出操作，就可以执行该操作。此外，所有其他有这样一个动作作为输入的自动机都将执行它。将有一个自动机B，建模节点j，它有一个接收（m）i，j作为输入动作。也有类似于输出动作的内部动作（即，有一个前提条件和一个结果），不同的是它们不与其他自动机交互（即，几个自动机可以具有相同名称的内部动作，并且它们都是独立的）。我们使用符号name.var来表示自动机名称的变量var，例如CHANNEL。Msgs是指自动机通道i，j的变量Msgs。每个IOA都配备了其本地控制的操作的分区（输出和内部动作）;分区中的每个等价类表示自动机应该执行的某些任务。为了使输入/输出交互发生，描述系统的自动机必须组合在一起。多个IOA的组合是单个IOA。IOA的执行由从起始状态开始的交替状态和转变的序列组成。 如果每个任务都是公平的，C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-343有无限多的机会去执行它的一个动作。形式上，IOA A的执行片段α被认为是公平的，如果以下条件对于A的每个C类任务成立：(i) 如果α是有限的，那么C在α的最终状态下不被使能。(ii) 如果α是无限的，那么α要么包含来自C的无限多个事件，要么包含C未被启用的状态的无限多次出现我们建议读者参考[7]第8章和第23章，以了解有关IOA模型的更多信息。3CMP协议我们现在描述Deng等人在[5]中提出的用于认证邮件的CMP 1协议。图2提供了协议消息流的简明表示。发送器S第三方TTP接收器RM1=M2=M4= M3图二. CMP1协议消息流的简明表示。要发送一个包含m的邮件消息给接收者R，接收者S首先用他的私钥对（S，R，ttp，m）进行数字签名，以产生SigS（S，R，ttp，m）。然后，S生成会话密钥k，并使用对称密钥密码系统在k下加密签名数据。 最后，S计算h（m）并发送消息-SageM1 =ΣS，R，ttp，h（m），P Kttp（k），Ek（SigS（S，R，ttp，m））Σ S（R，ttp，m）.明文部分（即，S，R，ttp，h（m））作为邮件标识符。这个消息通知R有一封来自S的认证邮件给他。后接收到这个消息，R有两个选择。他可能会忽略这个消息。在这种情况下，协议被中止。他可以选择接收信息。在这种情况下，他使用他的私钥签名（S，R，ttp，h（m））并发送消息M2=ΣSigR（S，R，ttp，h（m）），P Kttp（k），Ek（SigS（S，R，ttp，m））Σt =TTP.在接收到该消息时，TTP首先使用R的公钥检查SigR（S，R，ttp，h（m））的有效性。然后，它使用其私钥解密P Kttp（k），并使用k解密Ek（SigS（S，R，ttp，m））。接下来，TTP使用S的公钥检查SigS（S，R，ttp，m如果两个值匹配，则TTP知道m是S想要发送给R的邮件内容，并且R愿意接受M。在这种情况下，TTP能够计算消息344C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-M3=对应于原产地证明的M2Sigttp（SigR（S，R，ttp，h（m），R，m，并且M4=对应于递送证明的M2Sigttp（SigS（S，R，ttp，m）），并且将它们分别发送到R和S在接下来的部分中，通过使用IOA模型，我们将证明协议CMP 1满足以下要求：• 不可否认的起源。该协议为电子邮件的收件人提供了一个无可辩驳的证据，证明收到的邮件内容与发件人发送的邮件内容相同。这种来源证明可以防止发件人错误地否认发送该消息的• 不可否认的交付。该协议为邮件发送者提供了一个不可撤销的证据，证明接收者收到的邮件内容与发送者发送的邮件内容相同。这种传递证明可以防止收件人错误地拒绝接收邮件。• 公平。协议的正确执行确保来自邮件接收者的此外，协议必须是故障安全的。也就是说，协议的不完全执行不会导致这样的情况：发送方可以获得递送证明，但接收方无法获得原产地证明，反之亦然。4使用IOA模型在本节中，我们将使用IOA模型详细描述CMP 1协议我们使用自动机发送者i来模拟节点i上的发送者部分，使用自动机接收者i来模拟节点i上的接收者部分。因此，每个节点i∈ P用自动机的合成来建模：发送者i和接收者i。TTP用单个自动机建模，并且对于每个i，j∈ P存在对节点i和节点j之间的信道进行建模的自动机。我们假设从ttp到任何节点i∈ P的信道是可靠的，即，我们假设这些信道在传送消息时不会丢失或改变。因此，我们区分两种类型的信道，一种是可靠的： 信 道 TTP ， i，另一种是不可靠的： UNRELCHANNELi，j，对于任何i∈ P和j∈ P ∈ {ttp}。整个系统由上述所有自动机的组合来描述图3给出了组成系统的自动机的概述C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-345不可靠通道i，j接收者jSENDERi不可靠通道i，ttp通道ttp，jTTP通道ttp，i不可靠信道j，ttp接收器i发送者j不可靠信道j，i图三. 建模为IOA的系统概述。4.1IOA代码的缩写发送方 i的代码如图4所示。对于每个会话，发送方保留以下信息：StatusSnd是发送者i设S={idle，send，wait，done}州：对于每个id∈ NStatusSnd（id）∈ S，初始空闲M1（id）∈ M，初始nilM4（id）∈ M，初始nil行动：Input Deliver（m，j）iE：id：=Getuniqid（m，j）M1（id）：=ConstrM1（m，id）;StatusSnd（id）：=send输出Send（M1（id），id ） i ， jPre ： StatusSnd（ id ） =send E Pre ：StatusSnd（id）：=wait任务：{Send（M1（id），id）i，j}Input Received（m，id）ttp，i返回：if（StatusSnd（id）=wait）M4（id）：=mStatusSnd（id）：=完成见图4。 自动发送器i我们现在可以从描述自动机动作开始，并将按照它们在代码中出现的顺序从上到下（左列第一）来查看它们。此顺序对应于执行操作的逻辑顺序。请注意使用唯一的标识符id：它被附加到与特定电子邮件相关的所有消息：这只是为了避免干扰来自其他会话的可能延迟的消息。我们假设环境告诉自动机何时将电子邮件m发送给收件人j;这由输入动作Deliver（m，j）i建模。通过函数Getuniqid为该电子邮件创建一个新的会话ID，该ID用于标识与该请求相关的所有通信的346C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-处理对电子邮件m的请求的第一步是简单地构造协议的第一消息M1=S，R，ttp，h（m），P Kttp（k），其中k是会话密钥，通过使用函数ConstrM1.变量StatusSnd设置为发送，以便唯一启用的（非输入）操作是发送操作。此操作与到接收者j的通道交互，并发送存储在M1中的消息。程序计数器进入等待状态等待。所有非输入操作均未启用现在当从TTP接收到消息时，执行继续。当接收到该消息时，将其存储到变量M4中。程序计数器更新为完成。 此时，协议已成功终止，没有别的事要做。输出动作Send是在一个任务中，所以在一个公平的执行它有无限多的机会来执行。4.2接收器的IOA代码接收器i的代码如图5所示。对于发送方，状态变量由会话id索引。同样，状态变量StatusRcv是“程序计数器”。变量M1、M2和M3用于存储协议的相应消息。接收器i设S={空闲，接收，等待，丢弃，完成}州：对于每个id∈ N状态Rcv（id）∈ S，初始空闲M1（id）∈ M，初始nilM2（id）∈ M，初始nilM3（id）∈ M，初始nil行动：Input Receiver（m，id）j，iE：M1（id）：=mStatusRcv（id）：=已接收输出Send（M2（id），id）i，ttpPre：StatusRcv（id）=已接收M2（id）=Constr M2（M1（id），id）E：StatusRcv（id）：=等待任务：{Send（m，id）i，ttp，Discard（id）i}output Discard（id）iPrev：StatusRcv（id）=已接收E组： StatusRcv（id）：=已丢弃Input Received（m，id）ttp，i返回：if（StatusRcv（id）=wait）M3（id）：=mStatusRcv（id）：=完成图五. 自动接收机i接下来，我们从上到下、从左到右描述这些Lose操作对损坏邮件的传递进行建模。程序计数器StatusRcv设置为丢弃，协议中止。第一个接收动作从通道中获取消息，并开始处理传入的消息。C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-347变量M1用于存储消息本身。程序计数器StatusRcv设置为已接收，以便启用的操作为发送和丢弃。自动机非确定性地执行这些动作之一。如果它执行Discard操作，则程序计数器StatusRcv被设置为丢弃，并且不必执行任何其他操作。否则，使用函数[001 pdf 1st-31files]构造M2消息M 2 = Σ SigR（S，R，ttp，h（m）），PKttp（k），Ek（SigS（S，R，ttp，m））的数据被构造并发送到TTP。 通过将StatusRcv设置为等待，自动机进入等待状态（未启用内部或输出操作）。自动机在接收到来自TTP的消息时退出此等待状态。当接收到此消息时，将其存储到变量M3. 程序计数器更新为完成。 此时，协议已成功终止。此会话的完成状态意味着接收者拥有原始电子邮件。发送和丢弃操作在同一个任务中，因此，在公平执行中，这个任务有无限多的机会来执行执行这些操作之一。4.3可信第三方的IOA代码TTP令S={空闲，接收，发送接收，发送snd，损坏，完成}州：对于每个id∈ NStatusTtp（id）∈ S，初始空闲Rcv（id）∈ P，初始为nilM2（id）∈ M，初始为nilSnd（id）∈ P，初始为nilM3（id）∈ M，初始为nil Hcheck（id）∈ B，初始为noM4（id）∈ M，初始为nilHTtpToRcv（id）∈ B，初始为no行动：Input Receiver（m，id）i，ttpE：if（StatusTtp（id）=idle）M2（id）：=mRcv（id）：=ExtractRcv（m）Snd（id）：=ExtractSnd（m）StatusTtp（id）：=已接收internalCheck（M2（id），id）ttpPrev：StatusTtp（id）=received状态Ttp（id）：=发送接收M3（id）：=构造M3（M2（id），id）M4（id）：=构造M4（M2（id），id）Hcheck（id）：=是elseStatusTtp（id）：=corrupt输出Send（M3（id））ttp ，Rcv（id）Pre：StatusTtp（id）=send rcvE t：StatusTtp（id）：=send sndHTtpToRcv（id）：=是输出Send（M4（id））ttp ，Snd（id）Pre：StatusTtp（id）=send snd输出：StatusTtp（id）：=完成Tasks：{Check（M2（id），id）ttp}，{Send（M3（id））ttp，Rcv（id）}，{Send（M4（id））ttp，Snd（id）}见图6。 自动机TTP348C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-TTP的代码如图6所示。对于每个会话，TTP保存以下信息：StatusTtp是 通过使用CheckSignHash（m，id）函数，TTP首先使用R的公钥检查SIGR（S，R，ttp，h（m））的有效性，然后解密P Kttp（k）。使用其私钥，并使用k解密Ek（SigS（S，R，ttp，m））。 接下来TTP使用S的公钥检查SigS（S，R，ttp，m如果两个值匹配，则TTP知道m是S想要发送给R，并且R愿意接收m。 在这种情况下，函数CheckSignHash（m，id）返回true，并且TTP能够分别通过使用函数Constr M3和ConstrM4来构造原产地证明和递送证明。此外，我们还使用了两个历史变量2Hcheck和HTtpToRcv。如果TTP能够构造分别对应于来源证明和递送证明的消息M3和M4，则变量Hcheck被设置为是，而如果TTP已经将消息M3发送到接收方，则历史变量HTtpToRcv的值为是 现在我们准备从上到下，从左到右描述自动机TTP接收（m，id）i，ttp动作从通道获取消息并将其存储到变量M2中。程序计数器StatusTtp被设置为已接收，使得可执行的操作是内部操作Check（M2（id），id）tp。 Check（M2（i d），id）ttp动作检查它是否可以使用CheckSignHash（m，id）函数构造递送和来源的证明。如果这是不可能的，则程序计数器StatusTtp被设置为损坏，并且协议中止。否则，TTP构造消息M3=Sig ttp（Sig R（S，R，ttp，h（m），R，m和M4=Sig ttp（Sig S（S，R，ttp，m）），并且程序计数器StatusTtp被设置为send rcv，使启用的操作是发送到接收方。最后，Send（M3（id））ttp，Rcv（id）动作将程序图Co nt erS ta tusT tp设置为senddsnd，并且可以执行向发 送 方 发 送 动 作 。 消 息 M4 被 发 送 到 发 送 方 ， 使 得 程 序 计 数 器StatusTtp被更新为完成。此会话的done状态意味着此会话已完成，并且没有其他事情要做。 执行Che ck（M2（i d），id）ttp、Sen d（M3（id））ttp 、Rcv（id）和Sen d（M4（id））ttp 、Snd（id）是三个不同的任务，因此，在执行时，它们有无限多的执行机会。2历史变量是仅用于证明的变量，但在实际代码中并不需要。C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-3494.4IOA通道UNREL CHANNELi，j的代码如图7所示。状态由包含仍在通道上传输的消息的变量Msgs描述。它具有输入动作Send（m，id）i，j，其结果是在传输中消息的集合中添加消息非确定性地，自动机可以执行任务中的两个动作之一：{接收（m，id）i，j，丢失（m，id）i，j}。接收（m，id）i，j动作模拟消息的传递，而丢失（m，id）i，j动作模拟在通道上传输的消息的丢失或更改UNREL通道i，j州：Msgs，M的一组元素，初始为空行动：input Send（m，id）i，jE组： add（m，id）到Msgsreturn return（m，id）i，j上一条：（m，id）在消息中E组： remove（m，id）fromMsgs任务：{接收（m，id）i，j，丢失（m，id）i，j}内部Lose（m，id）i，j上一条：（m，id）在消息中E组： remove（m，id）fromMsgs见图7。 自动机UNREL CHANNEL i，j，通道TTP，i的代码如图8所示。第2.2节描述了自动机。我们只添加了两个历史变量：HChanSnd（id）和HChanRcv（id）。 历史变量HChanSnd（id）对从TTP到i的消息，而变量HChanRcv（id）对消息的传递进行建模。通道ttp，i州：对于每个id∈ NMsgs，M的一组元素，初始为空HChanSnd（id）∈ B，初始无HChanRcv（id）∈ B，初始无行动：input Send（m，id）ttp，iE组： add（m，id）到MsgsHChanSnd（id）=是任务：{接收（m，id）ttp，i}return return（m，id）ttp，i上一条：（m，id）在消息中E组： remove（m，id）fromMsgsHChanRcv（id）=是见图8。 自动机通道TTP，i350C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-5CMP1协议在本节中，我们使用IOA模型分析了CMP 1协议，特别是我们证明了该协议满足第3 .第三章。在下文中，我们用S和R分别表示与代表发送者和接收者的过程相对应的索引在Check（m，id）ttp动作期间，TTP执行函数CheckSignHash（m，id），如果TTP能够构造分别对应于消息M3和M4的来源证明和递送证明，则该函数返回yes因此，为了证明协议CMP 1满足第3节中的性质，我们必须证明以下三个非正式断言：• 发送方最终接收到对应于由ttp构造的递送证明的消息M4。• 接收方最终接收到对应于由ttp构造的来源证明的消息M3。• 当且仅当收件人最终收到原产地证明时，发件人最终收到递送证明。下面我们将证明几个不变量，它们将用于证明上述陈述。5.1不变量第一个不变量表明，如果StatusSnd（id）=done，则协议的消息M4已被发送给发送方。不变量5.1在任何可达状态s中，如果s.StatusSnd（id）=done则s。CHANNELTTP，S. HChanRec（id）= yes.证明：通过归纳法对长度进行了计算。基本情况包括证明不变量在初始状态下为真。StatusSnd（id）最初是空闲的。因此，不变量为真。对于归纳步骤，假设不变量在可达状态sJ中为真。我们需要证明在s中对于 任 何 可 能 的步 （ SJ ， π ， s ） 都 是 真 的 。 如果 s.StatusSnd （ id ）/=done，则不变量为true。因此，假设s.StatusSnd（id）=done。我们必须区分以下两种情况：• sJ.StatusSnd（id）= done。 根据归纳假设，SJ信道ttp，S. HChanRec（id）=yes.由于HChanRec（id）一旦设置为yes，永远不会改变，认为s.channel ttp，S. HChanRec（id）=yes.C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-351• sJ.StatusSnd（id）/=完成。仅存在一个将StatusSnd（id）设置为done的启用动作：π是发送方S自动化的接收（m，id）ttp，S动作。此输入动作由通道ttp，S自动机的输出动作Receive-t（m，id）ttp，S由于此操作设置了通道ttp，因此S。HChanRec（id）为yes，则如下所示s.channel，S. HChanRec（id）= yes.下一个不变量声明，如果我从TTP接收到消息，则该消息已由ttp发送。不变量5.2在任何可达状态s中，如果s。通道TTP岛HChanRecttp，i（id）=是的那么S。信道ttp，i.HChanSnd（id）=是。证明：通过归纳法对长度进行了计算。 基本情况包括证明不变量在初始状态下为真。最初，我们具有信道TTP，i。HChanRecttp，i（id）=否。因此，不变量为真。对于归纳步骤，假设不变量在可达状态sJ中为真。我们需要证明对于任何可能的步长（ SJ，π ，s），它在s如果我们有这个S。 通 道 TTP 岛HChanRec（id）=no，则不变量为真。假设S。通道TTP岛HChanRec（id）=yes.我们必须区分以下两种情况：• sJ。通道TTP岛HChanRec（id）=yes.从归纳假设，它认为，SJ。信道ttp，i. HChanSnd（id）=是的由于通道TTP，I. HChanSnd（id）一旦设置为yes，就不再改变，它保持s。通道TTP岛HChanSnd（id）=是。• 通道TTP岛HChanRec（id）=否。只存在一个设置% s的已启用操作。通道TTP岛HChanRec（id）toyes：π是信道ttp，iautomaton的输出动作Receive-up（m，id）ttp，i这个动作的前提条件是消息m是在信道TTP中，i. Msg.只有一个动作在通道TTP中插入消息，i.Msgs：通道ttp的输入动作Send（m，id）ttp，i，i automaton。此操作还设置通道TTP，i。HChanSnd（id）为yes。由于通道TTP，I. HChanSnd（id）一旦被设置为yes，就不再改变，因此s。通道TTP岛HChanSnd（id）=是。不变式5.3声明如果TTP已经向发送者发送了一条消息，它就完成了协议。不变量5.3在任何可达状态s中，如果s。CHANNELTTP，S. HChanSnd（id）=是那么s.StatusT tp（id）= done。352C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-S证明：通过归纳法对长度进行了计算。基本情况包括证明不变量在初始状态下为真。最初，我们有通道ttp，S。HChanSnd（id）=否。因此，不变量为真。对于归纳步骤，假设不变量在可达状态sJ中为真。我们需要证明对于任何可能的步骤（SJ，π，s），在SJ如果s。CHANNELTTP，S. HChanSnd（id）=no，不变量为true。假设S。CHANNELTTP，S. HChanSnd（id）=是。我们必须区分以下两种情况：• sJ。信道ttp，S . HChanSnd（id）=是。根据归纳假设sJ.StatusT tp（id）=done。由于StatusT tp（id）一旦被设置为done就不再改变，因此它保持s.StatusT tp（id）=done。• sJ。信道TTP，. HChanSnd（id）=是。只存在一个设置% s的已启用操作。CHANNELTTP，S. HChanSnd（id）to yes：π是通道ttp，S自动机的输入动作Send（m，id）ttp， S。这个输入动作由ttp自动机的输出动作Send（m，id）ttp，S控制。由于此操作将StatusT tp（id）设置为done，因此遵循s.StatusT tp（id）=done。下一个不变量表明，如果接收方已经完成了协议，则它接收到消息M3。5.4在任何可达状态s中，如果s.StatusRcv（id）=done，那么我们有s。CHANNELTTP，河HChanRec（id）= yes.证明：通过归纳法对长度进行了计算。 基本情况包括证明不变量在初始状态下为真。首先，StatusRcv（id）是空闲的。因此，不变量为真。对于归纳步骤，假设不变量在可达状态sJ中为真。我们需要证明对于任何可能的步长（ SJ，π，s），它在s如果它保持s.StatusRcv （id ）/=done，则不变量为真。因此，假设s.StatusRcv（id）=done。我们必须区分以下几分为两种情况：• sJ.StatusRcv（id）= done. 根据归纳假设，sJ。信道TTP， . HChanRec（id）= yes.自TTP通道以来，R. HChanRec（id）一旦设置为yes，就不再改变，它保持s。CHANNELTTP，河HChanRec（id）=yes.• sJ.StatusRcv（id）完了 只存在一个启用的操作，StatusRcv（id）to done：π是输入动作接收（m，id）ttp，R 的，托马顿接收器河此输入操作由输出操作控制接收信道ttp，R的（m，id）ttp，R。RC. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-353R由于此操作设置了通道ttp，因此R. HChanRec（id）为yes，则如下所示S. CHANNELTTP，河HChanRec（id）= yes.下一个不变量表示，如果消息在从ttp到接收方的信道上传输，则消息由TTP发送。不变量5.5在任何可达状态s中，如果s。CHANNELTTP，河HChanSnd（id）=是的那么S。HTtpToRcv（id）=是。证明：通过归纳法对长度进行了计算。 基本情况包括证明不变量在初始状态下为真。最初，我们有这个通道ttp，R。HChanSnd（id）=否。因此，不变量为真。对于归纳步骤，假设不变量在可达状态sJ中为真。我们需要证明对于任何可能的步长（SJ，π，s），它在s如果我们有这个S。CHANNELTTP，河HChanSnd（id）=no，则不变量为真。假设S。CHANNELTTP，河HChanSnd（id）=是。我们必须区分以下两种情况：• sJ。信道特普河. HChanSnd（id）=是。 根据归纳假设，这是J。HTtpToRcv（id）=是。 由于HTtpToRcv（id）一旦被设置为yes就不会再改变，所以它保持s。HTtpToRcv（id）=是。• sJ。信道TTP，. HChanSnd（id）=否。只存在一个启用的操作，S. CHANNELTTP，河HChanSnd（id）到yes：π是通道ttp，R的输入动作Send（m，id）TTP，R。 该输入动作由TTP自动机的输出动作Send（m，id）TTP， R控制。 由于此操作将HTtpToRcv（id）设置为yes，因此s。HTtpToRcv（id）=是。不变量5.6表明，如果TTP完成了协议，那么它已经向接收方发送了消息M3不变量5.6在任何可达状态s中，如果s.StatusT tp（id）= done，那么我们有s。HTtpToRcv（id）=是。证明：通过归纳法对长度进行了计算。基本情况包括证明不变量在初始状态下为真。状态T tp（id）=空闲。因此，不变量为真。对于归纳步骤，假设不变量在可达状态sJ中为真。我们需要证明对于任何可能的步长（SJ，π，s），它在s如果s.StatusT tp（id）/=done，则不变量为真。因此，假设s.StatusT tp（id）=done。我们必须区分以下几分为两种情况：354C. Blundo等人/ Electronic Notes in Theoretical Computer Science 99（2004）339-• sJ.StatusT tp（id）= done. 从归纳假设，它遵循， SJ。HTtpToRcv（id）=是。由于HTtpToRcv（id）一旦被设置为yes就不会再改变，所以它保持s。HTtpToRcv（id）=是。• sJ.状态T tp（id）完了只 存在一个启 用的 操作，S. StatusT tp（id）todone：π是tp的输出作用Sen d（m（id））tp ，Snd（id）自动机 这一行动的前提条件是：StatusT tp（id）= send-snd.将StatusTp（id）设置为send-snd的唯一动作是TTP 自动机的输出动作Sen d（m（id））ttp，Rcv（id）。 此操作还将HTtpToRcv（id）设置为yes。由于HTtpToRcv（id）一旦设置为yes就不再改变，因此它认为，S. HTtpToRcv（id）=是。下一个不变量显示TTP执行内部操作Check在执行其发送操作之前。不变量5.7在任何可达状态s中，如果s.StatusT tp（id）∈ {send-rcv，send-snd，done}然后s。Hcheck（id）= yes.证明：通过归纳法对长度进行了计算。基本情况包括证明不变量在初始状态下为真。初始状态tp（id）是空闲的。因此，不变量为真。对于归纳步骤，假设不变量在可达状态sJ中为真。我们需要证明对于任何可能的步长（SJ，π，s），它在s中为真如果s.StatusT tp（id）/∈{send-rcv，send-snd，done}，不变量为真。否则，我们必须区分以下两种情况：• sJ.状态T tp （id）∈ {send-rcv，send-snd，done}。从归纳假设SJ.Hcheck（id）=yes.由于Hcheck（id）一旦设置为yes，就不再改变，因此可以得出s。Hcheck（id）=yes.• sJ.状态T tp（id）∈ {send-rcv，send-snd，done}。只存在一个启用的操作，它将StatusT tp（id）设置为