Byzantizing Paxos by Refinement
Byzantizing Paxos by Refinement
复制标题
通过细化拜占庭化 Paxos
DOI：
10.1007/978-3-642-24100-0_22
复制
发表时间：
2011
期刊：
影响因子：
9.2
通讯作者：
L. Lamport
中科院分区：
文献类型：
--
作者：
L. Lamport
我们通过Byzantizing普通Paxos算法的一个变体推导出3f +1进程Byzantine Paxos共识算法-也就是说，尽管存在f个恶意进程，但通过让2f+1个无故障进程模拟普通Paxos算法。我们已经写了一个正式的，机器检查的证明，拜占庭算法实现了普通的Paxos共识算法在一个合适的细化映射。
We derive a 3f +1 process Byzantine Paxos consensus algorithm by Byzantizing a variant of the ordinary Paxos algorithm--that is, by having 2f+1 nonfaulty processes emulate the ordinary Paxos algorithm despite the presence of f malicious processes. We have written a formal, machine-checked proof that the Byzantized algorithm implements the ordinary Paxos consensus algorithm under a suitable refinement mapping.