Paper 2012/153

A Framework for the Cryptographic Verification of Java-like Programs

Ralf Kuesters, 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.

Note: In this version we fix some typos and introduce some minor changes.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. CSF 2012
Keywords
indistinguishabilityimplementation-level analysisjava
Contact author(s)
truderung @ uni-trier de
History
2012-04-11: revised
2012-03-23: received
See all versions
Short URL
https://ia.cr/2012/153
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2012/153,
      author = {Ralf Kuesters and Tomasz Truderung and Juergen Graf},
      title = {A Framework for the Cryptographic Verification of Java-like Programs},
      howpublished = {Cryptology {ePrint} Archive, Paper 2012/153},
      year = {2012},
      url = {https://eprint.iacr.org/2012/153}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.