密码协议的模型检测分析研究

《密码协议的模型检测分析研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、摘要密码协议安全性分析与研究对于促进我国信息化建设以及网络安全和信息安全研究具有非常重要的意义。本文主要研究运用模型检测技术分析密码协议的理论与技术。研究成果如下：夺系统介绍了密码协议的基本概念及其安全性分析的重要意义、研究进展和现状。夺研究了模型检测技术以及由此产生的密码协议运行模式分析法。夺给出了运用模型检测工具S^fv分析密码协议的方法。夺设计了Tw密码协议，运用运行模式分析法分析TW协议，并使用SMV编程实现了Tw协议的安全性检测分析。夺在设计实现Tw协议的SMV程序的基础上，设计了两方密码协议的s埘检测的通用程序。关键词：密码协议；模型检测；协议分析；形式方法；运行模式分析法；SM

2、VAbstractAnalysisofsecudtyprotocolshasasignificancetopromotetheinformationconstructionandtheresearchofthenetworkandtheinformationsecurityinourcountry．Thisdissertationfocusesonthetheoryandthetechniqueofthemodelcheckingofthesecurityprotocols．FollowingaIcthemainresultsofthisthesis：夺Introducethebasicco

3、nception，thesignificance，theevolvementandthestateofthecryptographicprotocolsanalysis．夺Studythemethodsofmodelcheckingandrunningmodes．夺GivethemethodofmodelcheckingbyusingthesofewareofSymbolicModelVerifiertoanalysisprotoc01．◆DesigntheTWprotocol，Usetherunning-modeanalysisapproachbasedonthetwo-partycryp

4、tographicprotocolstoanalyzetheTWprotoc01．anddesignaSMVprogramtochecktheTWprotoc01．夺InthebasisoftheSMVprogramofTWprotocol，DesignthegeneralprogramofSMVtocheckthetwo-partyprotoc01．Keywords：Cryptographicprotocol：Modelchecking；Protocolanalysis；Formalmethods：Running-modeanalysisapproach；SMV第一章绪论1绪论本章主要系统

5、地介绍了密码协议的基本概念和密码协议的分类，讨论了密码协议的安全性及其设计规范，概述了密码协议模型检测技术分析密码协议安全性方法的重要意义、研究进展和现状。最后列举了本文的主要研究工作，给出了本文的内容安排。1．1密码协议的基本概念通过网络来建立计算机系统之间的安全通信并证明此通信是安全的，不仅是一个日益受到关注的学术研究领域，而且也对社会生活具有非常重要的意义。在现实生活中，人们对协议并不陌生，人们都在自觉或不自觉地使用着各种协议。例如，在处理国际事物时，国家政府之间通常要遵守某种协议；在法律上。当事人之间常常要按照规定的法律程序去处理纠纷；在打扑克、电话订货、投票或到银行存款或取款时，都

6、要遵守特定的协议。由于人们能够熟练地使用这些协议来有效地完成所要做的事情，所以很少有人去深入地考虑它们。所谓协议(Protoc01)，就是两个或两个以上的参与者为完成某项特定的任务而采取的一系列步骤。这个定义包含三层含义：第一，协议自始至终是有序的过程，每一步骤必须依此执行。在前一步没有执行完之前，后面的步骤不可能执行。第二，协议至少需要两个参与者。一个人可以通过执行一系列的步骤来完成某项任务，但它不构成协议。第三，通过执行协议必须能够完成某项任务。即使某些东西看似协议，但没有完成任何任务，也不能成为协议，只不过是浪费时间的空操作。我们把为了完成某种安全任务的协议称为安全协议。安全协议为了保

7、证安全性，在设计时必须采用密码技术。因此，我们也将安全协议称作密码协议。所以，我们可给密码协议再下一个定义：密码协议是建立在密码体制基础上的一种交互通信的协议，它运行在计算机通信网或分布式系统中，借助于密码算法来达到密钥分配、身份认证等目的。1．2密码协议分类到目前为止，还未有人对密码协议进行过详细的分类。因为将密码协议进行严格分类是很难的事情，从不同的角度出发，就有不同的分类方法。例如，根据密码协议的功能，