International Association
for Cryptologic Research

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.