Visible to the public CRII: SaTC: Towards Stronger and Verified Security for Real-World CryptographyConflict Detection Enabled

Project Details

Performance Period

May 01, 2018 - Apr 30, 2020


Florida State University


National Science Foundation

Award Number

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.