安全协议的形式化需求及验证

• 作者: 刘怡文 李伟琴
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: BAN逻辑 模型检查 NRL FDR SMV 定理证明
• 年，卷（期）: 2002,（17）
• 所属期刊栏目: 学术探讨
• 页码范围: 125-128
• 页数: 4页
• 分类号: TP391.08
• 字数: 4795字
• 语种: 中文
• DOI: 10.3321/j.issn:1002-8331.2002.17.043

摘要

该文采用近世代数和时序逻辑的方法提出并描述了密码协议的形式化安全需求,并在AT模型的基础上加入信任和知识的非单调逻辑,建立了安全协议的计算模型.利用该计算模型对Denning-Sacco公钥协议进行了验证,发现了对此协议的重放攻击,并对协议进行了修改.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘怡文		7	84	4.0	7.0
2	李伟琴		37	324	9.0	17.0