CRII: SaTC: Towards Stronger and Verified Security for Real-World Cryptography

许多现实世界的密码方案都基于可证明安全范例，通过一些证明来证明它们的安全性。然而，在一些重要的环境中，现有的关于使用中结构的证明给出了弱的安全边界，甚至到了这些结果没有意义的程度。此外，文献中的许多证明都是错误的，给了人们对建筑安全的错误信心，而实际上建筑是脆弱的。更糟糕的是，实践者可能会在安全方案中引入看似无害的优化，但后来才发现这些优化完全破坏了这些方案的安全性。该项目旨在从以下几个方面部分解决这些问题：(1)提高重要应用的安全保障；(2)通过设计攻击来剔除现实世界协议的不安全优化；(3)开发密码证明自动验证工具。这项工作针对的是一些国家标准以及其他广泛使用的建筑。该研究还研究了如何在已发现的漏洞得到适当修复的情况下提供有意义的可证明安全保证。此外，该研究回顾了当前从随机源中提取高质量随机性的方法，目的是提高安全性和效率。这是密码学中的一个基本问题，因为许多密码学场景都严重依赖随机性的使用。最后，这项研究调查了如何改进当前自动验证加密证明的方法。这一裁决反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Many real-world cryptographic schemes are based on the provable-security paradigm, certifying their security via some proof. However, in several important settings, existing proofs for the in-use constructions give weak security bounds, even to the extent that these results are not meaningful. Moreover, many proofs in the literature are buggy, giving false confidence on the security of constructions which are in fact vulnerable. Even worse, practitioners may introduce seemingly harmless optimizations into a secure scheme, only to find out later that these optimizations completely undermine the security of these schemes. This project aims to partially address these issues from several fronts: (1) improving security guarantees of important applications, (2) weeding out insecure optimizations of real-world protocols by devising attacks, and (3) developing tools for automatic verification of cryptographic proofs.This research aims to develop some message-recovery attacks on real-world format-preserving encryption schemes, which are widely used for encrypting credit-card numbers. The work targets some national standards as well as other constructions that are widely used. The research also studies how to provide meaningful provable security guarantees assuming that the discovered weaknesses are fixed properly. Furthermore, the research revisits the current approach for extracting high-quality randomness from random sources, with the goal to improve both security and efficiency. This is a fundamental problem in cryptography, as many cryptographic scenarios crucially rely on the use of randomness. Finally, the research investigates how to improve current methods of automatically verifying cryptographic proofs.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.