公钥加密体制自动化安全性证明方法研究  

Research on Automated Security Proof of Public-Key Encryption Scheme

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

机构地区：[1]信息工程大学信息工程学院,河南郑州450002

出　　处：《信息工程大学学报》2010年第4期472-476,492,共6页Journal of Information Engineering University

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

摘　　要：可证明安全是目前分析密码协议安全性的一种重要方法,但是手工证明的难度较大,正确性也难以保证。利用计算机技术实现可证明安全性的自动化分析是目前的一个研究热点。文章在前人工作的基础上,设计了一个适用于更多密码协议的安全性证明的自动化证明工具。着重介绍了利用高级描述语言来描述的输入文件即"初始攻击游戏"的结构,并以带Hash的E lGamal加密体制为例,利用证明工具,实现了其安全性的自动化证明。Provable security is one of important techniques for analyzing the security of cryptographic protocols,while manual proof is difficult and hard to estimate.Automatic proof with the help of computers is a hotspot now.This paper designs a tool which can satisfy much more cryptographic protocols for the automatic proof.It also introduces the framework of the initial attack game and gaves an example.By using the pioposed tool,the semantic security of the hashed version of ElGamal encryption scheme is proved.

关 键 词：可证明安全 自动化 攻击游戏 ElGamal加密体制 

分 类 号：TN918.1[电子电信—通信与信息系统]