We study selfish mining attacks in longest-chain blockchains like Bitcoin, but where the proof of work is replaced with efficient proof systems -- like proofs of stake or proofs of space -- and consider the problem of computing an optimal selfish mining attack which maximizes expected relative revenue of the adversary, thus minimizing the chain quality. To this end, we propose a novel selfish mining attack that aims to maximize this objective and formally model the attack as a Markov decision process (MDP). We then present a formal analysis procedure which computes an $\epsilon$-tight lower bound on the optimal expected relative revenue in the MDP and a strategy that achieves this $\epsilon$-tight lower bound, where $\epsilon>0$ may be any specified precision. Our analysis is fully automated and provides formal guarantees on the correctness. We evaluate our selfish mining attack and observe that it achieves superior expected relative revenue compared to two considered baselines. In concurrent work [Sarenche FC'24] does an automated analysis on selfish mining in predictable longest-chain blockchains based on efficient proof systems. Predictable means the randomness for the challenges is fixed for many blocks (as used e.g., in Ouroboros), while we consider unpredictable (Bitcoin-like) chains where the challenge is derived from the previous block.

翻译：我们研究了像比特币这样的最长链区块链中的自私挖矿攻击，但其中工作量证明被高效证明系统（如权益证明或空间证明）所取代，并考虑了计算最优自私挖矿攻击的问题，该攻击旨在最大化对手的期望相对收益，从而最小化链质量。为此，我们提出了一种新颖的自私挖矿攻击，以最大化这一目标，并将该攻击形式化为马尔可夫决策过程（MDP）。然后，我们提出了一种形式化分析流程，用于计算MDP中最优期望相对收益的$\epsilon$-紧下界，以及实现该$\epsilon$-紧下界的策略，其中$\epsilon>0$可以是任意指定的精度。我们的分析是完全自动化的，并提供关于正确性的形式化保证。我们评估了所提出的自私挖矿攻击，并观察到与两种考虑的基线相比，它实现了更优的期望相对收益。在并行工作中，[Sarenche FC'24] 对基于高效证明系统的可预测最长链区块链进行了自私挖矿的自动化分析。可预测意味着挑战的随机性在多个区块中是固定的（例如，在Ouroboros中使用），而我们考虑的是不可预测的（类比特币）链，其中挑战源自前一个区块。