💻 computer science

Formal Verification of Probing Security via Conditional Independence

Cet article propose une nouvelle approche de vérification formelle pour la sécurité par sondage des algorithmes cryptographiques masqués en exploitant la logique de séparation probabiliste (Lilac) pour établir un lien entre les propriétés de non-interférence et l'indépendance conditionnelle.

Auteurs originaux : Satoshi Kura, Katsuyuki Takashima

Publié 2026-05-25

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Satoshi Kura, Katsuyuki Takashima

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayiez de garder une recette secrète en sécurité dans une cuisine animée et bruyante. Dans le monde de la cryptographie, cette « recette secrète » est une clé privée, et le « bruit » est une attaque par canal auxiliaire. Les attaquants ne tentent pas de casser les mathématiques ; ils essaient d'observer les « fuites » (comme la consommation d'énergie ou le temps d'exécution) pendant que l'ordinateur effectue des calculs pour deviner votre secret.

Pour empêcher cela, les cryptographes utilisent une technique appelée Masquage. Imaginez le masquage comme le fait de déchiqueter votre recette secrète en $t+1$ morceaux de papier (parts). Vous donnez un morceau à chacun des $t+1$ chefs différents. Tant qu'un espion ne peut observer que $t$ morceaux (ou moins), il ne voit que du charabia aléatoire. Il ne peut pas reconstituer la recette car il manque au moins une pièce cruciale.

Cependant, prouver qu'une recette complexe (algorithme) est véritablement sûre est incroyablement difficile. Si vous essayez de la vérifier à la main, vous pourriez manquer une fuite infime, et tout le système de sécurité échouera. C'est là que l'article intervient.

Le Problème : Vérifier la « Fuite »

Les auteurs souhaitent établir une preuve formelle (une garantie mathématique) qu'un algorithme masqué est sûr. Traditionnellement, cela se fait en utilisant le concept de « Simulateur ».

L'idée du Simulateur : Imaginez une boîte magique (le simulateur) qui tente de recréer exactement ce que l'espion observe. Si la boîte magique peut produire la même « fuite » exacte en utilisant uniquement les informations publiques (comme la liste des ingrédients) et sans jamais voir les morceaux de la recette secrète, alors l'algorithme réel est sûr. L'espion n'apprend rien de nouveau.

Mais construire ces simulateurs à la main est sujet aux erreurs. Les auteurs voulaient une meilleure façon de prouver cela.

La Solution : Un Nouvel Outil Logique (Lilac)

Les auteurs établissent un lien entre les « Simulateurs » et un concept appelé Indépendance Conditionnelle.

L'Analogie : Imaginez que vous essayez de deviner l'anniversaire d'un ami (le secret).
- Scénario A : Vous connaissez son âge et le mois de sa naissance (Info Publique).
- Scénario B : Vous connaissez aussi l'entrée de son journal intime secret (Info Secrète).
- Indépendance Conditionnelle : Si connaître l'entrée du journal intime ne change pas votre hypothèse sur l'anniversaire une fois que vous connaissez déjà l'âge et le mois, alors le journal est « conditionnellement indépendant » de l'anniversaire étant donné l'âge/le mois.

L'article prouve que si un simulateur existe, alors le secret est conditionnellement indépendant de la fuite, étant donné les informations publiques.

Pour vérifier cela mathématiquement, ils utilisent un outil appelé Lilac.

Qu'est-ce que Lilac ? Imaginez Lilac comme un manuel de règles très strict et surpuissant pour les probabilités. C'est comme un jeu de logique où vous devez prouver que deux tas de cartes (variables aléatoires) sont mélangés indépendamment l'un de l'autre.
La « Conjonction Séparante » : Dans ce manuel de règles, il existe un symbole spécial (comme une baguette magique) qui dit : « Ces deux tas de cartes sont totalement séparés et ne s'influencent pas mutuellement. »
L'Innovation : Les auteurs ont ajouté de nouvelles règles à ce manuel pour gérer la « Conditionnement » (la partie « étant donné que... »). Cela leur permet de prouver que même si l'espion voit certaines données, cela ne révèle pas le secret *parce qu'*ils possèdent déjà les données publiques.

Ce Qu'ils Ont Réellement Fait

Les auteurs ne se sont pas contentés de parler de théorie ; ils ont construit un système pour vérifier de vrais algorithmes cryptographiques en utilisant cette nouvelle logique. Ils ont appliqué leur méthode à trois « gadgets » (briques de construction) spécifiques utilisés dans le chiffrement moderne :

