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

摘要：

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

关键词：安全协议、变量、串空间、逻辑

所属期刊栏目：33

分类号：TP391(计算技术、计算机技术)

资助基金：贵州省省长基金2005368;贵州省自然科学基金20052107

在线出版日期：2007-09-03（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：28-30