模态逻辑与带变量串空间相结合的协议分析

• 作者: 彭长根 李祥 罗文俊 龙士工
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 安全协议 变量 串空间 逻辑
• 年，卷（期）: 2007,（13）
• 所属期刊栏目: 博士论文
• 页码范围: 28-30
• 页数: 3页
• 分类号: TP391
• 字数: 4019字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2007.13.010

摘要

在传统的串空间基础上引入带变量的串空间模型,对于未确定的消息项或其子项用变量表示,允许变量出现在消息项及其演算中,协议由参与协议运行的不同主体的带变量的串组成.以协议运行的迹语义为模型,提出了一个用于推理协议主体的各种行为的模态逻辑系统,给出了该逻辑的语法、公理及推理规则.基本的模态公式表示主体A完成动作P,是相应的结果,通过主体行为的各种组合并绑定相应逻辑公式,最终推断安全协议的秘密性和可鉴别性.用该方法分析Helsinki协议,能发现其中的安全漏洞Horng-Hsu攻击.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	罗文俊	贵州大学计算机软件与理论研究所	34	192	8.0	12.0
2	彭长根	贵州大学计算机软件与理论研究所	96	449	11.0	16.0
3	李祥	贵州大学计算机软件与理论研究所	91	551	13.0	19.0
4	龙士工	贵州大学计算机软件与理论研究所	39	110	5.0	9.0