MINIADDREPNOISE : Un outil utilisé pour ajouter du bruit aléatoire aux données (comme ajouter du sel à une soupe pour masquer la saveur originale). Ils ont prouvé que même si un attaquant observe une partie de la soupe salée, il ne peut pas déterminer la saveur originale.
REFRESH : Un outil qui prend les morceaux déchiquetés du secret et les remélange pour qu'ils semblent tout neufs, empêchant les attaquants de les suivre dans le temps. Ils ont prouvé que ce remélangeage est sûr.
SECMULT (Multiplication Sécurisée) : Un outil qui multiplie deux nombres secrets ensemble sans révéler le résultat jusqu'à la toute fin. C'est l'une des opérations les plus difficiles à sécuriser. Ils ont prouvé que cette multiplication est sûre contre les attaques par « sondage t ».

La Conclusion

L'article affirme qu'en traduisant l'idée complexe des « Simulateurs » dans le langage de l'« Indépendance Conditionnelle », ils peuvent utiliser le système logique Lilac pour vérifier automatiquement et rigoureusement que ces outils cryptographiques sont sûrs.

Ils ont démontré cela avec succès en écrivant des preuves formelles pour MINIADDREPNOISE, REFRESH et SECMULT, montrant que ces algorithmes spécifiques satisfont aux exigences de sécurité strictes nécessaires pour protéger les secrets contre les attaques par canal auxiliaire. Ils n'ont pas prétendu résoudre tous les problèmes de sécurité futurs ni appliquer cela à des dispositifs médicaux ; leur travail concerne strictement la preuve de la sécurité de ces opérations mathématiques cryptographiques spécifiques en utilisant un nouveau cadre logique.

Résumé Technique : Vérification Formelle de la Sécurité par Sonde via l'Indépendance Conditionnelle

Énoncé du Problème

Les attaques par canal auxiliaire constituent une menace majeure pour la sécurité des schémas cryptographiques, ce qui a favorisé l'adoption généralisée du masquage en tant que contre-mesure. Le masquage divise les valeurs secrètes en parts pour garantir que la fuite d'information provenant de n'importe quel sous-ensemble de valeurs intermédiaires ne révèle pas le secret sous-jacent. Cependant, prouver la sécurité des algorithmes masqués, en particulier sous le modèle de sondage ISW (où un adversaire peut sonder jusqu'à $t$ valeurs intermédiaires), est notoirement sujet à erreurs lorsqu'il est effectué manuellement. Plusieurs failles ont été identifiées dans les preuves de sécurité manuelles, rendant nécessaire la vérification formelle.

Bien que la logique de séparation probabiliste ait été appliquée avec succès pour vérifier des propriétés telles que l'indépendance des entrées (par exemple, dans les jetons à usage unique), elle n'a pas encore été utilisée pour vérifier la sécurité par sondage (spécifiquement la $t$ -non-interférence) des algorithmes masqués. Les outils de vérification formelle existants reposent souvent sur des méthodes basées sur la substitution ou l'inférence de types, qui peuvent manquer de modularité ou d'expressivité nécessaires au raisonnement complexe sur l'indépendance conditionnelle inhérent au masquage.

Méthodologie

Ce travail propose une approche novatrice de vérification formelle en établissant un lien rigoureux entre les définitions de sécurité basées sur les simulateurs et l'indépendance conditionnelle. La méthodologie repose sur Lilac, une logique de séparation probabiliste conçue pour raisonner sur l'indépendance conditionnelle.

1. Fondement Théorique : Simulateurs et Indépendance Conditionnelle

Les auteurs reformulent la définition standard de non-interférence basée sur les simulateurs en termes d'indépendance conditionnelle.

Vue basée sur les simulateurs : Un algorithme masqué est sécurisé si, pour tout ensemble de sondes $O$ (observé par un adversaire), il existe un simulateur capable de générer la distribution de $O$ en utilisant uniquement un sous-ensemble de parts d'entrée $I$ , sans accès aux parts secrètes restantes.
Vue basée sur l'indépendance conditionnelle : Cette exigence de sécurité équivaut à l'affirmation selon laquelle les valeurs observées $O$ sont conditionnellement indépendantes des parts d'entrée secrètes ( $\Delta \setminus I$ ) étant donné les parts d'entrée publiques $I$ . Formellement, cela s'exprime par $O \perp (\Delta \setminus I) \mid I$ .

L'article démontre que cette équivalence vaut dans le cadre sémantique de Lilac, qui modélise l'indépendance probabiliste à l'aide de combinaisons indépendantes d'espaces de probabilité et de conditionnement via la désintégration.

2. Extension de Lilac

Pour appliquer Lilac à la sécurité par sondage, les auteurs étendent la logique avec des règles de preuve spécifiques qui n'étaient pas présentes dans la formulation originale de Lilac :

Axiomes Semi-Gémoïdes : L'article démontre que les axiomes semi-gémoïdes de l'indépendance conditionnelle (Symétrie, Décomposition, Union Faible et Contraction) valent dans la sémantique de Lilac. Ces axiomes sont cruciaux pour manipuler les énoncés d'indépendance conditionnelle lors des preuves.
Règles de Composabilité : De nouvelles règles sont introduites pour gérer la composition des propriétés de non-interférence, spécifiquement pour la composition séquentielle et les boucles for. Ces règles permettent une vérification modulaire d'algorithmes complexes construits à partir de petits gadgets.
Propriété et Affaiblissement : Des règles supplémentaires facilitent le raisonnement sur la propriété des variables aléatoires et l'affaiblissement des propriétés de non-interférence lors du traitement d'entrées non partagées ou de sous-ensembles de variables.

