Modèle d’attaquant de Dolev-Yao et cryptographie symbolique

Proposé par Danny Dolev et Andrew Yao en 1983, le modèle de Dolev-Yao est le modèle standard de l'adversaire pour l'analyse symbolique des protocoles. L'attaquant contrôle l'ensemble du réseau.

L'attaquant de Dolev-Yao peut : intercepter n'importe quel message, stocker des messages, rejouer d'anciens messages et forger de nouveaux messages à partir de composants connus, mais il ne peut pas casser les primitives cryptographiques sous-jacentes.

Dans les modèles symboliques, le chiffrement est une boîte noire parfaite : l’attaquant ne peut pas déchiffrer sans la clé, factoriser de grands nombres ni falsifier des signatures. Cela simplifie l’analyse, mais peut laisser de côté des attaques visant l’implémentation.

Les messages sont modélisés comme des termes : enc(k, m), sig(sk, m), hash(m), pair(a, b). L’attaquant connaît certains termes et en dérive de nouveaux à l’aide de règles définies (règles de déduction).

Les connaissances de l’attaquant sont closes par déduction : s’il connaît enc(k,m) et k, il peut en déduire m. S’il connaît pair(a,b), il peut en déduire a et b. La clôture des connaissances initiales = tout ce que l’attaquant peut apprendre.

La sécurité du protocole s’énonce ainsi : « les connaissances de l’attaquant ne contiennent jamais le secret s dans aucun état atteignable ». Confidentialité = atteignabilité. Authentification = absence de certains schémas de traces indésirables.

Protocole à deux parties : A→B : {Na, A}_{K_B} ; B→A : {Na, Nb}_{K_A} ; A→B : {Nb}_{K_B}. En algèbre des termes : Alice envoie enc(pubkey_B, pair(Na, A)). Nous vérifions qu’après l’exécution, seul B connaît Na.

Le calcul pi appliqué (Abadi et Fournet, 2001) est une algèbre de processus destinée à modéliser les protocoles. Les processus communiquent par des canaux ; l’attaquant contrôle les canaux publics. ProVerif et Tamarin utilisent ce formalisme.

Un protocole sécurisé dans le modèle de Dolev-Yao peut néanmoins être vulnérable sur le plan computationnel si l’instanciation cryptographique est faible. Le théorème de solidité computationnelle (Cortier et al.) fait le lien pour certaines classes de primitives.

Dolev-Yao ne peut pas modéliser : les propriétés algébriques (par exemple, la commutativité de XOR), les attaques par canal auxiliaire, les bogues d’implémentation ou les défaillances probabilistes. Des extensions comme le modèle par théorie équationnelle prennent en charge certaines propriétés algébriques.

Dolev-Yao donne à l’attaquant le contrôle total du réseau, tout en supposant une cryptographie parfaite. Les messages sont des termes dans une algèbre ; la sécurité est une propriété d’atteignabilité. Le calcul pi appliqué fournit le langage formel. Limites : il ne peut pas modéliser les relations algébriques, les canaux auxiliaires ni les bogues d’implémentation.