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

Research on Automated Security Proof of Public-Key Encryption Scheme

可证明安全是目前分析密码协议安全性的一种重要方法,但是手工证明的难度较大,正确性也难以保证。利用计算机技术实现可证明安全性的自动化分析是目前的一个研究热点。文章在前人工作的基础上,设计了一个适用于更多密码协议的安全性证明的自动化证明工具。着重介绍了利用高级描述语言来描述的输入文件即"初始攻击游戏"的结构,并以带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.