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.
Category / Keywords: cryptographic protocols / implementation-level analysis, simulation-based security Original Publication (with major differences): 3rd Conference on Principles of Security and Trust (POST 2014) Date: received 14 Jan 2014, last revised 17 Jan 2014 Contact author: scapin at uni-trier de Available format(s): PDF | BibTeX Citation Version: 20140117:100310 (All versions of this report) Short URL: ia.cr/2014/038 Discussion forum: Show discussion | Start new discussion