基于πt建模与约束求解的加密协议自动化验证算法及其工具的实现与研究

《基于πt建模与约束求解的加密协议自动化验证算法及其工具的实现与研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、ResearchonCryptographicProtocolAutomatedCheckingAlgorithmandToolRealiZationBasedon丌tModelingApproachandConstraintSolving(Ph．DDissertation)ByHanJinSupervisedbyProfessorXieJunyuanAdissertationsubmittedinpartialfulfillmentofTherequirementsforthedegreeofDoctoro

2、fPhiplosophy(ComputerSoftwareandTheory)inNanjingUniversityDepartmentofComputerScienceandTechnologyNanjingUniversity,P．R．CHINA2009直立太堂熊±途塞基王翌!建撞皇约塞壅鲤的加查垃这自动丝坠适篡洼区王县的塞现皇婴塞摘要J㈣必加密协议是信息安全的基石，加密协议能否实现用户所需的安全目标是所有加密协议设计者、使用者所关心的问题，但是加密协议的验证却是相当困难的。自从上世纪七十年代至今，加密协

3、议的验证研究已走过了三十多年的时间，形成了一批重要的研究成果，但加密协议的验证仍面临着诸多挑战。加密协议验证过程的复杂性使得大多数协议验证过程需要人工参与。随着新型加密协议的种类与应用快速增长，加密协议验证的低效率给协议的设计与应用带来了很大的限制。因此加密协议的自动化验证成为加密协议验证研究的必然趋势。本文的研究内容即是基于n‘演算建模与约束求解的方式实现对加密协议的自动化验证，具体研究内容和创新性成果如下：l、Ⅱ。演算的加密协议建模方法：该方法通过对n演算的扩展，在其中引入了类型推理规则，并对扩展后的演算

4、在类型系统安全方面做了严格的证明。通过Ⅱ‘演算，实现对加密协议的建模，既具备兀演算在并行计算建模方面所具有的严格、简洁表述的优点，又在其中引入了类型判断与推理能力。该建模方法与其它同类建模方法相比，能提供更多的加密协议分析支持，良好的扩展性。Ⅱ‘演算是本文所实现的加密协议验证工具对协议建模，代码映射与验证的基础。2、基于约束求解的加密协议验证算法：本文采用加密协议一致性目标来描述加密协议的认证性与秘密性安全属性。基于D．Y攻击者模型以及完善加密机制前提，本文得出注入攻击是D—Y攻击者实现攻击的必然手段。由于注

5、入攻击会造成被攻击会话执行受阻，因此攻击者必须在其掌握的会话数据中求解出满足协议进一步执行的会话数据。由此加密协议的验证转换成攻击者基于约束，求解目标会话数据的过程。本文算法基于攻击者由约束出发，通过拆分约束形成求解目标，并由求解过程形成求解域，从而实现对加密协议的验证。本文提出了相似会话、相似会话数据、同构求解域等概念，证明了一个成功的攻击路径参与者个数的最多为N+I，并由求解域的同构性，证明了本文算法对于规则加密协议该算法的收敛性。本文算法实现了不需要人工参与的加密协议自动化验证，与其它基于模型检测等方法

6、相比，本文算法的特点是对于规则加密协议该算法的收敛性，这使得自动化验证结果更具实用性。本文给出了相关的实验及其分析结果。3、加密协议自动化验证工具．1njectView：InjectView是本文开发的加密协议自动化验证工具，其基于丌‘演算建立的类型系统推理与判断规则，接收用户定义的协议角色会话文档及数据类型定义文档，实现加密协议模型的代码映射与自动化验证。由于InjuctView采用独立的通道模块、加／解密机制、会话状态机设计，并由定义文档实现协议模型的自动化映射，使得InjuctView具有很高的易用性与

7、自动化程度。关键词：加密协议验证Ⅱ‘演算加密协议建模约束求解自动化验证工具，InjectViewAbstractCryptographicprotocolisthebasisofInformationSecurity．Whenacryptographicprotocoltobedesignedorused，thereisalwaysaquestion：doitattainitssecurityaims?Researcheshaveprovedthatitisdifficulttoanswerthisquest

8、ion．Fromthe70‘Soflastcentury，cryptographicprotocolcheckingresearchhasbeengoneformorethanthirtyyears，andalotofimportantresultshasgotten．Buttodaycryptographicprotocolcheckingresearchisstillconfrontedwith