黑料福利网

Digital security in a changing world

Modern society relies on secure digital communication. Online banking, messaging apps, software updates, and the control of critical infrastructure need cryptography to protect sensitive information. Cryptography ensures that data remains private and that digital messages truly come from their claimed sender.

Most cryptographic systems used today are secure because they rely on mathematical problems that are extremely hard for classical computers to solve. However, this foundation has been challenged by the promise and on-going development of quantum computers, which use the principles of quantum physics to process information in fundamentally different ways. Although still under development, sufficiently powerful quantum computers could break many of the mathematical assumptions underlying current cryptographic systems.

The quantum threat

In particular, quantum algorithms such as Shor鈥檚 algorithm made it possible to efficiently solve problems like integer factorisation and discrete logarithms. These are mathematical problems that currently make systems like RSA and elliptic curve cryptography secure.

This has introduced a serious concern known as the 鈥渟tore now, decrypt later鈥� threat. This means that encrypted data that is safe today may become readable in the future once quantum computers become more widely available.

Preparing for post quantum cryptography

To prepare for this transition, researchers are now developing post-quantum cryptography. These are new types of cryptographic schemes designed to remain secure even against quantum computers. They rely on different mathematical problems 鈥� such as lattices, error correcting codes, and hash functions. These problems are believed to remain hard to solve, even for quantum computers.

However, this new generation of cryptography also introduces a challenge. Researchers need to be confident that these new schemes are truly secure. Post-quantum constructions are complex and relatively new, which increases the risk of subtle mistakes in their design, in their security arguments, or in their software implementations. History shows that even well studied cryptographic systems can contain flaws that remain unnoticed for many years.

As a result, designing secure schemes is not enough. Their correctness and security must also be verified as rigorously as possible.

Machine checked security proofs

In his PhD thesis Toward Machine-Checked Post-Quantum Cryptography, addressed this challenge by applying computer-assisted verification techniques to post-quantum cryptographic constructions. He used specialised software tools to help construct and check mathematical security proofs. This reduces the risk of human error and increases confidence in the results.

Digital signatures under formal scrutiny

A major part of Meijers鈥� work focused on digital signature schemes, which are cryptographic methods used to verify that digital messages and data are authentic and have not been tampered with.

His PhD research project examined two important post-quantum signature schemes: XMSS and SPHINCS+. Both are based on cryptographic hash functions and are considered strong candidates for secure digital signatures in a future where quantum computers could break many current cryptographic systems.

Using the EasyCrypt proof assistant, Meijers constructed fully machine-checked security proofs for these schemes. This means every step of the mathematical reasoning was formally verified by software, ensuring each conclusion logically follows from the previous ones. This provides a higher level of confidence than traditional handwritten proofs alone.

From specification to implementation

For XMSS, Meijers鈥� work went further by connecting abstract security proofs to a concrete implementation written in the Jasmin programming language.

This made it possible to verify that the actual software code matches the formal mathematical specification. In other words, not only was the theory proven to be correct, but the implementation itself was checked against that theory too.

By linking proofs directly to executable code, the gap between theory and practice was reduced, leading to what are known as end-to-end security guarantees.

Hybrid cryptographic constructions

Beyond digital signatures, Meijers also examined how different key establishment mechanisms can be securely combined.

These so-called hybrid approaches are especially important during the transition to post-quantum cryptography, a setting where classical cryptographic methods and post-quantum methods may need to be used side-by-side with post-quantum cryptography.

Hybrid constructions are designed to remain secure as long as at least one of the underlying components is still secure. This makes it possible to reduce risk during migration and provides a safer path for transitioning to new cryptographic systems.

Building better verification tools

Alongside these technical results, Meijers鈥� work led to the development of reusable tools and methods for formal verification in cryptography.

By improving the underlying infrastructure, it becomes easier for other researchers to apply similar formal verification techniques to new cryptographic systems.