Supervision : Damien VERGNAUD

Co-supervision : Sonia BELAÏD et Matthieu RIVAIN

Secure and Verified Cryptographic Implementations in the Random Probing Model

The masking countermeasure is among the most potent countermeasures to counteract side-channel attacks. Leakage models have been exhibited to theoretically reason on the security of such masked implementations. So far, the most widely used leakage model is the probing model, but it has been recently challenged as it does not fully capture the capabilities of a side-channel adversary. To capture a broader class of attacks, another model was introduced, referred to as the random probing model. From a leakage parameter p, each wire of the circuit leaks its value with probability p. The random probing model enjoys practical relevance thanks to a reduction to the noisy leakage model, which is admitted as the suitable formalization for power and electromagnetic side-channel attacks. In addition, the random probing model is much more convenient than the noisy leakage model to prove the security of masking schemes.
In this thesis, we study more closely the random probing model and define the first framework dedicated to it. We formalize a composition property for secure random probing gadgets and exhibit its relation to the strong non-interference (SNI) notion used in probing security. We then revisit the expansion idea proposed by Ananth, Ishai, and Sahai (CRYPTO 2018) and introduce a compiler that builds a random probing secure circuit from small base gadgets, achieving a random probing expandability (RPE) property. We then provide an in-depth analysis of the RPE security notion, allowing us to obtain much more efficient instantiations of the expansion technique, with constructions tolerating a leakage probability of up to 2^-7, against 2^-26 for the previous construction and an improved complexity of O kappa^3.2 against O kappa^7.87 for the previous constructions, where kappa is the security parameter. We also show that our constructions achieve a quadratic complexity in kappa asymptotically as the number of shares grows. Further attempts to optimize constructions include generalizing the RPE approach by considering a dynamic choice of the base gadgets at each step in the expansion. We show that such techniques can further reduce the complexity from quadratic to quasi-linear while tolerating good leakage rates.
Finally, we introduce IronMask, a new versatile verification tool for masking security. IronMask is the first to verify standard simulation-based security notions in the probing model and recent notions in the random probing model. It supports any masking gadgets with linear randomness (e.g., addition, copy, and refresh gadgets) as well as quadratic gadgets (e.g., multiplication gadgets) that might include non-linear randomness (e.g., by refreshing their inputs) while providing complete verification results for both types of gadgets.
We conclude this thesis by discussing ongoing research projects in the random probing model and suggestions for future works.

2020-2023 Publications

• 2023
  • A. Taleb : “Secure and Verified Cryptographic Implementations in the Random Probing Model”, thesis, defence 11/07/2023, supervision Vergnaud, Damien, co-supervision : Sonia, BELAÏD et Matthieu RIVAIN (2023)
  • Q. Meunier, A. Taleb : “VerifMSI: Practical Verification of Hardware and Software Masking Schemes Implementations”, Proceedings of the 20^th International Conference on Security and Cryptography SECRYPT, vol. 1, Rome, Italy, pp. 520-527, (SciTePress), (ISBN: 978-989-758-666-8) (2023)
• 2022
  • S. Belaid, D. Mercadier, M. Rivain, A. Taleb : “IronMask: Versatile Verification of Masking Security”, 2022 IEEE Symposium on Security and Privacy (SP), San Francisco, United States, pp. 142-160, (IEEE) (2022)
• 2021
  • S. Belaid, M. Rivain, A. Taleb, D. Vergnaud : “Dynamic Random Probing Expansion with Quasi Linear Asymptotic Complexity”, Advances in Cryptology – Asiacrypt 2021, vol. 13091, Lecture Notes in Computer Science, Singapour, Singapore, pp. 157-188, (Springer) (2021)
  • S. Belaid, M. Rivain, A. Taleb : “On the Power of Expansion: More Efficient Constructions in the Random Probing Model”, Advances in Cryptology - EUROCRYPT 2021 - 40^th Annual International Conference on the Theory and Applications of Cryptographic Techniques, vol. 12697, Lecture Notes in Computer Science, Zagreb, Croatia, pp. 313-343, (Springer International Publishing) (2021)
  • A. Taleb, D. Vergnaud : “Speeding-Up Verification of Digital Signatures”, Journal of Computer and System Sciences, vol. 116, pp. 22-39, (Elsevier) (2021)
• 2020
  • S. Belaid, J.‑S. Coron, E. Prouff, M. Rivain, A. Taleb : “Random Probing Security: Verification, Composition, Expansion and New Constructions”, Advances in Cryptology - CRYPTO}2020 - 40^th Annual International Cryptology Conference, {CRYPTO} 2020, Santa Barbara, CA, USA, August 17-21, 2020, Proceedings, Part I, vol. 12170, Lecture Notes in Computer Science, Santa Barbara, CA / Virtual, United States, pp. 339-368, (Springer) (2020)