Keetaの2相コンセンサスを形式検証、永久ロックアウトの条件を発見

Modeling and Verification of Keeta's Consensus [pdf]

Keetaは、国境を越えた高額決済向けに設計されたブロックチェーンネットワークで、クライアント主導の2相コンセンサスアルゴリズムを採用しています。本論文では、このアルゴリズムをQuintで形式仕様化し、TLCモデルチェッカーを用いてビザンチン障害モデル下で検証しました。その結果、固定された等重みの代表者集合の下で合意が保持されることを確認し、任意の代表者数への一般化を論じるとともに、競合するアカウントが恒久的にロックアウトされる条件を明らかにしました。ステーク加重投票下での安全性は未解決のままです。