Researches on Automatic Approach of Provable Security

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 its initial game and observational equivalences for the first time.