密码协议安全性证明系统解析器的设计与实现  

Design and implementation parser of provable security system for security protocols

作　　者：李安乐[1] 陈楠[1] 顾纯祥[1] 祝跃飞[1] 

机构地区：[1]解放军信息工程大学信息工程学院

出　　处：《计算机应用研究》2010年第9期3529-3532,共4页Application Research of Computers

基　　金：国家“863”计划资助项目(2007AA01Z471)

摘　　要：可证明安全性是密码协议安全性评估的重要依据,但手写安全性证明容易出错且正确性难以判定,利用计算机辅助构造游戏序列进而实现自动化证明是当前一种可行的方法。为此提出一种基于进程演算的密码协议形式化描述模型,定义了描述密码协议安全性证明中攻击游戏的语法规则,并借助工具LEX和YACC,设计出解析器程序,将密码协议及其安全性的形式化描述解析为自动化安全性证明系统的初始数据结构,并用实例来说明这种方法的可行性。Provable security is important in evaluating the security of protocols,while manual proof is fallible and hard to estimate. This paper proposed a formal model based on process calculus. Within this model,built an attack game sequence to automatically prove the security of protocols. Defined a set of syntax rules to describe attack games,and then designed a parse program using LEX and YACC. With this parse program,transformed the formal description of security protocols to the input data structures of the automatic security proving system. And used an example to illustrate the feasibility of this approach.

关 键 词：可证明安全 自动化 进程演算 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]