复杂安全协议的建模与验证

《复杂安全协议的建模与验证》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、川Ⅲ川IIIlI!!llJll⋯。⋯⋯川洲Y1523917分类号至￡§Q9工学博士学位论文学号Q5Q§2Q§2密级公开复杂安全协议的建模与验证博士生姓名周倜学科专业计算机科学与技术研究方向计算机软件与理论指导教师李舟军教授国防科学技术大学研究生院二oo八年十月国防科学技术大学研究生院博十学位论文的安全协议进行有效验证。为了提高抽象模型的精度，本文进一步提出了局部抽象一精化迭代验证的理论框架。局部抽象可以提高整个验证过程的验证效率，为复杂协议的验证提供了有效的途径。4．时间敏感安全协议的建模与验证。通过

2、将描述时间的事件加入到进程代数模型中，使得时间戳能方便有效地在协议模型中描述出来。将时间元素的线性约束加入到基于Horn逻辑的安全协议模型中，使得Horn逻辑模型能有效地处理时间约束信息。通过研究规则中各时间元素与消解的关系，找到了确定时间相关元素的时间先后关系的办法，提出了两阶段验证方法。一条规则是否可用，此时还需考察其所对应的约束系统是否可满足。因此，本文对该模型下的约束系统进行了研究，提出了一个高效判断其可满足性的判定算法，并证明了该算法是多项式时间算法。由于约束系统中存在大量冗余的不等式，本文

3、还深入研究了该系统，针对其本身的特性，提出了约束的抽象理论简化约束系统，该方法能有效地降低时空开销。5．设计并实现了一个高效的安全协议验证工具SPVToII。本文提出了不停机性预测和抽象一精化迭代验证框架的实现算法，在安全协议自动分析工具SPVT的基础上，结合抽象一精化迭代验证框架，设计并实现了一个自适应选择验证方法的高效的协议验证工具SPVT-II。该工具既能发现协议中可能的反例，也能尽可能地减少虚假反例的产生。6．Kerberos协议协议的分析与验证。本文通过对Kerberos协议进行分析，将公钥

4、Kerberos协议的认证服务交换阶段进行了建模，并用SPVT-II对协议模型进行了自动化的验证。实验结果表明SPVT．II能自动发现PKINIT-26中认证服务阶段的攻击。关键词：安全协议；建模；验证；反例构造；不停机性预测；抽象；精化；时间敏感；约束系统；Kerberos协议第ii页国防科学技术大学研究生院博十学位论文．ABSTRACTWiththedevelopmentofnetwork．securityproblemsintheinternetarebecomingmoreandmoreurg

5、entandimportant．Securitypropertiesencountermoreandmorechal-lenges．Securityprotocolisoneofeffectivemethodstosolvetheinternetsecurityissues．Theopeninternetwithsecurityprotocolscanrealizevarioussecurityfunctions，suchasidentityauthenticationetc．Sincepartici

6、pantsofcommunicationcannotfindtherealiden-tityofeachotherbybiometricfeaturesincomputernetwork，themutualauthenticationshouldbefoundedoncryptography．Securityprotocolisatypeofcommunicationprotocolbasedoncryptography,whichrunsoverthecomputernetworkordistrib

7、utedsystems，andarrangestheexecutionstepsandtheexecutionruleswiththecryptographicalgorithmsamongtheparticipantswhoimplementtaskssuchaskeydistribution，identityauthenti—cation，e-commercetransaction，etc．Thecorrectnessofsecurityprotocolsiscriticalforthetrans

8、actionsovertheopennetworks．However，securityprotocolsdesignedandusedintherealworlddonotalwaysachievetheirobjectives．Manyprotocolshavebeenfoundhavingflawsafteralongapplicationperiod．It’Sahotfieldinformalmethodtodesignanddevelopanef