可证明安全性自动化证明方法研究

Researches on Automatic Approach of Provable Security

可证明安全性是密码协议安全性评估的重要依据,但手写安全性证明容易出错且正确性难以判定。该文论述了基于游戏(Game based)转换的安全性证明及其自动化实现方法,重点论述了基于进程演算的自动化证明方法,并以该方法研究OAEP+的自动化安全性证明,首次给出了其初始游戏和相关的观察等价式。

Probable security is an important criteria for analyzing the security of cryptographic protocols. However, writing and verifying proofs with hand are prone to errors. This paper introduces the game-based approach of writing security proofs and its automatic technique. It advocates the automatic security proof approach based on process calculus, makes researches on the automatic security proof of OAEP＋, and presents it s initial game and observational equivalences for the first time.