基于密钥链的TTP透明CEM协议的安全性验证

理论计算机科学电子笔记274（2011）51-65www.elsevier.com/locate/entcs基于密钥链的TTP透明CEM协议的刘志远a庞军b张晨毅ca卢森堡大学，卢森堡山东大学，中国卢森堡大学，卢森堡c卢森堡大学，卢森堡新南威尔士大学，澳大利亚摘要在认证电子邮件（CEM）协议中，TTP透明度是一项重要的安全要求，有助于避免不良宣传以及保护个人用户的隐私。 最近，我们扩展了Cederquist等人的CEM协议，以满足TTP透明性。 作为延续，本文对扩展协议中的安全需求进行了形式化验证。 在模型检验工具Mocha中检验了公平性、有效性和及时性，在工具集μCRL和CADP中分析了TTP透明性。结果证实，我们提出的扩展实现了我们的设计目标。关键词：验证，公平性，及时性，TTP透明性，CEM协议，Mocha，μCRL1引言认证电子邮件（CEM）协议作为常规电子邮件服务的扩展，要求发送者和接收者都对他们在电子邮件服务中的角色负责。这意味着，当协议成功运行到最后时，发送者不能拒绝发送电子邮件，接收者也不能拒绝接收。这种要求通常由接收方获取的不可否认的来源证据（EOO）和发送方获取的不可否认的接收证据（EOR EOO和EOR都可以作为争议的证据。作为一类特殊的公平交换协议[20]，CEM协议应该保证关于不可否认证据的公平性。非正式地，在公平协议运行结束时，要么双方都获得所有证据，要么没有一方获得证据。可以引入可信第三方（TTP）来负责整个过程，并提供不可否认的提交（发送者）和交付（接收者）记录。然而，以这种方式，如果TTP必须涉及大量CEM服务，则TTP可能容易成为瓶颈。1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.07.00652Z. Liu等人理论计算机科学电子笔记274（2011）51一个更好的解决方案，即所谓的乐观协议[5]，有助于从TTP中释放这种负担。在乐观协议中，TTP只需要在意外事件（例如网络故障或一方的不当行为）的情况下参与，以恢复公平性。如果签名者和接收者都表现正确，并且不存在显著的网络延迟，则CEM协议在没有TTP干预的情况下成功终止。TTP透明度规定，如果TTP已被联系以帮助制定方案，则所得证据将与TTP未参与的情况下获得的证据相同。换句话说，单看证据，是不可能发现TTP是否参与其中的。在实践中，透明的TTPs是重要和有用的，例如，可以避免负面宣传。此外，该属性还确保了参与者向TTP寻求帮助的隐私在CEM协议的背景下，透明TTP的使用首先由Micali [17]提出，随后进行了许多工作，例如，[16，18，19，21，12]，其中使用不同的加密方案来实现TTP透明性。最近，我们已经开发了一个具有透明TTP的CEM协议[15]，该协议基于Cederquist等人的协议。[9]该协议应用密钥链来减少TTP的存储需求。我们通过采用[22]的可验证加密签名方案来实现TTP透明性。我们已经证明，我们的扩展是满足TTP透明性的最有效的CEM协议之一，除了其他重要属性，如强公平性、有效性和及时性。对我们的主张的公正性是在相当非正式的层面上进行的[15]。在本文中，我们打算把我们的分析更进一步，通过结合形式验证技术。有限状态模型检查器Mocha [4]用于验证公平性，及时性和有效性的属性，这些属性在具有游戏语义的交替时间时态逻辑（ATL）公式中自然解释[3]。ATL中表达的属性的验证对应于获胜策略的计算。另一个工具集μCRL [7，6]用于TTP透明性，这需要在各种情况下比较可观察的跟踪。μCRL工具集具有生成状态空间的能力，这些状态空间可以由工具箱CADP [11]可视化和操作，该工具箱充当μCRL的后端论文的结构 我们解释了我们提出的CEM协议的扩展[9]，并在第2节中讨论了其所需的属性。两个验证工具Mocha和μCRL将在第3节中简要介绍。在第4节中，我们验证了Mocha的公平性，及时性和有效性，重点是建模，并在第4节中。5验证了μCRL中 TTP的透明性相关工作将在第二节讨论第六章我们在节结束的第七章2一种基于密钥链的TTP透明CEM协议我们的协议是在协议[9]的基础上开发的，以支持TTP透明性。密钥链用于减少TTP的存储需求。一旦在Alice和Bob之间初始化了密钥链，Alice就可以使用其中的任何密钥来加密消息。我们的方法需要使用可验证加密的签名方案，Z. Liu等人理论计算机科学电子笔记274（2011）5153对接收者接收电子邮件的承诺进行编码为了便于阅读，我们将发送者写成Alice，接收者写成Bob. 我们假设通信信道是弹性的，在这个意义上，每个消息都保证最终到达目的地。我们写{M}k表示用对称密钥k加密的消息m，并且（M）P表示消息M上的参与方P1我们写（M）B|T表示Bob在M上的可验证加密（部分）签名，通过使用TTP的公钥加密Bob在M上的签名。每个人都可以证明（M）B|T是可信的，但是只有TTP和Bob能够从（M）B中提取出完整的签名（M）B|T.2.1该协议协议的结构由交换子协议、中止子协议和恢复子协议组成。交换子协议由通信双方执行，以传递电子邮件以及交换不可否认的证据。其他子协议由一方发起，以联系TTP来处理错误情况。每个使用协议的交换被称为一个协议回合，一个初始化阶段之后的多个协议回合被称为一个协议会话。每个协议会话属于唯一的一对通信方。钥匙链生成。在乐观CEM协议中，如果交换过程中断，通信方将请求TTP帮助。为了实现（强）公平性，TTP通常需要存储足够数量的信息，以便能够解密、检索或发送信息，从而使协议最终达到公平状态。在大多数现有的CEM协议中，发起者使用TTP第一种方法通常需要非对称密钥操作，这比对称密钥操作更昂贵。第二种方法给TTP存储交换信息的负担，例如参与方，电子邮件内容的哈希值等。为了减少TTP存储过多信息的负担，协议[ 9 ]使用密钥链。k eys的c链是keys的序列K0J， . ，KnJ，使得对于每个i≥0，KiJ：=H（Gi（K 0）），其中K 0是种子，H：κ → κ是公知的单向抗碰撞哈希函数，G：κ → κ是公知的非循环哈希函数，function（k是key domain）。H和G是不可交换的，即，给定一个H（Ki），其中Ki是未知的，计算H（G（Ki））是不可行的初始化。 为了初始化会话，发起者Alice（A）将密钥链种子K0和潜在响应者Bob（B）的身份连同随机数nc一起发送到TTP（T）。TTP将检查在她的数据库中是否已经存在指示密钥链是否已经建立的条目A，B，K0，SIDJ如果是，TTP将忽略此请求。否则，TTP将选择一个新的会话标识sid，并将消息cert：=（A，B，sid）T发送给Alice，然后在她的数据库中存储certA，B，K0，sid01在实践中，签名总是应用于散列值。54Z. Liu等人理论计算机科学电子笔记274（2011）51M我M一一M我MB我交换子协议。下面描述协议会话sid中的第i个协议轮。舍入数i最初为0，并且可以任意增长，Alice递增1i每轮之后。为了方便起见，我们使用EOR2表示（EOOM）B|T.1例。 A → B：A，B，T，i，sid，h（KiJ），{M}K′，EOOM，cert12例。B→A：EOR 23例。A→B：KiJ4例。B→A：EORM首先，Alice发送消息1ex给Bob。在收到EOOM之后，Bob在EOOM上发送他的部分签名以表明他承诺接收电子邮件。如果Alice进一步向Bob发送密钥KiJ，Bob将向Alice返回一个完整的签名作为收到的最终证据。中止子协议。只有Alice可以中止，前提是协议尚未恢复。通常，如果Alice没有接收到消息2ex，则她中止。为了中止交换，Alice向TTP发送以下消息：1 .一、 A → T：f a，A，B，i，sid，h（{M}Ki′），abrt其中，fa是用于标识中止请求的签名，并且abrt是Alice在中止请求上的签名。在收到这个请求后，TTP会检查几件事，如签名、身份、密钥链条目和状态（i）的正确性，以做出决定。如果状态（i）尚未初始化，TTP将其设置为中止（状态（i）：=a）并发回中止令牌。如果当前轮已经恢复，则TTP检查status（i）是否=h（{M}Ki′）。 如果是，TTP将发回一个恢复代币否则，形式为（error，（error，abrt）T）的错误消息为送回来的恢复子方案。允许Alice启动恢复子协议，只要她已经发出了消息3ex，但是还没有接收到消息4ex。类似地，如果Bob已经发送了消息2ex，但是还没有接收到消息3ex，则他可以启动恢复子协议。Alice的恢复子协议的第一条消息是11河 A → T：fr，A，B，h（KiJ），h（{M}K′），i，sid，EOR 2，EOOM其中FR是用于标识恢复请求的标记。Bob的恢复子协议的第一条消息是1河 B → T：f r，A，B，h（KiJ），h（{M}K′），i，sid，EORM，EOOM在接收到用于恢复的消息时，TTP需要检查（1）1(veriEORM和EORM（EOR2）上的可加密）签名 （2）身份TTP，以及（3）在其数据库中是否存在与HTTPA、B、*、SIDHTTP匹配的条目。如果所有Z. Liu等人理论计算机科学电子笔记274（2011）5155M我一B如果上述检查成功，TTP将检索K0，以及（4）检查h（H（Gi（K0）是否匹配h（KiJ）。如果是，TTP将检查第i轮的状态（i）。• 如果状态（i）尚未初始化，TTP将设置状态（i）：= h（{M}Ki′）。当-必要时TTP转换EOR2 进入EORM。 之后，TTP发送以下消息。2河T→B：KiJ，（KiJ）T3河T→A：EORM• 如果status（i）= h（{M}K′），则TTP（再次）执行步骤2r和步骤3r。• 如果status（i）=a，则TTP向发起协议的一方发送中止令牌。2河 T→A（B）：abrt，（abrt）T如果测试（1）、（2）、（3）和（4）中的任何一个失败，TTP将忽略恢复请求并发回错误消息。2河 T→ A（B）：误差，（误差，m r）T其中mr是在步骤1r或1r中接收的整个消息。证据和争议解决。当发生争议时，双方都需要向外部法官提供证据。对于每个协议回合i，Bob期望的EOO（起源证据）包括：A，B，T，M，i，sid，KiJ，EOO M.爱丽丝想要的EOR（收据证据）包括A，B，T，M，i，sid，KiJ，cert，EOR M.2.2安全要求下面的属性被要求满足所提出的协议。E.效率。如果未发生错误，则协议成功运行直至结束，无需TTP的任何干预。很准时。Alice和Bob都有能力在协议执行过程中的任何地方最终完成这是为了防止一个诚实的一方在意外情况下无休止的等待。公平。诚实的爱丽丝（鲍勃）会得到她（他）的证据，只要对方从她（他）那里得到证据。2证据可以用来说服裁决者，在Alice的情况下，Bob已经收到了邮件真正的信息发送者，在鲍勃的例子中如果对Bob2注意，只有诚实的参与者才需要受到保护。156Z. Liu等人理论计算机科学电子笔记274（2011）51Ⓧ□Ⓧ□从爱丽丝（鲍勃）的证据，即，它不一定涉及TTP，也不一定涉及Bob（Alice）的参与。TTP透明度。无论TTP是否参与方案执行，每位参与者获得的证据都具有相同的3Mocha和μCRL为了形式化地分析一个安全协议是否达到了它的设计目标，首先我们必须用一种形式化的语言来描述这个协议，然后表达所需属性的规范。模型检查器Mocha [4]允许指定具有并发游戏结构的模型，并使用具有游戏语义的ATL（交替时间时序逻辑）[3]公式表示属性，适用于检查公平性，有效性和及时性等属性。对于TTP透明度的分析，我们的主要思路是比较不同情况下3因此，使用进程代数语言μCRL及其工具集[7，6]。3.1摩卡和ATLMocha [4]是一个交互式验证环境，用于异构系统的模块化和层次化验证。它的模型框架是反应模块的形式。反应模块的状态由变量确定，并在一系列轮次中改变。Mocha可以检查ATL公式，这些公式将属性自然地表达为具有游戏语义的获胜策略。这是我们选择Mocha作为模型检查器的主要原因。Mocha提供了一种基于并发博弈结构的保护命令语言来对协议进行建模。这种语言的语法和语义可以在[4]中找到时间逻辑ATL是关于命题的有限集合和参与者的有限集合来定义的。ATL公式是以下公式之一：• p，对于命题p∈φ。• <$φ或φ1<$φ2，其中φ、φ1和φ2是ATL公式。• ⟨⟨A⟩⟩φ,⟨⟨A⟩⟩φ,or⟨⟨A⟩⟩φ1Uφ2,whereA⊆Σ is a set of players,andφ,φ1andφ2是ATL公式。ATL公式在具有相同命题和参与者的并发博弈结构的状态上进行解释[3]。用命题对并发博弈结构的状态进行标记逻辑连接词<$和<$具有标准意义。直觉上，运算符A的作用是选择性量化A中的智能体可以选择执行。路径量化器（next）、（globally）和U（until）具有它们在逻辑CTL中的通常含义，Qφ被定义为真Uφ。3.这是摩卡做不到的Z. Liu等人理论计算机科学电子笔记274（2011）5157ΣD3.2μCRL和CADPμCRL是一种以代数风格指定分布式系统和协议的语言。μCRL规范由两部分组成：一部分指定数据类型，另一部分指定进程。数据部分包含等式规范;可以声明排序和作用于这些排序的函数，并通过等式描述这些函数的含义。过程由过程术语表示。过程术语由操作名称和带有零个或多个数据参数的递归变量组成，并与过程代数运算符相结合。动作和递归变量携带零个或多个数据参数。直觉上，一个动作可以自己执行，然后成功终止。有两个预定义的动作：δ代表死锁，τ代表内部动作。p.q表示顺序合成，它首先执行p，然后执行q。p+q表示非确定性选择，这意味着它可以表现为p或q。求和d：Dp（d）提供了对数据类型D的可能无限选择。条件构造p b q，其中b是一个布尔数据项，如果b，则表现为p，如果不是b，则表现为q。并行组合pq使p和q的动作交错;此外，如果预定义的通信函数明确允许，来自p和q的动作两个动作只有在它们的数据参数相同时才能同步，这意味着通信可以用来捕获从一个进程到另一个进程的数据传输。如果两个动作能够同步，那么一般来说，我们只希望这些动作在相互通信中发生，而不是单独发生。这可以由封装操作符强制执行δH（p），它将集合H中所有在p中出现的动作重命名为δ。此外，隐藏算子τI（p）将集合I中所有在p中出现的动作都转化为τ。μCRL工具集[7]是用于分析和操作μCRL规范的工具集合。μCRL工具集与CADP工具集[11]一起作为μCRL工具集的后端，具有可视化，仿真，LTS生成和最小化，模型检查，定理证明和状态位哈希功能。4在Mocha中验证协议我们给出了我们的建模方法的草图，并讨论了扩展CEM协议的模型。详细的模型和分析见[14]。4.1在Mocha首先，每个参与者都被建模为玩家（在游戏中），使用Mocha的守护命令语言描述其行为。诚实参与者的模型可以很容易地严格按照协议指定。对于不诚实模型，我们主要考虑不诚实参与者因此，我们建立了诚实和不诚实的模型，58Z. Liu等人理论计算机科学电子笔记274（2011）51--空闲动作而不停止[]~pa_stoppa_eoo->--（1）爱丽丝发送EOO给Bob[]~pa_stop~A_contacted_T~pa_eoo->pa_eoo--（二）爱丽丝发送出来关键而接收半提高采收率参与者对于每个参与者，我们分别写Pi和Pi H来表示不诚实和诚实的模型直觉上，不诚实的模型Pi允许玩家作弊，而Pi H只是诚实地遵守协议。不诚实的行为包括在任何时候发送从他的知识中推导出的消息，在任何时候停止;因此，不诚实的模型可能不会在协议中的角色需要停止的时候停止。使用共享变量对通信进行证据（EOO和EOR），密钥和电子邮件被建模为布尔变量，初始化为false并由其发送者更新。我们将发送证据或其他消息的行为建模为一个受保护的命令，其中发送者将相应的变量重置为真。 在诚实参与者Pi H的模型中，守卫由严格按照协议满足的所有条件组成，命令由所有要执行的相应动作然而，对于不诚实的Pi，守卫只是由必要的消息组成，以生成要发送的消息名单1给出了描述诚实爱丽丝行为的摩卡代码。首先，Alice可以在她通过发送EOOM发起协议回合之后做空闲动作。对于诚实的Alice来说，她在交换子协议中主要执行两种动作，包括发送来源证据和密钥。它们在步骤（1）和（2）中描述步骤（1）对发送EOOM的动作进行建模，其中我们使用布尔变量hk和pa eoo，分别表示由Alice签名的KiJ和消息（B，T，i，sid，h（KiJ），{M}Ki′）A的散列值。将hk和pa eoo设置为true意味着Alice已经通过发送她的EOOM来发起与Bob的通信。步骤（2）表示如果Alice已经接收到正确的可验证加密的消息，即pb halffetch已变为真，则她可以将k设置为真，这表示发送密钥KiJ的动作。 除了交换子协议之外，如果Alice没有接收到可验证加密的消息，她也能够发起中止协议。鲍勃的签名pb一半。在步骤（4）中描述了中止请求，其中保护表示从TTP请求中止的要求，并且命令表示联系TTP以中止的行为。 除了中止子协议之外，Alice还可以发起在步骤（6）中建模的恢复子协议。 恢复请求被建模为布尔变量一个恢复请求，如果保护被满足，它将被设置为真，其中k和pb半值为真，而pb半值为假。注意，一旦诚实的Alice发起与TTP的恢复或中止子协议，她将不会继续交换子协议。 该机制是通过对布尔变量A与T的接触进行建模来实现的。最后，如果Alice从Bob接收到最终EORM（步骤（3））或从TTP接收到恢复令牌（步骤（7）），则她可以停止。中止令牌（步骤（5））还可以使Alice停止协议回合。以类似的方式，我们可以模拟鲍勃的诚实行为。清单1：为扩展的CEM协议Z. Liu等人理论计算机科学电子笔记274（2011）5159--空闲动作而不停止[]~pa_stoppa_eoo->--爱丽丝可以停止随时[]~pa_stoppa_eoo->pa_stop--（1）爱丽丝可以发送EOO 随时--发送正确散列关键字[]~ pa_stop& ~ pa_eoo& ~hk& ~ hke->pa_eoo--发送不正确散列关键字[]~ pa_stop& ~ pa_eoo& ~hk& ~ hke->“”= true;“hke--（2）Alice可以随时发送密钥[]~pa_stop~k ->k--（三）爱丽丝可以发送中止请求[]~pa_stoppa_eoo-> A_abort_req--（四）爱丽丝可以发送恢复请求[]~pa_stoppb_halfeorm-> A_reovery_req--（五）爱丽丝接收异常终止符记[]~pa_stopT_abort_send_A-> T_abort_token_A--（6）Alicereceivesrecoverytokenn[]~pa_stopT_recovery_send_A-> par_rece_eorm[]~ pa_stop&~ A_contacted_T&pb_halferom&~K->k--（三）爱丽丝可以停止当她接收Bob[]~ pb_stop&~ A_contacted_T&铅当量&~ par_rece_evening- ->- pa_rece_erom--（四）爱丽丝可以发送出来中止请求TTP如果她没接收一半EOR_M从鲍勃[]~ pa_stop&~ A_contacted_T&帕欧&~ pb_halfefeirs- ->- A_contacted_T--（五）爱丽丝停止后接收中止令牌从TTP[] ~ pa_stop A_contacted_T T_abort_send_A- ->- T_abort_token_A pa_stoop--（6）Alice可以在她拥有pb_halfefecycle时[]~ pa_stop&~ A_contacted_T&K&半铅&~pb_e- ->- A_contacted_T--（七）爱丽丝停止后接收恢复令牌从TTP [] ~pa_stop T_recovery_send_A->par_rece_eorm pa_stop名单2描述了不诚实的爱丽丝的行为，她的恶意行为描述如下。首先，爱丽丝不仅可以空闲，还可以随时停止和退出协议。发送EOOM和密钥的行为在步骤（1）和（2）中指定。步骤（1）模拟了Alice可以在任何时候通过将变量pa eoo设置为true来发送她的起源证据，即使她已经联系了TTP并且应该停止。与pa eoo一起，恶意Alice仍然可以选择发送正确的散列密钥hk或不正确的散列密钥hke。类似地，步骤（2）指定Alice可以在她想要的任何时候发送她的密钥如果变量k为真，则表示发送了正确的密钥。否则，它表示Alice没有发送任何密钥或发送的密钥是错误的。此外，步骤（3）和（4）建模为只要Alice已经接收到足够的消息，她就可以联系TTP以中止或恢复，但是她不将A联系T设置为真。最后两个步骤描述了Alice从TTP接收到EORM或中止令牌时的情况。清单2：为扩展的CEM协议以类似的方式，我们可以对鲍勃的不诚实行为进行建模。名单3模拟了TTP的相应行为。TTP是一个特殊的参与者，必须以特定的方式进行建模。 它必须是客观的，不能与协议参与者合谋我们建立TTP模型，60Z. Liu等人理论计算机科学电子笔记274（2011）51--（一）如果TTP接收中止请求从Alice[]A_abort_req（T_stateAB=abrt）~T_response_A- ->- T_abort_send_AT_response_A[]A_abort_req（T_stateAB=empty）~T_response_A- ->- T_abort_send_AT_response_A[]A_abort_req&（T_stateAB = recov）&~ T_response_A- ->- T_recovery_send_A--（二）如果TTP接收恢复请求从Alice[]A_recovery_req（T_state =empty）~T_response_A->->T_stateA BT_recovery_send_B[]A_recovery_req&（T_state= recov）&~ T_response_A->- ->- T_recovery_send_AT_response_A[]A_recovery_req&（T_state= abrt）&~ T_response_A->- ->- T_abort_send_A--（三）如果TTP接收恢复请求从鲍勃[]B_recovery_req（T_state =empty）~T_response_B->->T_stateA BT_recovery_send_B[]B恢复请求&（T_state= recov）&~ T_response_B->- ->- T_recovery_send_AT_response_B[]B恢复请求&（T_state= abrt）&~ T_response_B->->T_abort_send_A：=true;T_abort_send_B遵守规定对于每个协议回合，我们使用变量TstateAB来记录协议的状态。TstateAB有三个可能的值，分别是abrt、recov和empty，分别表示中止、恢复和空状态。在收到恢复或中止请求后，TTP将根据这些值进行操作T状态AB。第一部分描述了TTP如何处理来自发起者Alice的中止请求。 如果状态为空或abrt ， 则 TTP 向 Alice 和 Bob 发 送 中 止 令 牌 ， 并 且 如 果 原 始 状 态 为 空 ， 则 TstateAB也需要设置为abrt。然而，如果T stateAB是recov，这意味着对应的回合已经被恢复，则对应的EORM和密钥必须分别发送给Alice和Bob。第二部分和第三部分对处理来自Alice和Bob的恢复请求的行为进行建模。如果TTP接收到恢复请求并且其状态为空或恢复，则必须分别向Alice和Bob发送所否则，将发送中止令牌清单3：扩展CEM协议4.2在ATL给定一个只有两个参与者Alice和Bob的CEM协议，以下表达式适用于诚实的参与者，即使另一个参与者不诚实。实际上，我们只关心诚实参与者的公平性和及时性。至于有效性，它要求双方都必须诚实行事E.效率。如果诚实的参与者愿意用电子邮件交换收据，那么协议将在Alice已经获得EOR并且Bob已经接收到EOO和M而没有TTP的参与的状态下终止。有效性评估（评估Pa H，Pb H评估Q（EOO评估M评估EOR））Z. Liu等人理论计算机科学电子笔记274（2011）5161其中Pa H和Pb H表示诚实参与者Alice和Bob，并且EOR表示来自接收者Bob的接收证据。此外，EOO和M表示来源证据和来自Alice的电子邮件内容很准时。 在任何时候，诚实的参与者都有一个策略来停止协议，从而防止无休止的等待。Alice和Bob的时间间隔被公式化为：及时性P a停止□（及时性P a H停止QP a停止）及时性P b停止□（及时性P b H停止QP b停止）。其中Pa H和Pb H表示诚实的Alice和Bob，Pa stop（Pb stop）表示Alice（Bob）已经终止了协议。公平。如果满足以下条件，则协议对诚实的Alice P a是公平的：无论何时Bob获得P a的不可否认来源证据（EOO）和电子邮件内容M，P a H都有策略来获得Bob的不可否认接收证据（EOR）。在ATL中，诚实的Alice的公平性可以被公式化为：公平性P aH□（（EOO M）公平性P a HQ（EOR））。同样，Bob的公平性公式如下。如果Alice获得Pb H公平性P b H□（（EOR）公平性P b HQ（EOOM））。4.3分析结合上述公式，我们建立了三个Mocha模型：Pa HPbHTTP、PaHPb HTTP和PaH PbHTTP，以验证我们的CEM协议的公平性、及时性和有效性。这些属性已在Mocha中成功检查。5在μCRL中验证协议在这一节中，我们只简要介绍如何在μCRL中对协议进行建模，并重点介绍如何在μCRL中检查协议的TTP透明性。详细的模型和分析见[14]。5.1μCRL协议建模如第5节所述，每个μCRL规范由两部分组成，分别是抽象数据类型定义和参与者的行为规范。由于协议的执行主要依赖于消息的交换，因此没有详细处理数据的内容，而是捕获所使用的数据类型和相应的操作。因此，我们可以简化复杂的密码原语，如加密，解密和可验证加密的消息。TTP透明度是指最终证据并不能揭示TTP是否干预了协议。检查TTP透明度62Z. Liu等人理论计算机科学电子笔记274（2011）51ΣΣ在隐藏所有不必要的动作（例如TTP和用户之间的消息）以及最小化生成的状态空间模弱迹等价之后，比较从三个不同模型获得的迹。这三种模型分别是诚实的Alice和诚实的Bob、诚实的Alice和恶意的Bob和TTP以及恶意的Alice和诚实的Bob和TTP的组合。参与者通过沟通渠道联系起来。根据我们的假设，通信信道是弹性的，在这个意义上，每个消息都保证最终到达目的地。因此，通过使用μCRL中的操作和通信操作符，我们能够强制参与者Alice、Bob和TTP的动作进行同步。每个参与者都被定义为一个过程。它们之间的通信由发送和接收消息的动作组成。参与者的诚实和不诚实行为与摩卡模型中的行为相似。例如，在具有参数密钥的过程中对发起者Alice的行为进行建模，该过程通过向接收者Bob发送起源EOO的证据来发起CEM协议。动作init Alice（x，y，i，A，B）示出Alice初始化用于使用密钥x向Bob递送电子邮件y的协议回合i。然后，在收到来自鲍勃的可验证加密消息后，诚实的爱丽丝将发送她的密钥。如果Bob 动作证据Alice（x，y，i，halffetch，eetch，A，B）报告她已经获得了发送具有密钥x的电子邮件y的协议回合i的事件。爱丽丝的行为简述Alice（x：Key）= y：Itemi：Number initSend（A，eoo，B）. 初始化A（A，y，x，i，B）recv（B，halfefeetamine，A）. send（A，k，B）.recv（B，each，A）. 证据A（A，y，x，i，each，B）其中Eoo表示用于协议轮i的第一消息1ex。半签名和半签名代表Bob的可验证加密签名和最终签名。当考虑TTP时，我们需要扩展上述过程，以涵盖Alice何时类似地，诚实的Bod、不诚实的Alice、不诚实的Bob和TTP也可以在μCRL中建模，方法是如前所述指定它们的行为。5.2分析我们检验TTP透明性的方法是通过比较只有诚实参与者的系统和包含不诚实参与者的系统的证据获取轨迹。在隐藏了一些动作并简化了模型之后，我们从图1（a）中描绘的诚实系统中获得了一个轨迹，它显示了在没有TTP的情况下获得证据的情况。图1（b）描述了从包含诚实的Alice、不诚实的Bob和TTP的模型获得的迹我们可以发现，图1（b）还有一条迹线。两种痕迹的证据形式相同，但获得的顺序不同Z. Liu等人理论计算机科学电子笔记274（2011）5163evidence_A（A，m，eoo，k1，B）evidence_B（B，m，eoo，k1，A）evidence_A（A，m，each，k2，B）evidence_A（A，m，eoo，k1，B）evidence_A（A，m，eoo，k1，B）evidence_B（B，m，eoo，k1，A）evidence_B（B，m，eoo，k1，A）evidence_A（A，m，eoo，k1，B）evidence_B（B，m，eoo，k2，A）evidence_B（B，m，eoo，k1，A）evidence_B（B，m，eoo，k1，A）evidence_A（A，m，eoo，k1，B）initCom（A，m，eoo，one，k1，B）initCom（A，m，eoo，k1，B）initCom（A，m，eoo，k1，B）initCom（A，m，eoo，k2，B）（一）（b）第（1）款（c）第（1）款Fig. 1. 获得的痕迹。他们是不同的。然而，这种差异并不影响TTP透明性的正确性。在检验Bob和Alice拥有的证据时，唯一重要的是证据的内容，而由于协议模型的复杂性，转换次数（可能反映执行时间）无关紧要。图1（c）描绘了从包含不诚实的Alice、诚实的Bob和TTP的模型中获得的轨迹。我们可以发现这个图比图1（b）多一条迹线。这个额外的跟踪描述了Alice然而，这一痕迹的出现表明，在没有TTP干预的情况下，Alice和Bob都得到了他们期望的证据。如果Alice或Bob试图联系TTP进行恢复，他们将只获得错误消息而不是证据。因此，该痕迹并未揭示TTP的参与。通过以上分析，我们可以得出结论，我们的扩展CEM协议满足TTP透明性。6相关工作人们已经认识到，形式化验证对于安全协议是重要的，因为安全规则的严重性。 在本文中，我们使用的技术模型检查自动检查CEM协议的给定模型是否满足某些给定规范。据我们所知，CEM协议的形式验证文献包括Kremer等人的作品。[13]，Cederquist等人。[8]阿巴迪和布兰切特[1]。Kremer等人。[13]提出了一种使用模型检查器Mocha对CEM pro-tools进行建模和分析的方法。 使用摩卡的好处是，用并发博弈结构对CEM协议建模，并指定属性在ATL语言中，一种带有博弈语义的时态逻辑。 因此，摩卡非常适64Z. Liu等人理论计算机科学电子笔记274（2011）51合用于检查可以用游戏语义自然解释的属性，例如公平性、及时性和有效性。出于类似的原因，摩卡一直被Z. Liu等人理论计算机科学电子笔记274（2011）5165用于其他公平交换协议[10，23]。除了Mocha之外，μCRL工具集以及作为后端的CADP也用于自动分析CEM协议。Cederquist等人[8]设计了一个乐观的CEM协议，并使用μCRL工具集检查安全性和活性属性。所需的属性使用μ演算指定。存在另一种检查CEM协议的方法，该方法由Abadi和Blanchet [1]提出他们的协议是使用应用的pi演算指定的。以协议规范作为输入语言，验证器ProVerif自动检查属性保密性。至于公平性，它不是完全自动检查的，而是通过一些人工证明。7结论我们已经正式验证了该协议[15]，这是Cederquist等人基于密钥链的CEM协议[9]的扩展。核查分两步进行。首先，我们使用模型检查器Mocha检查了公平性、效率和及时性。在此基础上，我们用进程代数语言μCRL对该协议进行了建模，并使用μ CRL的工具集和CADP对TTP透明性进行了检验。分析表明，该协议达到了设计目标。本文提出的TTP透明性的形式化方法从底层的密码技术和攻击者的能力中抽象了很多东西。在未来，我们希望研究一种更合适的方法，例如，有趣的是，我们是否可以在应用的pi演算中使用静态等价来解释TTP透明性[2]。另一个方向是进一步扩展协议，以覆盖其他设计目标，如无状态TTP和问责制。引用[1] Abadi，M.和B. Blanchet，Computer-assisted Verification of a Protocol for Certified Email Protocol，Science of Computer Programming58（2005），pp.3-27号。[2] Abadi， M.和 C. Fournet， Mobile values， new names， and secure communication， in ： Proc. 28thSymposium on Principles of Programming Languages（POPL）（2001），pp.104-115[3]巴尔河，T. A. Henzinger和O.李文，交替时间时序逻辑，北京：计算机科学出版社，2001（2002），pp. 672-713[4] 巴 尔 河 ， T. A. Henzinger ， F.Y. C. Mang ， S.Qadeer ， S.K. Rajamani 和 S.Tasiran ， Mocha ：Modularity in model checking ， in ： Proc. 10th International Conference on Computer AidedVerification（CAV），LNCS1427（1998），pp.521-525[5] Asokan，N.，M. Waidner和M. Schunter，Optimistic protocols for fair exchange，in：Proc. 4th ACMconference on Computer and Communications Security（CCS）（1997），pp.7比17[6] Blom，S.C. C.的方法，J. R. 卡拉梅湾Lisser，S.M. Orzan，J.Pang，J.C. van de Pol，M.托拉比·达什蒂和A. J. Wijs，使用μCRL进行分布式分析：案例研究概要，载于：第13届会议论文集关于系统构建和分析的工具和算法（TACAS），LNCS 4424（2007），pp. 683-689[7] Blom，S. C. C.的方法，W. J. Fokkink，J. F.格鲁特岛A. van Langevelde，B.利瑟和J. C. van de Pol，DμCRL ： A tool set for analyzing algebr