Paper 2014/038
Extending and Applying a Framework for the Cryptographic Verification of Java Programs.
Ralf Kuesters, Enrico Scapin, Tomasz Truderung, and Juergen Graf
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.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. Major revision. 3rd Conference on Principles of Security and Trust (POST 2014)
- Keywords
- implementation-level analysissimulation-based security
- Contact author(s)
- scapin @ uni-trier de
- History
- 2014-01-17: last of 3 revisions
- 2014-01-14: received
- See all versions
- Short URL
- https://ia.cr/2014/038
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2014/038,
author = {Ralf Kuesters and Enrico Scapin and Tomasz Truderung and Juergen Graf},
title = {Extending and Applying a Framework for the Cryptographic Verification of Java Programs.},
howpublished = {Cryptology {ePrint} Archive, Paper 2014/038},
year = {2014},
url = {https://eprint.iacr.org/2014/038}
}