Il y a des outils ± formels pour ça, ça peut aider à trouver les failles (faire son propre protocole, c'est dangereux et compliqué, surtout avec la crypto, cf les failles découvertes récemment dans TLS ou les passeports français). En général, c'est pas facile à utiliser, mais il y a un nouvel arrivant assez intéressant par l'un des auteurs de Raft (le protocole de consensus). Il décrit l'outil dans un blog post. Le focus est mis sur la simulation (on écrit un petit programme pour représenter le protocole, on écrit des invariants, et on peut lancer des simulations randomisées pour tester — en gros, du model checking) ET sur la visualisation (avec d3.js) pour débugguer le protocole en même temps qu'on le formalise. Perso j'aime bien l'exemple des ascenseurs ^
# en parlant de décrire des protocoles
Posté par c^3 . En réponse au journal Écrire des diagrammes de séquences. Évalué à 2.
Il y a des outils ± formels pour ça, ça peut aider à trouver les failles (faire son propre protocole, c'est dangereux et compliqué, surtout avec la crypto, cf les failles découvertes récemment dans TLS ou les passeports français). En général, c'est pas facile à utiliser, mais il y a un nouvel arrivant assez intéressant par l'un des auteurs de Raft (le protocole de consensus). Il décrit l'outil dans un blog post. Le focus est mis sur la simulation (on écrit un petit programme pour représenter le protocole, on écrit des invariants, et on peut lancer des simulations randomisées pour tester — en gros, du model checking) ET sur la visualisation (avec d3.js) pour débugguer le protocole en même temps qu'on le formalise. Perso j'aime bien l'exemple des ascenseurs ^
The cake is a lie.