基于进程演算的公钥密码体制安全性自动化证明系统

Automatic Security Proving System for Public-Key Cryptosystems Based on Process Calculus

可证安全是一种通过严格证明确保密码体制安全性的形式化方法,但由于其证明结论严重依赖于证明者个人的经验和技巧,这一方法本身的可靠性受到了质疑。文章设计并实现了一套公钥密码体制安全性自动化证明系统,使用一种概率多项式时间进程演算描述可证安全模型,借助进程间的互模拟等价关系和进程约减实现基于游戏的可证安全自动化证明。系统在C语言环境下实现,已完成ElGamal加密体制和FDH签名体制在内的一系列密码体制的安全性证明测试。

Provable security is a formal method which ensures the security of public-key cryptosys- tems through rigorous proof. However, there is doubt on its reliability since the conclusions depend heavily on the experiences and skills of the method practitioner. In this paper an automatic security proving system for public-key cryptosystems is presented. The system uses a probabilistic polynomi- al-time process calculus to describe the provable security model, and performs automatic game-based proof according to the bi-simulation equivalence and reduction on process. The system has been implemented in C language and tested on a number of examples including Elgamal encryption and FDH signature scheme.