Cryptography FM

Anyone who’s looked at the French civil code -- or, God forbid, the French tax code -- will tell you that it takes more than a mere human mind to decipher its meaning, given how it’s been growing and growing ever since it was established by Napoleon hundreds of years ago.

Well, Catala is a new project that takes this adage perhaps a bit too literally, by applying formal methods -- a field increasingly seen as immediately adjacent to cryptography -- on the French tax code! Catala aims to provide a “domain-specific programming language designed for deriving correct-by-construction implementations from legislative texts.” -- what that means is that you’ll be able to describe the tax code in a programming language, and get a proven-correct processing of your tax returns in that same language, too!

This episode of Cryptography FM is not directly about cryptography. Instead we’ll be covering a highly related and definitely interesting tangent: can we use the same formal methods that have recently proven the security of protocols like Signal and TLS in order to formally verify our tax returns? And, more importantly, can today’s guest help me pay less taxes?!

Joining us today is doctoral student Denis Merigoux, to talk about Catala, and more.

Links:

Music composed by Toby Fox and performed by Sean Schafianski.

Special Guest: Denis Merigoux.

Sponsored By:

• Symbolic Software: This episode is sponsored by Symbolic Software. Symbolic Software helps you bring in the experience and knowledge necessary to design, or prove secure, state-of-the-art cryptographic systems for new solutions. We've helped design and formally verify some of the world's most widely used cryptographic protocols.

Ever since its introduction in 2012, the BLAKE hash function has been reputed for achieving performance matching and even exceeding MD5 while still maintaining a high security margin.

While the original BLAKE did make it as a finalist to the NIST SHA3 competition, Keccak was ultimately selected. But this hasn’t discouraged the BLAKE team, who in January of this year, published BLAKE3, promising to be even faster than BLAKE2 thanks to a highly parallelizable design and fewer rounds.

But wait, what exactly is a parallelizable hash function? Isn't a lower round number risky? And heck, how do you even design a hash function?! Joining me today are two of the four BLAKE3 authors: Jack O’Connor and Jean-Philippe Aumasson, to discuss these questions and more.

Links and papers discussed in the show:

Music composed by Toby Fox and performed by Sean Schafianski.

Special Guests: Jack O'Connor and Jean-Philippe Aumasson.

Sponsored By:

• NSU: This episode of Cryptography FM is sponsored by NSUCRYPTO, the International Olympiad in Cryptography. NSUCrypto is the unique cryptographic Olympiad containing scientific mathematical problems for professionals, school and university students from any country. Its aim is to involve young researchers in solving curious and tough scientific problems of modern cryptography. From the very beginning, the concept of the Olympiad was not to focus on solving olympic tasks but on including unsolved research problems at the intersection of mathematics and cryptography. There were more than 1900 participants from 52 countries in the first six Olympiads!

Aside from working on a competition for standardizing post-quantum primitives, the United States National Institute of Standards and Technology, or NIST, has also organized a lightweight cryptography competition meant to attract designs for symmetric primitives, such as hash functions and authenticated encryption ciphers, that work in use cases where even AES is not an adequately speedy standard.

Among the submissions to NIST’s lightweight cryptography competition has been Gimli, a family of cryptographic primitives comprised of a hash function and of an authenticated encryption with associated data (AEAD) cipher. Named after the Lord of the Rings Dwarf warrior and authored by a long list of accomplished cryptographers, Gimli looked like a promising submission -- until a team of cryptanalysts at INRIA produced a surprising set of results outlining some potentially serious weaknesses in Gimli’s current design.

In their paper, which recently was declared as the winner of the IACR Asiacrypt 2020 Best Paper Award, Antonio Flórez Gutiérrez, Gaëtan Leurent, María Naya-Plasencia, Léo Perrin, André Schrottenloher and Ferdinand Sibleyras from the INRIA research institute here in France presented some very strong results against Gimli’s security.

But why does Gimli even matter? Why aren’t AES, ChaCha20-Poly1305, and BLAKE2 enough, even for the most performance-constrained scenarios? And how did this team of researchers succeed in obtaining such serious results on a family of cryptographic primitives that was certainly designed with care and expertise?

Links and papers discussed in the show:

Music composed by Toby Fox and performed by Sean Schafianski.

Special Guest: Léo Perrin.

Sponsored By:

• Symbolic Software: This episode is sponsored by Symbolic Software. Symbolic Software helps you bring in the experience and knowledge necessary to design, or prove secure, state-of-the-art cryptographic systems for new solutions. We've helped design and formally verify some of the world's most widely used cryptographic protocols.

TLS 1.3 has been widely praised as a major upgrade to the Transport Layer Security protocol responsible for securing the majority of Web traffic. But one area in which TLS 1.3 seems to be lacking is its potential for resistance to attacks that utilize quantum computing – computers that, theoretically, could factor the products of large primes and solve the discrete logarithm problem in relatively short periods of time, significantly affecting the security of TLS 1.3.

Today however, we’re discussing an interesting new paper, to be published at this year’s ACM CCS, which introduces KEMTLS: a modified version of TLS 1.3 that uses Key Encapsulation Mechanisms, or KEMs, instead of signatures for server authentication, thereby providing a sort of “post-quantum TLS”.

But what even are KEMs? Are quantum computers even a thing that we should be worried about? On the first ever episode of Cryptography FM, we’ll be hosting Dr. Douglas Stebila and PhD Candidate Thom Wiggers to discuss these questions and more.

Dr. Douglas Stebila is an Associate Professor of cryptography in the Department of Combinatorics & Optimization at the University of Waterloo in Waterloo, Ontario, Canada. His research focuses on improving the security of key exchange protocols and Internet cryptography protocols such as TLS and SSH, including the development of quantum-resistant solutions. His previous work on the integration of elliptic curve cryptography in TLS has been deployed on hundreds of millions of web browsers and servers worldwide.

Thom Wiggers is a PhD Candidate at the Institute of Computing and Information Sciences at Radboud University in The Netherlands. He is working on the interactions of post-quantum cryptography with protocols, under the supervision of Dr. Peter Schwabe, who is also a co-author of the research work that we’re going to discuss today.

Links to discussed papers:

Music composed by Toby Fox and performed by Sean Schafianski.

Special Guests: Douglas Stebila and Thom Wiggers.

Sponsored By:

• Symbolic Software: This episode is sponsored by Symbolic Software. Symbolic Software helps you bring in the experience and knowledge necessary to design, or prove secure, state-of-the-art cryptographic systems for new solutions. We've helped design and formally verify some of the world's most widely used cryptographic protocols.