# 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(κ^{3.2}) against O(κ^{7.87}) for the previous constructions, where κ is the security parameter. We also show that our constructions achieve a quadratic complexity in κ 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.