一种基于拜占庭容错的PoS共识协议形式化分析方法

doi:10.3969/j.issn.1671-1122.2021.08.005

信息网络安全 ›› 2021, Vol. 21 ›› Issue (8): 35-42.doi: 10.3969/j.issn.1671-1122.2021.08.005

一种基于拜占庭容错的PoS共识协议形式化分析方法

陈凯杰¹(), 熊焰¹, 黄文超¹, 武建双²

1.中国科学技术大学计算机科学与技术学院,合肥 230022
2.合肥天帷信息安全技术有限公司,合肥 230000

收稿日期:2021-06-10 出版日期:2021-08-10 发布日期:2021-09-01
通讯作者: 陈凯杰 E-mail:ckjkevin@mail.ustc.edu.cn
作者简介:陈凯杰（1997—）,男,安徽,硕士研究生,主要研究方向为区块链安全、形式化方法|熊焰（1960—）,男,安徽,教授,博士,主要研究方向为网络安全、漏洞挖掘、形式化建模|黄文超（1982—）,男,湖北,副教授,博士,主要研究方向为网络安全、漏洞挖掘、形式化建模|武建双（1984—）,男,山西,硕士,主要研究方向为网络安全等级保护
基金资助:
国家自然科学基金(61972369);国家重点研发计划(2018YFB2100301)

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

CHEN Kaijie¹(), XIONG Yan¹, HUANG Wenchao¹, WU Jianshuang²

1. Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230022, China
2. Hefei Tianwei Information Security Technology Co., Ltd., Hefei 230000, China

Received:2021-06-10 Online:2021-08-10 Published:2021-09-01
Contact: CHEN Kaijie E-mail:ckjkevin@mail.ustc.edu.cn

摘要/Abstract

摘要：

区块链共识协议是一种确保区块链网络中不同节点的数据达成一致的重要机制,随着区块链应用的爆发性增长,针对区块链共识协议的攻击不断出现。文章提出一种基于拜占庭容错的PoS共识协议形式化分析方法,通过归纳建模共识节点整体状态迁移解决协议模型状态空间爆炸问题,同时结合实际安全威胁形式化建模信道模型和攻击者模型,根据协议一致性要求形式化描述两大类安全属性并进行形式化验证。实验结果表明,该类协议具有拜占庭容错能力。最后,文章分析了针对0确认交易的双花攻击所需的条件,并提出防护方法。

关键词: 区块链共识协议, 拜占庭容错, 归纳建模, 形式化分析

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

中图分类号:

TP309

陈凯杰, 熊焰, 黄文超, 武建双. 一种基于拜占庭容错的PoS共识协议形式化分析方法[J]. 信息网络安全, 2021, 21(8): 35-42.

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.

图/表 9

图1

图2

图3

表1

表2

表3

表4

表5

图4

参考文献 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₎	×	√	√

一种基于拜占庭容错的PoS共识协议形式化分析方法

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

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

图/表 9

参考文献 20

相关文章 6

编辑推荐

Metrics

本文评价

[1]	姚萌萌, 唐黎, 凌永兴, 肖卫东. 基于串空间的安全协议形式化分析研究[J]. 信息网络安全, 2020, 20(2): 30-36.
[2]	郑敏, 王虹, 刘洪, 谭冲. 区块链共识算法研究综述[J]. 信息网络安全, 2019, 19(7): 8-24.
[3]	吕宗平, 丁磊, 隋翯, 顾兆军. 基于时间自动机的工业控制系统网络安全风险分析[J]. 信息网络安全, 2019, 19(11): 71-81.
[4]	姚萌萌, 朱正超, 刘明达. 一种改进的基于认证测试的形式化分析方法[J]. 信息网络安全, 2019, 19(1): 27-33.
[5]	余磊, 魏仕民, 江明明. 基于主体关联度的安全协议形式化分析方法[J]. 信息网络安全, 2018, 18(6): 45-51.
[6]	朱鹏飞, 张利琴, 李伟, 于华章. 交互型电子签名的形式化分析[J]. 信息网络安全, 2016, 16(9): 31-34.