A Formal Analysis Method of PoS Consensus Protocol Based on Byzantine Fault Tolerance

doi:10.3969/j.issn.1671-1122.2021.08.005

Abstract

Abstract:

The blockchain consensus protocol is an important mechanism to ensure that the data of different nodes reach consensus in the blockchain network. With the explosive growth of blockchain applications, attacks against blockchain consensus mechanisms continue to emerge. This paper proposes a formal analysis method of PoS consensus protocol based on Byzantine fault tolerance. To solve the problem of protocol model state space explosion, the method first inductively models the state migration process of all consensus nodes. Then, the communication channel models and attacker models are formally modeled based on the actual security threats. Finally, according to the requirements of protocol consistency, two kinds of security properties are formally modeled and verified. The experimental results show that the protocol has the claimed Byzantine fault tolerance, and the protocol has a double-spending attack against the zero-confirmation transaction. This paper further analyzes the conditions to implement the attack and puts forward suggestions for protection.

Key words: blockchain consensus protocol, Byzantine fault tolerance, inductive modeling, formal analysis

CLC Number:

TP309

CHEN Kaijie, XIONG Yan, HUANG Wenchao, WU Jianshuang. A Formal Analysis Method of PoS Consensus Protocol Based on Byzantine Fault Tolerance[J]. Netinfo Security, 2021, 21(8): 35-42.

Figures/Tables 9

References 20

[1]	ZHENG Min, WANG Hong, LIU Hong, et al. Survey on Consensus Algorithms of Blockchain[J]. Netinfo Security, 2019, 19(7):8-24.
	郑敏, 王虹, 刘洪, 等. 区块链共识算法研究综述[J]. 信息网络安全, 2019, 19(7):8-24.
[2]	YUAN Yong, NI Xiaochun, ZENG Shuai, et al. Blockchain Consensus Algorithms: the State of the Art and Future Trends[J]. Acta Automatica Sinica, 2018, 44(11):2011-2022.
	袁勇, 倪晓春, 曾帅, 等. 区块链共识算法的发展现状与展望[J]. 自动化学报, 2018, 44(11):2011-2022.
[3]	NAKAMOTO S. Bitcoin: A Peer-to-Peer Electronic Cash System[EB/OL]. https://bitcoin.org/bitcoin.pdf , 2008-10-31.
[4]	NAYAK K, KUMAR S, MILLER A, et al. Stubborn Mining: Generalizing Selfish Mining and Combining with An Eclipse Attack[C]//IEEE. IEEE European Symposium on Security and Privacy, March 21-24, 2016, Saarbrücken, Germany. New Jersey: IEEE, 2016: 305-320.
[5]	KARAME G, ANDROULAKI E, CAPKUN S. Double-spending Fast Payments in Bitcoin[C]//ACM. ACM Conference on Computer and Communications Security, October 16-18, 2012, Raleigh, NC, USA. New York: ACM, 2012: 906-917.
[6]	HEILMAN E, KENDLER A, ZOHAR A, et al. Eclipse Attacks on Bitcoin’s Peer-to-Peer Network[C]//USENIX. 24th USENIX Security Symposium 2015, August 12-14, 2015, Washington, D.C., USA. Berkeley: USENIX, 2015: 129-144.
[7]	BUCHMAN E. Tendermint: Byzantine Fault Tolerance in the Age of Blockchains[D]. Guelph: University of Guelph, 2016.
[8]	BLANCHET B. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[C]//IEEE. 14th IEEE Computer Security Foundations Workshop(CSFW-14 2001), June 11-13, 2001, Cape Breton, Nova Scotia, Canada. Piscataway: IEEE, 2001: 82-96.
[9]	MEIER S, SCHMIDT B, CREMERS C, et al. The TAMARIN Prover for the Symbolic Analysis of Security Protocols[C]//Springer. Computer Aided Verification, July 13-19, 2013, Saint Petersburg, Russia. Berlin: Springer, 2013: 696-701.
[10]	BASIN D A, DREIER J, HIRSCHI L, et al. A Formal Analysis of 5G Authentication[C]//ACM. 2018 ACM SIGSAC Conference on Computer and Communications Security, October 15-19, 2018, Toronto, ON, Canada. New York: ACM, 2018: 1383-1396.
[11]	CREMERS C, KIESL B, MEDINGER N. A Formal Analysis of IEEE 802.11’s WPA2: Countering the Kracks Caused by Cracking the Counters[C]//USENIX. 29th USENIX Security Symposium, August 12-14, 2020, Boston, USA. Berkeley: USENIX, 2020: 1-17.
[12]	CREMERS C, HORVAT M, HOYLAND J. A Comprehensive Symbolic Analysis of TLS 1.3[C]//ACM. 2017 ACM SIGSAC Conference on Computer and Communications Security, October 30-November 3, 2017, Dallas, TX, USA. New York: ACM, 2017: 1773-1788.
[13]	MILLER A, LAVIOLA J J. Anonymous Byzantine Consensus from Moderately-hard Puzzles: A Model for Bitcoin[EB/OL]. https://allquantor.at/blockchainbib/pdf/miller2014anonymous.pdf , 2020-12-22.
[14]	GARAY J A, KIAYIAS A, LEONARDOS N. The Bitcoin Backbone Protocol: Analysis and Applications[C]//Springer. 34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, April 26-30, 2015, Sofia, Bulgaria. Berlin: Springer, 2015: 281-310.
[15]	PASS R, SEEMAN L, SHELAT A. Analysis of the Blockchain Protocol in Asynchronous Networks[C]//Springer. 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, April 30-May 4, 2017, Paris, France. Berlin: Springer, 2017: 643-673.
[16]	DAIAN P, PASS R, SHI E. Snow White: Provably Secure Proofs of Stake[EB/OL]. https://eprint.iacr.org/2016/919.pdf , 2016-09-21.
[17]	DAVID B, GAZI P, KIAYIAS A, et al. Ouroboros Praos: An Adaptively-secure, Semi-synchronous Proof-of-stake Blockchain[C]//Springer. 37th Annual International Conference on the Theory and Applications of Cryptographic Techniques, April 29-May 3, 2018, Tel Aviv, Israel. Berlin: Springer, 2018: 66-98.
[18]	YACKOLLEY A, ANTONELLA D P, MARIA P, et al. Correctness of Tendermint-core Blockchains[C]//Springer. 22nd International Conference on Principles of Distributed Systems, December 17-19, 2018, Hong Kong, China. Berlin: Springer, 2018: 1-16.
[19]	THIN W Y M M, DONG N, BAI G, et al. Formal Analysis of a Proof-of-stake Blockchain[C]//IEEE. 23rd International Conference on Engineering of Complex Computer Systems, December 12-14, 2018, Melbourne, Australia. Piscataway: IEEE, 2018: 197-200.
[20]	DOLEV D, YAO A C. On the Security of Public Key Protocols[C]//IEEE. 22nd Annual Symposium on Foundations of Computer Science, October 28-30, 1981, Nashville, Tennessee, USA. Piscataway: IEEE, 1981: 350-357.

