Affordable Access

A Framework for Automated Security Proof and its Application to OAEP

Publication Date
  • Provable Security
  • Automated Security Proof
  • Oaep
  • Ind-Cca2
  • Partial-Domain One-Wayness


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.

There are no comments yet on this publication. Be the first to share your thoughts.