Notation de protocole de sécurité
# Notation de protocole de sécurité

En cryptographie, la notation de protocole de sécurité (ingénierie), également connue sous le nom de narrations de protocole et notation Alice & Bob, est une manière d'exprimer un protocole de correspondance entre les entités d'un système dynamique, tel qu'un réseau informatique. Dans le cadre d'un modèle formel, elle permet de raisonner sur les propriétés d'un tel système.

La notation standard consiste en un ensemble de mandants (traditionnellement nommés Alice, Bob, Charlie, etc.) qui souhaitent communiquer. Ils peuvent avoir accès à un serveur S, des clés partagées K, des horodatages T, et peuvent générer des nonces N à des fins d'authentification.

Un exemple simple pourrait être le suivant :

    $A\rightarrow B:\{X\}_{K_{A,B}}$

Celui-ci indique que Alice destine un message à Bob composé d'un texte en clair X chiffré sous la clé partagée $K_{A,B}.$

Un autre exemple pourrait être le suivant :

    $B\rightarrow A:\{N_{B}\}_{K_{A}}$

Ceci indique que Bob destine un message pour Alice composé d'un nonce $N_B$ chiffré à l'aide de la clé publique d'Alice.

Une clé à deux indices, $K_{A,B},$ est une clé symétrique partagée par les deux individus correspondants. Une clé avec un indice, $K_A,$ est la clé publique de l'individu correspondant. Une clé privée est représentée comme l'inverse de la clé publique.

La notation spécifie uniquement l'opération et non sa sémantique — par exemple, le cryptage par clé privée et la signature sont représentés de manière identique.

Nous pouvons exprimer des protocoles plus compliqués de cette manière. Voir Kerberos comme exemple. Certaines sources font référence à cette notation sous le nom de notation Kerberos. Certains auteurs considèrent la notation utilisée par Steiner, Neuman, & Schiller comme une référence notable.

Plusieurs modèles existent pour raisonner sur les protocoles de sécurité de cette manière, dont l'un est la logique BAN.

La notation des protocoles de sécurité a inspiré de nombreux langages de programmation utilisés dans la programmation chorégraphique.

