User Tools

Site Tools

Extending and Applying a Framework for the Cryptographic Verification of Java Programs (BibTeX)

    author = {Ralf K{\"u}sters and Enrico Scapin and Tomasz Truderung and J{\"u}rgen Graf},
    title = {{Extending and Applying a Framework for the Cryptographic Verification of Java Programs}},
  institution = {Cryptology ePrint Archive, Report 2014/038},
  note = {Available at
  year = 2014,
  abstract = {In our previous work, we have proposed a framework which allows tools that can check standard noninterference properties but a priori cannot deal with cryptography to establish cryptographic indistinguishability properties, such as privacy properties, for Java programs. We refer to this framework as the CVJ framework (Cryptographic Verification of Java Programs) in this paper.  While so far the CVJ framework directly supports public-key encryption (without corruption and without a public-key  infrastructure) only, in this work we further instantiate the framework to support, among others, public-key encryption and  digital signatures, both with corruption and a public-key  infrastructure, as well as (private) symmetric encryption.  Since  these cryptographic primitives are very common in security-critical  applications, our extensions make the framework much more widely  applicable.    To illustrate the usefulness and applicability of the extensions  proposed in this paper, we apply the framework along with the tool  Joana, which allows for the fully automatic verification of  noninterference properties of Java programs, to establish  cryptographic privacy properties of a (non-trivial) cloud storage  application, where clients can store private information on a remote server.  },