时间敏感的安全协议建模与验证_研究综述

《时间敏感的安全协议建模与验证_研究综述》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、万方数据第36卷第8期计算机科学V01．36No．8；QQ!生§旦≤查翌巳坠!宝!兰￡i宝翌￡曼垒坚g!QQ!时间敏感的安全协议建模与验证：研究综述周倜1李舟军2王志勇3王巾盈4(国防科技大学计算机学院长沙410073)1(北京航空航天大学计算机学院北京100083)2(空军雷达学院基础部)3(北京跟踪与通信技术研究所北京100094)4摘要安全协议用于实现开放互连网的通讯安全，时间戳可以保证协议传榆消息时的新鲜性。但目前对含有时间特性的协议的研究还很不成熟，还没有有效的方法来验证带时间戳的安全协议。这使得一些大规模复杂协议的安全性质无法通过形式

2、化方法进行全面的验证。详细说明了时间戳的起因和研究时间戳的原因；详细介绍了国际上时间戳特性的几种主流研究方法——MSR方法、归纳法、CSP方法和BAN逻辑在时间敏感安全协议验证方面的工作，对它们的优缺点进行了评述，并指出了进一步的研究方向。关键词安全协议，形式化验证，时间模型，时间戳中图法分类号TP309文献标识码ASurveyOilModellingandVerificationofTimeSensitiveSecurityProtocolZHOUTilLIZho州un2WANGZhi-yon93wANGJin-yin94(SchoolofCo

3、mputerScience，NationalUniversityofDefenceTechnology，Changsha410073，China)1(SchoolofComputerScienceandEngineering，BeijingUniversityofAeronauticsandAstronautics，Beijing100083，China)2(BasicCourseDepartment，RadarAcademy0fAirForce)3(BeijingInstituteofTrackingandCommunicationsTechn

4、olngy，Beijing100094，China)‘AbstractSecurityprotocolsareusedtoprovideSecurecommunicationoveropennetwork．Time-stampcanmakesurethefreshnessofthemessageintheprotocol，butitisnotenoughtOresearchthetimesensitiveprotocols，andtherearenoeffectivemethodsthatCanverifytheseprotocols．Soit’

5、Sverydifficulttoverifyallaspectsofthosehugeandcomplexprotocolsinformalways．Thispaperdescribedwhyusingtime-stampandresearchingit，anddiscussedseveralpopularmethodsinthisfieldwhichareMSRmethod，inductionmethod，CSPmethodandBANlogicmethodinverificationoftimesensitivesecurityprotoco

6、ls．Thispapergaveouttheirestimations．Finallywealsostatedthepossiblenewdirec—tionsoftimesensitivesecurityprotocolsverification．KeywordsSecurityprotocols，Formalverification，Timedmodel，Time-stamp1引言在过去的几十年里，网络和分布式系统的发展为各类组织与用户提供了更多的交流与服务，也使资源的利用率进一步得到了提高。为了从系统中获益，参与者必须按一定方式证明自己的身

7、份，这就产生了协议。协议是指两个或者两个以上的参与者为完成某特定任务而相互约定的步骤和规则。安全协议是指在网络环境中完成主体身份认证和密钥分发等任务的具有安全功能的协议。由于网络上参与者们只能靠发送、接受消息来判断对方的身份，这就使得网络上的身份认证、数据保密等要求不能用现实世界中的办法来保证。安全协议使用加密技术在开放的互联网上实现密文传送、身份认证、授权等功能，它是实现安全电子商务的基本保证。但是在技术发展的同时，安全协议的安全性质也受到越来越多的挑战，不少协议相继发现了攻击，这使得人们对协议的形式化验证产生了极大的兴趣，随之产生了许多形式化

8、分析方法[·，引。同时，由于有些协议修改了一些内容(例如引入了异或算子等)，这使得它的安全性质需要重新评估。著名的Needham-Sch