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

Protocol Analysis of Modal Logic Combined with Strand Space with Variables

作　　者：龙士工[1] 罗文俊[1] 彭长根[1] 李祥[1] 

机构地区：[1]贵州大学计算机软件与理论研究所,贵阳550025

出　　处：《计算机工程》2007年第13期28-30,共3页Computer Engineering

基　　金：贵州省省长专项基金资助项目(2005368);贵州省自然科学基金资助项目(20052107)

摘　　要：在传统的串空间基础上引入带变量的串空间模型,对于未确定的消息项或其子项用变量表示,允许变量出现在消息项及其演算中,协议由参与协议运行的不同主体的带变量的串组成。以协议运行的迹语义为模型,提出了一个用于推理协议主体的各种行为的模态逻辑系统,给出了该逻辑的语法、公理及推理规则。基本的模态公式[P]Aφ表示主体A完成动作P,φ是相应的结果,通过主体行为的各种组合并绑定相应逻辑公式,最终推断安全协议的秘密性和可鉴别性。用该方法分析Helsinki协议,能发现其中的安全漏洞Horng-Hsu攻击。A strand space model with variables is provided based on traditional strand space, the undermined terms and subterms are expressed with variables, and the variable occurs in the message term and its calculus. The protocol consists of strands with variables belonging to different participants in the protocol running. Based on the concrete traces, the logic designed for reasoning about the principal action, consists of syntax, atoms and inference rules. The basic modal formula [P]A Ф means that the action P is finished with the result of Ф. By associating sequence of actions and attaching the formulas, it can prove the security properties of protocols such as secrecy and authentication. It analyzes Helsinki protocol through the method, and the logic leads directly to rediscovery of Horng-Hsu＇s attack.

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

分 类 号：TP391[自动化与计算机技术—计算机应用技术]