|
This project develops a comprehensive proof construction and verification framework for a well-defined class of cryptographic protocols: attribute-based cryptosystems. In particular, existing automated proof construction and verification frameworks, such as EasyCrypt and CryptoVerif, are extended to provide support for attribute-based cryptography. The extensions consist of libraries of simple transformations, algebraic manipulations, commonly used abstractions and constructs, and proof strategies, which will help in generation and verification of proofs in attribute-based cryptography. Additionally, the investigator seeks to understand the limitations, if any, on the development of verification tools for attribute-based cryptosystems.
The project builds upon and expands the scope of the toolset to include other classes of cryptographic protocols, such as identity-based cryptosystems, and non-interactive zero-knowledge proofs, which share the same underlying mathematical assumptions and constructs. All code and modules produced from this peoject will be compatible with existing proof verification tools. Educational activities are an integral part of this project. This project provides undergraduate and master's-level students an introduction to, and an opportunity to work on an advanced area in cryptography, and provide an opportunity to work with state-of-the-art model-checkers, and proof assistants.
|
CRII: SaTC: Automated Proof Construction and Verification for Attribute-based Cryptography