Blockchain technology, though widely adopted, faces significant security risks, such as double spending, during temporary chain branches (forks) that occur before the reorganization (reorg) process resolves them.
However, existing formal verification approaches do not capture the dynamic behavior of transaction pools and state transitions during reorganization processes, limiting their ability to assess blockchain safety under realistic fork conditions.
This study introduces a method to formally verify the safety of the blockchain as a risk-assessment tool during reorgs, utilizing the cryptographic protocol verification tool ProVerif.
We formalize the transaction pool by treating communication channels as sets.
This allows us to model the series of processes from mining to chain forks and reorgs, independent of specific consensus algorithms.
By imposing two static constraints on the transaction pool of the node that generates the discarded block, we successfully develop a formal model that ensures block consistency and expected behavior throughout the reorg process.
This formalization confirms blockchain finality and facilitates the evaluation of system safety during a reorg.