规则形式化表示	规则说明
[In(<signed_valid_txs, valid_txs, pkc>), Ld_State1($L, pkl, skl, height, round, step, proposal)]	前提1：从公开信道获取有效交易前提2：提议节点处于状态1
--[Eq(verify(signed_valid_txs, valid_txs, pkc), true), Generate_Newpoposal(pkl, proposal, height)]->	动作1：交易签名真实有效动作2：产生新交易提案
[Ld_State2($L, pkl, skl, height, round, step, proposal), Out(signed_proposal)]	结论1：提议节点进入状态2 结论2：提议节点发送新交易提案到公开信道

威胁模型记号	模型说明（3类信道均由敌手控制）
A₍_honest₎	所有节点均诚实
A₍_transaction₎	部分交易节点被敌手控制
A₍_validator_<1/3)	比例为r的验证节点被敌手控制（0 < r <1/3）
A_(1/3≤_{validator <}_2/3)	比例为r的验证节点被敌手控制（1/3≤r < 2/3）
A₍_validator_≥2/3)	比例为r的验证节点被敌手控制（2/3≤r≤1）
A₍_proposer₎	提议节点被敌手控制

实验设置	具体配置
实验工具	Tamarin-prover
版本号	1.6.0
操作系统	Ubuntu18.04 LTS
处理器	Intel(R) Core (TM) i5-3450 CPU @3.10 GHz×4
内存	16 GB

威胁模型	A₁	A₂	A₃	A₄	A₅
A₍_honest₎	√	√	√	√	√
A₍_transaction₎	√	√	√	√	√
A₍_validator<_1/3)	√	√	√	√	√
A_(1/3≤_validator<_2/3)	×	×	×	×	×
A₍_validator_≥2/3)	×	×	×	×	×
A₍_proposer₎	×	√	×	√	√

威胁模型	B₁	B₂	B₃
A₍_honest₎	√	√	√
A₍_transaction₎	×	√	√
A₍_validator<_1/3)	√	√	√
A_(1/3≤_validator<_2/3)	×	×	×
A₍_validator_≥2/3)	×	×	×
A₍_proposer₎	×	√	√