基于游戏的密码协议自动化安全性证明

Provable security has become a popular approach for analyzing the security of cryptographic protocols. However, writing and verifying proofs by hand are prone to errors. This paper advocates the automatic security proof framework with sequences of games. We make slight modifications to Blanchets calculus to make it easy for parsing the initial game. The main contribution of this work is that it introduces algebraic properties with observational equivalences to automatic security proofs, and thus can deal with some practical cryptographic schemes with hard problems. We illustrate the use of algebraic properties in the framework by proving the semantic security of the ElGamal encryption scheme.