Die Blockchain-Technologie, obwohl weit verbreitet, sieht sich erheblichen Sicherheitsrisiken ausgesetzt, wie z.B. dem Double Spending, während temporärer Kettenzweige (Forks), die auftreten, bevor der Reorganisationsprozess (Reorg) sie löst.
Allerdings erfassen bestehende formale Verifikationsansätze nicht das dynamische Verhalten von Transaktionspools und Zustandsübergängen während der Reorganisationsprozesse, was ihre Fähigkeit einschränkt, die Sicherheit der Blockchain unter realistischen Fork-Bedingungen zu bewerten.
Diese Studie führt eine Methode ein, um die Sicherheit der Blockchain als Risikobewertungstool während Reorgs formal zu verifizieren, indem das kryptografische Protokollverifikationstool ProVerif genutzt wird.
Wir formalisierten den Transaktionspool, indem wir Kommunikationskanäle als Mengen behandelten.
Dies ermöglicht es uns, die Reihe von Prozessen vom Mining über Kettenforks bis hin zu Reorgs zu modellieren, unabhängig von spezifischen Konsensalgorithmen.
Durch die Auferlegung von zwei statischen Einschränkungen auf den Transaktionspool des Knotens, der den verworfenen Block generiert, entwickeln wir erfolgreich ein formales Modell, das die Blockkonsistenz und das erwartete Verhalten während des Reorg-Prozesses sicherstellt.
Diese Formalisierung bestätigt die Endgültigkeit der Blockchain und erleichtert die Bewertung der Systemsicherheit während eines Reorg.