A tecnologia blockchain, embora amplamente adotada, enfrenta riscos de segurança significativos, como o gasto duplo, durante ramificações temporárias da cadeia (forks) que ocorrem antes que o processo de reorganização (reorg) as resolva.
No entanto, as abordagens de verificação formal existentes não capturam o comportamento dinâmico dos pools de transações e das transições de estado durante os processos de reorganização, limitando sua capacidade de avaliar a segurança da blockchain sob condições realistas de fork.
Este estudo introduz um método para verificar formalmente a segurança da blockchain como uma ferramenta de avaliação de riscos durante reorgs, utilizando a ferramenta de verificação de protocolos criptográficos ProVerif.
Formalizamos o pool de transações tratando os canais de comunicação como conjuntos.
Isso nos permite modelar a série de processos desde a mineração até os forks da cadeia e reorgs, independentemente de algoritmos de consenso específicos.
Ao impor duas restrições estáticas no pool de transações do nó que gera o bloco descartado, desenvolvemos com sucesso um modelo formal que garante a consistência do bloco e o comportamento esperado ao longo do processo de reorg.
Essa formalização confirma a finalidade da blockchain e facilita a avaliação da segurança do sistema durante um reorg.