认证邮件协议论文：认证邮件协议密钥链可信第三方透明性形式化验证

1、认证邮件协议论文：认证邮件协议密钥链可信第三方透明性形式化验证【中文摘要】随着电子商务的发展，认证邮件协议作为一种能够使协议的参与方都满足公平性的邮件协议，越来越受到人们的关注。认证邮件协议是公平交换协议的一种，它是指一个发送方需要将邮件的内容与接收方收到邮件的证据进行公平交换的协议。本论文首先研究了Cerderquist等人提出的基于密钥链的认证邮件协议，该协议采用密钥链来减少对可信第三方TTP(TrustedThirdParty)的存储要求,并满足公平性、有效性和有限等待，但是并不能满足TTP透明性。TTP透明性是指任何人都无法判断TTP是否参与过邮件协议的执行过程，因此能保护TTP免于恶

2、意曝光。鉴于TTP透明性在安全的认证邮件协议中的重要性，本课题采用一种基于双线性对的可验证加密签名机制将该协议进行扩展，使其在满足原有属性的基础上，能够满足可信第三方透明性。实验结果表明，扩展后的协议是满足属性最多，并且最高效的认证邮件协议之一。为了验证上述扩展协议的正确性，本课题采用了形式化验证方法对协议进行属性验证。形式化验证是指能够利用某一工具来自动的检测某一系统的模型是否能够满足所需属性的技术。该方法具有自动检测功能，因此检测比较全面，但是对系统建模和属性描述的精确性及技巧性要求极高。在验证扩展认证邮件协议的过程中，本课题首先选用模型检测工具Mocha来完成对公平性、有效性和有限等待这

3、三种属性的形式化验证。Mocha允许的输入协议模型使用守卫命令语言来描述，需要检验的属性也均用转换时态逻辑ATL来描述。利用Mocha所建立的协议模型具有博弈属性，其参与方被模拟成不同的玩家，并且协议的属性也是用具有博弈性的语义逻辑来描述，因此，利用Mocha对认证邮件协议进行验证的过程就相当于博弈论中对获胜战略的计算过程。该方法能比较好的验证邮件协议是否满足公平性、有限等待和有效性。此外，对于可信第三方的透明性验证，本文的主要思路采用一种代数形式的语言11CRL来为协议建模，并在CADf工具的支持下得到获取证据的路径踪迹，然后进行比较。通过对这些路径踪迹的比较，最终得到了对透明性的验证结果。

4、形式化验证的结果表明，本文所扩展的认证邮件协议完全满足公平性、有效性、有限等待和可信第三方透明性。【英文摘要】Withthedevelopmentofelectronicbusiness,certifiedemail(CEM)protocolisgettingmoreandmoreattention.CEMprotocoliskindoffair-exchangeprotocol,whichallowstwomutuallymistrustingpartiestoexchangeanelectronicmessagewiththehelpofevidences.Itissupposedtogu

5、aranteefairnesswithrespecttonon-repudiableevidenee,i.e.,itisundesirablethatattheendoftheprotocol,onlyoneofthetwopartiesgetsallthatheexpects.Ourstartingpointisanoptimisticcertifiedemailprotocol,whichisproposedbyCederquistetal.Thecrucialpointoftheprotocolisthatitemployskeychainstoreducethestoragerequi

6、rementofthetrustedthirdparty.WeextendtheirprotocoltosatisfyonemorepropertyofTTP(trustedthirdparty)transparency,usinganexistingverifiablyencryptedsignatureschemebasedonbilinearpairings.Weareabletoshow,byadetailedcomparison,thatourextendedprotocolisoneofthemostefficientcertifiedemailprotocolssatisfyin

7、gstrongfairness,timeliness,effectivenessandTTPtransparency.Afterthat,weanalyzetheextendedprotocolusingthetechniqueofautomaticformalverification.Formalverificationisatechniquetocheckautomaticallywhetheragivespecificationofsystemsatisfiesthespecificationofproperties.Thefinite-statemodelcheckerMochaisa

8、doptedtoverifythepropertiesoffairness,timelinessandeffectivenesswhichcanbenaturallyinterpretedinalternating-timetemporallogic(ATL)formulaswithgamesemantics.ThemodelfortheextendedCEMprotocolisbuiltusingtheguardedcommandIanguagewithconcurrentgamestructures.TheverificationofpropertiesexpressedinATLformulascorrespondstothecomputationofwinningstrategies.Besides,astohowtoanalyzethepropertyofTTPtransparency,anothertoo