User Tools

Site Tools

A Framework for the Cryptographic Verification of Java-like Programs (BibTeX)

  author      = {Ralf K{\"u}sters and Tomasz Truderung and J{\"u}rgen Graf},
  title       = {{A Framework for the Cryptographic Verification of Java-like Programs}},
  year        = 2012,
  booktitle   = {IEEE Computer Security Foundations Symposium, CSF 2012},
  publisher   = {IEEE Computer Society},
  pages       = {198-212},
  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) non-interference 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 non-interference 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.},