基于事件逻辑的无线Mesh网络客户端认证协议的形式化分析

《基于事件逻辑的无线Mesh网络客户端认证协议的形式化分析》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、分类号______________________________密级______________________________ＵＤＣ______________________________编号______________________________硕士学位论文基于事件逻辑的无线Mesh网络客户端认证协议的形式化分析学位申请人：李娅楠学科专业：计算机软件与理论指导教师：肖美华教授答辩日期：独创性声明本人郑重声明：所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表和撰写的研究成

2、果，也不包含为获得华东交通大学或其他教育机构的学位或证书所使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。本人签名_______________日期____________关于论文使用授权的说明本人完全了解华东交通大学有关保留、使用学位论文的规定，即：学校有权保留送交论文的复印件，允许论文被查阅和借阅。学校可以公布论文的全部或部分内容，可以采用影印、缩印或其他复制手段保存论文。保密的论文在解密后遵守此规定，无保密内容。本人签名____________导师签名__________日期___________摘要基于事件逻辑的无线Me

3、sh网络客户端认证协议的形式化分析摘要安全协议保障信息资源在交互过程中的机密性、完整性及可用性。形式化方法规范密码协议的安全特性，拥有较完善的理论体系及模型。定理证明是形式化方法的一种，基于严格数学理论知识和逻辑推导，确定协议是否在合理假设下满足要验证的安全属性。事件逻辑理论是一种描述并发与分布式系统中状态迁移和算法的定理证明方法，可用于证明网络协议的安全性。本文运用事件逻辑理论分析无线Mesh网络客户端认证协议安全性，降低协议分析过程中的冗余度及复杂度，提高协议分析效率。论文主要工作如下：(1)基于事件逻辑理论，结合事件结构、事件类、公理簇以及随机数引理等，提出置换规则保

4、证协议交互用户在置换中性质的等价转换，推导出多组合信息交互、不叠加、事件匹配、去重复、去未来等性质，扩展事件逻辑理论在协议分析中的应用。(2)通过事件逻辑描述客户端与LTCA间交互协议的基本序列，对协议交互动作形式化描述。证明协议强认证性质，得出无线Mesh网络客户端与LTCA间认证协议在合理假设下是安全的。表明事件逻辑理论可以对安全协议不同身份主体间的认证性进行证明。(3)在客户端用户已得到LCA颁发的认证证书条件下，通过事件逻辑理论证明无线Mesh网络客户端间认证协议安全性，得出无线Mesh网络客户端间认证协议在合理假设下是安全的。表明事件逻辑理论不仅可以证明有线网络协

5、议安全属性，对无线网络协议的安全属性也可以论证，从而保证安全协议在信息交互过程的可靠性。(4)详述事件逻辑理论证明协议安全属性过程，通过流程图简化协议形式化证明步骤，体现事件逻辑理论的指导实用性。比较分析事件逻辑理论与其它逻辑推理方法，表明事件逻辑理论具有通用性。关键词：形式化方法，事件逻辑理论，强认证性质，无线Mesh网客户端认证协议，通用性IAbstractFORMALANALYSISOFWIRELESSMESHNETWORKCLIENTAUTHENCATIONPROTOCOLSBASEDONEVENTLOGICABSTRACTSecurityprotocolsensu

6、reconfidentiality,integrityandavailabilityofresourcesintheprocessofinteraction.Formalmethodsregulatesecurityfeaturesofcryptographicprotocolsandhaveamorecompletetheoreticalsystemandmodel.Theoremprovingisaformalmethodtodeterminewhetherprotocolsatisfiessecurityattributestobevalidatedunderreas

7、onableassumptions,basedonrigorousmathematicstheoryknowledgeandlogicalderivation.Eventlogicisatheoremprovingmethodthatdescribesstatetransitionsandalgorithmsinconcurrentanddistributedsystemsandcanbeusedtoprovesecurityofnetworkprotocols.Usingeventlogictoanalyzese