SaTC: CORE: Small: Practice-Driven Cryptographic Theory

点击翻译按钮获取中文摘要

When users go to a popular Internet site, their browser will show a lock symbol, indicating that cryptography is being used to secure the communications. This cryptography has different components, including signature schemes and schemes for authenticated encryption. The same cryptography is also the basis of security in popular messaging apps, and used in many cryptocurrencies. Similarly, Callisto, a tool that allows victims to report sexual assault while protecting their privacy, uses a new and advanced form of cryptography called a two-party secure computation protocol, and usage of this tool is expanding. But does all this cryptography actually work, meaning provide the expected security? This question is not moot: recent years have witnessed attacks breaking widely-deployed cryptography, and this impacts millions of people. This project aims to validate existing cryptography via mathematical proofs of security, an approach that is now well accepted as reducing the likelihood of failures. The work aims to provide such proofs for widely-used signature schemes, authenticated encryption schemes and two-party secure computation protocols, increasing security assurance for the cryptography in use today. The project will likewise identify forms of cryptography that are important to future capabilities and needs, and build this next-generation cryptography, accompanying it again by proof-based validation so as to reduce the risk of future failure. The broader impacts include a software tool called PlayCrypt that will educate students in the design of high-assurance cryptography as needed in industry today. The project will also seek to broaden participation by confronting paucity of women in academia as something to be addressed early in the pipeline, not later, and focus on identifying promising women undergraduates and, through research, advancing them to PhD positions; then, working with women PhD students, advancing them to faculty positions. EdDSA is a signature scheme that is a government standard and widely used on the Internet. Existing security proofs for it, however, suffer from three limitations: they fail to prove security of the scheme that is actually in use due to improper modeling of the hash functions; the reductions underlying the proofs are so loose that the quantitative security guarantee, for the 256-but curves in which the scheme is implemented, is almost nil; the quantitative security guarantees in the multi-user setting relevant to the Internet are even worse. This project aims to fill all these gaps, by introducing the filtered Random Oracle Model and a corresponding notion of filtered indifferentiability; and a reduction from the classical Schnorr signature scheme rather than from an algebraic problem. The project will also consider authenticated encryption schemes like Galois/Counter Mode (GCM) that are currently used to encrypt data over the Internet, and explain that they fail to provide security for certain choices of nonces, a gap to be filled with a framework that allows users to pick, with confidence, nonces we show, via proofs, to result in secure encryption. The project will also show how to extend current authenticated encryption schemes to ones that commit to their key, thereby preventing certain new classes of attacks on password-based encryption, and moreover show how key-committing authenticated encryption results in secure password-based authenticated encryption. Finally, the project will revisit the foundations of two-party secure computation, giving definitions amenable to a concrete-security treatment, and giving security proofs that deliver protocols whose security is quantitatively as high as possible, leading to the best possible efficiency for a desired level of security.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.