La technologie blockchain, bien que largement adoptée, fait face à des risques de sécurité significatifs, tels que la double dépense, lors des branches temporaires de chaîne (forks) qui se produisent avant que le processus de réorganisation (reorg) ne les résolve.
Cependant, les approches de vérification formelle existantes ne capturent pas le comportement dynamique des pools de transactions et des transitions d'état pendant les processus de réorganisation, limitant leur capacité à évaluer la sécurité de la blockchain dans des conditions de fork réalistes.
Cette étude introduit une méthode pour vérifier formellement la sécurité de la blockchain en tant qu'outil d'évaluation des risques lors des reorgs, en utilisant l'outil de vérification de protocoles cryptographiques ProVerif.
Nous formalisons le pool de transactions en considérant les canaux de communication comme des ensembles.
Cela nous permet de modéliser la série de processus allant du minage aux forks de chaîne et aux reorgs, indépendamment des algorithmes de consensus spécifiques.
En imposant deux contraintes statiques sur le pool de transactions du nœud qui génère le bloc abandonné, nous développons avec succès un modèle formel qui garantit la cohérence des blocs et le comportement attendu tout au long du processus de reorg.
Cette formalisation confirme la finalité de la blockchain et facilite l'évaluation de la sécurité du système lors d'un reorg.