A Framework for the Cryptographic Verification of Java-Like Programs
The authors consider the problem of establishing cryptographic guarantees - in particular, computational indistinguishability - for Java or Java-like programs that use cryptography. For this purpose, they propose a general framework that enables existing program analysis tools that can check (standard) non-interference properties of Java programs to establish cryptographic security guarantees, even if the tools a priori cannot deal with cryptography. The approach that they take is new and combines techniques from program analysis and simulation-based security. Their framework is stated and proved for a Java-like language that comprises a rich fragment of Java. The general idea of their approach should, however, be applicable also to other practical programming languages.