Cryptology ePrint Archive: Report 2012/153
A Framework for the Cryptographic Verification of Java-like Programs
Ralf Kuesters and Tomasz Truderung and Juergen Graf
Abstract: We consider the problem of establishing cryptographic guarantees -- in particular, computational indistinguishability -- for Java or Java-like programs that use cryptography. For this purpose, we propose a general framework that enables existing program analysis tools that can check (standard) noninterference properties of Java programs to establish cryptographic security guarantees, even if the tools a priori cannot deal with cryptography. The approach that we take is new and combines techniques from program analysis and simulation-based security. Our framework is stated and proved for a Java-like language that comprises a rich fragment of Java. The general idea of our approach should, however, be applicable also to other practical programming languages.
As a proof of concept, we use an automatic program analysis tool for checking noninterference properties of Java programs, namely the tool Joana, in order to establish computational indistinguishability for a Java program that involves clients sending encrypted messages over a network, controlled by an active adversary, to a server.
Category / Keywords: cryptographic protocols / indistinguishability, implementation-level analysis, java
Publication Info: CSF 2012
Date: received 23 Mar 2012, last revised 11 Apr 2012
Contact author: truderung at uni-trier de
Available format(s): PDF | BibTeX Citation
Note: In this version we fix some typos and introduce some minor changes.
Version: 20120411:082549 (All versions of this report)
Discussion forum: Show discussion | Start new discussion
[ Cryptology ePrint archive ]