基于时序逻辑的加密协议分析

• 作者: 刘才兴 周权 张焕国 肖德琴
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 加密协议 形式化方法 时序逻辑
• 年，卷（期）: 2002,（10）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 1083-1089
• 页数: 7页
• 分类号: TP309
• 字数: 6577字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2002.10.012

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张焕国	武汉大学计算机学院软件工程国家重点实验室	244	4083	31.0	56.0
2	肖德琴	中国科学院研究生院信息安全国家重点实验室	93	894	17.0	25.0
4	刘才兴	华南农业大学理学院计算机系	37	433	13.0	19.0
5	周权	广州大学理学院数学系信息安全研究所	35	231	8.0	14.0