安全协议分析的界——综合模型检查与Strand Spaces(英文)
更新时间:2019-05-21
访问次数:
关键词:安全协议分析 模型检查 Strand Spaces 定理证明
作者单位:北京航空航天大学计算机科学与工程系,北京航空航天大学计算机科学与工程系 北京100083
,北京100083
内容提要:Strand Spaces是一种用于分析安全协议的机器证明方法.简要介绍了 Strand Spaces的基本特点,分析了其优劣,提出了构造协议的理想子环的算法,并以此来约束协议入侵者的能力和协议并行运行的次数.将模型检查与 Strand Spaces结合在一起,提出了一种综合分析方法来验证协议的安全特性,该方法可充分发挥模型检查与 Strand Spaces二者的优势.
期刊名:中国科学院研究生院学报
期号:第3期
年份:2002
页数:288-294