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

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

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.