Advances in computer-aided cryptography
Designing, analyzing and implementing correct, secure and efficient cryptography are challenging tasks. Computer-aided cryptography is a young field of research which aims to provide rigorous tools that ease these tasks. Computer-aided cryptography leverages advances in the broad area of formal methods, and in particular program verification. The talk will present recent developments in computer-aided cryptography and reflect on some of the challenges, benefits and opportunities.
Gilles Barthe is a scientific director at MPI-SP and a part-time research professor at the IMDEA Software Institute. His research interests include logic, formal verification, programming languages, security and privacy. His current work focuses on formal approaches for high-assurance cryptographic algorithms and implementations.
Security of Masked Implementations
Masking is a sound and widely deployed countermeasure to counteract side-channel attacks on embedded systems. In a nutshell, it consists in splitting each sensitive variable manipulated in the implementation into t+1 shares, where the masking order t represents the security level. In the probing model defined by Ishai, Sahai, and Wagner at Crypto 2003, an attacker is allowed to get the exact value of t variables in the implementation. Within this model, if the t+1 shares of each sensitive data are manipulated independently from each other, then the masking countermeasure makes the implementation t-probing secure. While the masking countermeasure well improves the security level of an implementation, it can be complex to design as t grows. This first part of my talk will be dedicated to recent automatic tools that manage to detect all possible flaws in the probing model given concrete implementations. So far, such tools remain exponential in the implementation size and in the masking order making it impossible to verify reasonable implementations (e.g., of a block cipher) at reasonable order (e.g., greater than 2). In the second part of my talk, I'll thus review recent techniques of composition. Namely, secure gadgets as atomic masked functions (e.g., masked multiplications, additions) can be composed into probing secure global implementations by inserting strong refreshing gadgets at carefully chosen locations. I'll try to give an overview of recent progress together with the remaining limitations, before concluding on ongoing challenges.
Sonia Belaïd is a security expert at CryptoExperts in France. She received her PhD degree in Computer Science from the Ecole Normale Supérieure (ENS) in Paris in 2015 for her thesis on side-channel attacks and countermeasures. Prior to joining CryptoExperts in August 2017, Sonia held engineering positions at Oberthur Technologies (now Idemia) and Thales. Her interests include cryptography, cybersecurity, and also formal methods. In particular, she has contributed to new efficient and formally proven secure countermeasures to thwart side-channel attacks.
Practical quantum-resistant key exchange from supersingular isogenies and its efficient implementation
Supersingular isogeny key encapsulation (SIKE), an IND-CCA secure protocol based on the very popular SIDH protocol, stands out as one of the most attractive cryptosystems in the ongoing NIST post-quantum standardization process, thanks to featuring the smallest keys among all the candidates and for being the only isogeny-based algorithm submitted that is partially based on traditional elliptic curve arithmetic. In this talk we describe SIDH and SIKE, their underlying arithmetic and its efficient implementation on popular platforms.
Dr. Patrick Longa is a cryptography researcher with the MSR Security and Cryptography group at Microsoft Research, USA. He is co-designer of several cryptographic primitives and protocols including the post-quantum schemes SIKE, qTESLA and FrodoKEM, the high-speed elliptic curve FourQ, and state-of-the-art instantiations of SIDH. He has written several high-performance cryptographic libraries including FourQlib and SIDH, and his research interests mainly involve post-quantum cryptography, elliptic curve cryptography, algorithmic design, and high-performance implementation of cryptographic primitives.