文献类型：期刊文章

作　　者：肖德琴[1] 周权[2] 张焕国[3] 刘才兴[4]

机构地区：[1]中国科学院研究生院信息安全国家重点实验室,北京100080 [2]广州大学理学院数学系信息安全研究所,广州510405 [3]武汉大学计算机学院软件工程国家重点实验室,武汉430072 [4]华南农业大学理学院计算机系,广州510642

出　　处：《计算机学报》

基　　金：国家自然科学基金 ( 199310 10 ;6 6 9730 34);中国科学院研究生院信息安全国家重点实验室课题资助

年　　份：2002

卷　　号：25

期　　号：10

起止页码：1083-1089

语　　种：中文

收录情况：BDHX、BDHX2000、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、核心刊

摘　　要：形式化方法由于其精炼、简洁和无二义性 ,逐步成为分析加密协议的一条可靠和准确的途径 ,但是加密协议的形式化分析研究目前还不够深入 ,至今仍没有统一的加密协议验证体系 .针对这一现状 ,该文从加密协议可能面临的最强大的攻击着手 ,提出了一种基于时序逻辑的加密协议描述方法 ,在该模型下 ,对协议行为、入侵者行为、安全需求等特性的描述均用时序逻辑公式表达 ,从而利用现有的统一的时序逻辑框架分析密码协议的性质 .特别地 ,作者描述和检测了一个系统入侵者不能用任何代数和逻辑的办法获得消息的实例 .通过对比 ,作者认为该方法具有形式化程度较高的特点 .

关 键 词：时序逻辑 加密协议分析  形式化方法 密码学 单钥加密系统  

分 类 号：TN918.1]