摘要
借助形式化的方法或工具分析安全协议是非常必要而且行之有效的.进程演算具有强大的描述能力和严格的语义,能够精确刻画安全协议中各个参与者之间的交互行为.作者以进程演算为基础,嵌入消息推理系统以弥补进程演算固有的缺乏数据结构支持的特点,尝试地提出了一个基于可达关系的安全协议保密性分析模型.基于此模型,形式化地描述了安全协议的保密性,证明了一定限制条件下的可判定性.并且以TMN协议为例,给出了该模型的实例研究.
The analysis and verification of security protocols are very important techniques to guarantee the security properties and the application requirements. Formal methods and automated tools are both necessary and efficient for these purposes. Security protocols are typical dis tributed concurrent systems, while process calculus is a powerful tool to model distributed concurrent systems. With strong ability of description and formal semantics, process calculus can precisely characterize the interaction between different participants of a security protocol. However, it inherently lack support of data structure. So the authors add a message inference system into process calculus. In this paper, a formal model is proposed for the secrecy analysis of security protocols based on process calculus with message inference. Using this model, the authors define two concepts, one-step reachability and multi-step reachability. Secrecy property can be formally defined and analyzed based on these teachability relations. By a case of study, the authors analyze the TMN protocol in the model. At last, the future direction to perfect the model is pointed.
出处
《计算机学报》
EI
CSCD
北大核心
2007年第2期255-261,共7页
Chinese Journal of Computers
基金
国家杰出青年科学基金(60225012)
国家"九七三"重点基础研究发展规基金(2003CB317005)
国家自然科学基金(60473006)资助
关键词
安全协议
可达关系
进程演算
消息推理
security protocol
reachability relation
process calculus
message inference
