Enhancing Security Through Improved Cryptographic Reductions

Most modern cryptographic constructions are accompanied by a proof of security, in which the difficulty of violating the security of the construction (e.g., distinguishing ciphertexts for an encryption scheme) is reduced to the difficulty of solving a certain algebraic problem. Cryptographic proofs of security - also called reductions - thus lie at the heart of provable security, yet writing and verifying cryptographic reductions is currently a time-intensive and manual process, with most reductions highly individualised for a specific primitive or algebraic setting. By identifying proof techniques common to many settings, the landscape of both reductions and the hardness assumptions that constructions rely on for security can be vastly simplified.

In a previous project, we demonstrated that certain proof techniques could also be applied outside of the settings for which they were originally intended, and moreover could be applied to show the equivalence of certain ad-hoc assumptions and more well-established assumptions. Thus, rather than avoid ad-hoc assumptions by providing new constructions or writing new reductions, we demonstrated that the security of a variety of existing constructions - which had relied previously on these ad-hoc assumptions for security - could now be considered secure under a milder assumption.

In this work, we will formalise techniques that are common across different proofs in a fashion that makes them easier to reuse, verify, and apply to new settings. This will not only make reductions easier to both write and understand, but also expand the applicability of useful proof techniques.

The motivation for this research proposal largely stems from a collaboration with researchers at Microsoft Research Redmond, and it will be conducted in close collaboration with two particular members of Microsoft Research. This collaboration will ensure that the scope of the project remains relevant to the technology sector and that the project stays close to its goal of ultimately impacting the deployment of secure systems. The main avenue for achieving this goal is to visit companies, give invited talks on the research, and host a workshop at the end of the project to present the more practical findings of the research programme.

Over the longer term, the findings of this research programme could impact not only which cryptographic constructions are deployed in secure systems, but also which ones are endorsed by government entities such as national standards bodies, by allowing them to consider the quality of the underlying security reduction as a criterion for selection. The main avenue for achieving this goal is visits and discussions with government entities and standards bodies - both within the UK and internationally - as well as a workshop held at the end of the project.

Eventually, the goal of this project is to create stronger guarantees for the end users of secure systems; i.e., to assure users that the level of security they expect a system to provide is in fact being met. The main avenue for doing this is via interaction with stakeholders in the technology industry and the government, which will ultimately ensure that (1) the technology being used has the strongest possible security guarantees and (2) the cryptographic technologies that governments endorse and standardise are the ones most likely to withstand attacks and abuses going forward. Both of these avenues, along with advertisements via the PI's website, public seminars held at UCL, and scientific articles will also serve to increase awareness of these issues for the general public.