安全协议模型检测技术的研究与应用

《安全协议模型检测技术的研究与应用》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、安全协议模型检测技术的研究与应用摘要：安全协议的安全性是网络安全的重要基础，运用形式化方法分析安全协议的安全性己成为目前研究的主要热点。本文主要研究运用形式化技术分析安全协议的理论与技术，对基于模型检测技术的运行模式分析法进行深入的研究，并把其应用到实用安全协议的分析与设计中去。本文的主要研究内容包括：（1）系统介绍安全协议的背景和密码协议安全性分析的重要意义。概述协议形式化分析的三种思路；（2）在两方密码协议运行模式的基础上，将七种运行攻击模式简化为五种。（3）介绍基于一个可信第三方的三方密码运行模式，给出四

2、种组合形式的运行模式。（4）运用运行模式法成功分析了NS公钥协议，找出协议漏洞，并对协议进行了改进。（5）将模型检测法与其他经典形式化分析法进行比较，给出结论。关键词：安全协议；模型检测；形式化分析；运行模式分析ResearchandApplicationonModelCheckingofSecurityProtocolAbstract:Thesecurityofsecurityprotocolsisthefoundationofthenetworksecurity.Presentlytheanalysisof

3、securityofsecurityprotocolsusingtheformalmethodhasbecomeahotspotofresearch.Thisdissertationmakesaresearchonthetheoryandtechniqueoftheformalanalysisofthesecurityprotocolsandfocusesontherunning-modeanalysismethodbasedonthemodelcheckingtechnology.Furthermorethi

4、smethodisusedtoanalyzeanddesignpracticalsecurityprotocols.Theresearchesaresummarizedasfollows:Thebackgroundandsignificanceofthecryptographicprotocolsecurityanalysisareintroduced,andwealsosummarizethethreeclassificationsoftheformalanalysismethods.Weintroducet

5、herunning-modeanalysisbasedonthetwo-partysecurityprotocol,andfounditwillbesimplifiedtherunningmodesfromseventofive.Weintroducetherunning-modeanalysisbasedonthethree-partysecurityprotocolincludingonlyoneserverwhichactsasthetrustedthirdparty.Thenwefindthereare

6、fourformrunningmodeswhentheprotocolsrun.Furthermore,therunning-modeanalysisbasedonthetwo-partysecurityprotocolisusedtoanalyzeonpublic-keyprotocolofNeedham-Schroeder(NS).Thepropertieswechoosemaynotadapttothemodel,weneedtochangethemodel'sbehaviorortheverificat

7、ionparameter.Finally,wecomparethemodelcheckingwithotherformalanalysismethodsandgivetheconclusions-Keywords:securityprotocol,modelchecking,formalanalysis,running-modeanalysis第1章绪论11」安全协议的背景11.2分析安全协议的安全性的困难性11.3国内外研究现状21.4常见的安全协议形式化分析方法31.5本文的研究内容41.6本文的组织结构4

8、第2章模型检测及基于模型检测的运行模式分析法52」模型检测的基本思想及工作方式52.2模型检测技术分析协议方法62.3运行模式分析法的基本思想及其优点72.4运行模式分析法简介72.4.1分析协议的基本假设72.4.2两方安全协议的运行模式分析法简介82.4.3三方安全协议运行模式分析法9第3章运行模式分析法的运用133」NSPK协议133.2对NSPK协议的运行模式分析143.2.1