Biblio

Computer-aided cryptography increases the rigour of cryptographic proofs by mechanizing their verification. Existing tools focus mainly on game-based proofs, and efforts to formalize composable frameworks such as Universal Composability have met with limited success. In this paper, we formalize an instance of Constructive Cryptography, a generic theory allowing for clean, composable cryptographic security statements. Namely, we extend CryptHOL, a framework for game-based proofs, with an abstract model of Random Systems and provide proof rules for their equality and composition. We formalize security as a special kind of system construction in which a complex system is built from simpler ones. As a simple case study, we formalize the construction of an information-theoretically secure channel from a key, a random function, and an insecure channel.

Motivated by the complexity of cryptographic proofs, we propose methods to automate the construction and verification of cryptographic proofs in the standard model. Proofs in the standard model (as opposed to the random oracle model) are the gold standard of cryptographic proofs, and most cryptographic protocols strive to achieve them. The burgeoning complexity of cryptographic proofs implies that such proofs are prone to errors, and are hard to write, much less verify. In this paper, we propose techniques to generate automated proofs for attribute-based encryption schemes in the standard model, building upon a prototype tool, AutoG&P due to Barthe et al. In doing so, we significantly expand the scope of AutoG&P to support a rich set of data types such as multi-dimensional arrays, and constructs commonly used in cryptographic protocols such as monotone-access structures, and linear secret-sharing schemes. We also provide support for a extended class of pairing-based assumptions. We demonstrate the usefulness of our extensions by giving automated proofs of the Lewko et al. attribute-based encryption scheme, and the Waters' ciphertext-policy attribute-based encryption scheme.

This paper proposes two adaptive Huffman coding hash tree algorithms to construct the hash tree of a file system. The algorithms are used to design the real-time proof of violation (PoV) scheme for the cloud storage service to achieve mutual non-repudiation between the user and the service provider. The PoV scheme can then generate cryptographic proofs once the service-level agreement (SLA) is violated. Based on adaptive Huffman coding, the proposed algorithms add hash tree nodes dynamically when a file is accessed for the first time. Every node keeps a count to reflect the frequency of occurrence of the associated file, and all nodes' counts and the tree structure are adjusted on-the-fly for every file access. This can significantly reduce the memory and computation overheads required by the PoV scheme. The file access patterns of the NCUCCWiki and the SNIA IOTTA datasets are used to evaluate the performance of the proposed algorithms. The algorithms are also compared with a related hash tree construction algorithm used in a PoV scheme, named ERA, to show their superiority in performance.