A Framework for Automated Security Proof and its Application to OAEP

Abstract

OAEP is a widely used public-key encryption scheme based on trapdoor permutation. Its security proof has been scrutinized and amended repeatedly. In this paper we present a automatically proof for IND-CCA2 security of OAEP, which is completed by a framework for mechanized security proof, without any human intervention. The framework is built on the base of probabilistic polynomial-time process calculus, and capable of dealing with padding-based encryption schemes. We provide an overview of the proof instance and explain several crucial steps of the game transformation.