La tecnología blockchain, aunque ampliamente adoptada, enfrenta riesgos de seguridad significativos, como el doble gasto, durante las ramas temporales de la cadena (forks) que ocurren antes de que el proceso de reorganización (reorg) las resuelva.
Sin embargo, los enfoques de verificación formal existentes no capturan el comportamiento dinámico de los grupos de transacciones y las transiciones de estado durante los procesos de reorganización, limitando su capacidad para evaluar la seguridad de la blockchain bajo condiciones de fork realistas.
Este estudio introduce un método para verificar formalmente la seguridad de la blockchain como una herramienta de evaluación de riesgos durante los reorgs, utilizando la herramienta de verificación de protocolos criptográficos ProVerif.
Formalizamos el grupo de transacciones tratando los canales de comunicación como conjuntos.
Esto nos permite modelar la serie de procesos desde la minería hasta los forks de la cadena y los reorgs, independientemente de los algoritmos de consenso específicos.
Al imponer dos restricciones estáticas en el grupo de transacciones del nodo que genera el bloque descartado, desarrollamos con éxito un modelo formal que garantiza la consistencia del bloque y el comportamiento esperado a lo largo del proceso de reorg.
Esta formalización confirma la finalización de la blockchain y facilita la evaluación de la seguridad del sistema durante un reorg.