3. Cadre de Vérification

Le processus de vérification implique :

La traduction des algorithmes masqués (écrits dans le langage de programmation probabiliste APPL) en triplets de Hoare dans Lilac.
L'utilisation de l'équivalence établie (Théorème V.1) pour réduire la vérification de la $(I, O)$ -non-interférence à la preuve d'un triplet de Hoare spécifique d'indépendance conditionnelle :
$\{ \text{own } \Delta \} \ M \ \{ Y. \ C_{x \leftarrow I}(\text{own}(\Delta \setminus I) * \text{own } O) \}$
L'application de l'ensemble étendu de règles de preuve (incluant les nouveaux axiomes semi-gémoïdes et les règles de composabilité) pour dériver les implications requises.

Contributions Clés

Lien Formel : L'article établit une équivalence formelle entre les définitions de sécurité par sondage basées sur les simulateurs et les propriétés d'indépendance conditionnelle exprimables dans Lilac. Cela comble le fossé entre les notions de sécurité cryptographique et la logique de séparation probabiliste.
Extension de Lilac : Les auteurs fournissent une suite de règles de preuve supplémentaires nécessaires pour vérifier les algorithmes masqués, incluant les axiomes semi-gémoïdes pour l'indépendance conditionnelle et les règles de composabilité pour la composition séquentielle et les boucles.
Études de Cas : L'efficacité de l'approche est démontrée en vérifiant formellement la sécurité par sondage de trois algorithmes critiques utilisant Lilac :
- MINIADDREPNOISE : Une sous-routine pour ajouter du bruit uniforme aux valeurs masquées.
- REFRESH : Un algorithme fondamental pour rafraîchir les parts afin d'empêcher l'accumulation de fuites.
- SECMULT : Un algorithme standard de multiplication masquée.
- ADDREPNOISEER : Une variante utilisée dans le schéma de signature Raccoon (un candidat pour la standardisation de la Cryptographie Post-Quantique NIST), prouvant qu'il satisfait la propriété de $t$ -Non-Interférence Forte avec Entrée Non Partagée ( $t$ -SNIU).

Résultats

L'article dérive avec succès des triplets de Hoare pour les algorithmes cibles, confirmant leurs propriétés de non-interférence.

Pour MINIADDREPNOISE, la preuve montre que les parts de sortie sont conditionnellement indépendantes des parts d'entrée non observées étant donné les entrées observées.
Pour REFRESH, la preuve vérifie que l'algorithme satisfait la $t$ -Non-Interférence Forte ( $t$ -SNI), une propriété plus forte que la non-interférence standard, essentielle pour la composabilité dans le masquage d'ordre supérieur.
Pour SECMULT et ADDREPNOISEER, les preuves exploitent les nouvelles règles de composabilité pour gérer les boucles imbriquées et les dépendances de données complexes inhérentes à ces algorithmes.

La vérification de ADDREPNOISEER est particulièrement significative car elle valide un composant clé de la preuve de sécurité du schéma de signature Raccoon, qui repose sur la propriété $t$ -SNIU.

Importance et Revendications

Les auteurs affirment que ce travail fournit la première application de la logique de séparation probabiliste (spécifiquement Lilac) à la vérification formelle de la sécurité par sondage pour les algorithmes masqués. En traduisant les preuves de sécurité en raisonnement sur l'indépendance conditionnelle, l'approche offre une alternative modulaire et logiquement rigoureuse aux outils existants basés sur la substitution ou l'inférence de types.

L'article souligne que, bien que l'idée sous-jacente de relier les simulateurs à l'indépendance conditionnelle soit conceptuellement simple, sa formalisation dans Lilac est techniquement non triviale en raison de la dépendance de la logique aux combinaisons indépendantes plutôt qu'aux espaces de probabilité produits standards. La dérivation réussie du théorème principal et l'application à des composants cryptographiques réels (Raccoon) démontrent que ce cadre est viable pour vérifier des schémas de masquage complexes et d'ordre élevé.

Le travail reste modeste quant à son périmètre, notant que les résultats actuels sont limités au cadre informationnel de la sécurité par sondage. Les auteurs identifient l'extension de l'approche au cadre computationnel et l'implémentation de la méthode dans un prouveur de théorèmes interactif comme des directions importantes pour les travaux futurs. Ils suggèrent également que le cadre pourrait être appliqué à d'autres propriétés de sécurité basées sur les simulateurs, telles que celles trouvées dans le calcul multipartite sécurisé.