Page 188 - 《软件学报》2026年第6期

吕永阳 等: XCMP 协议的形式化验证与改进: 提升跨链交互安全性 2507

exploit-and-code-how-we-lost-610m-dollar-and-got-it-back-c4a7d0606267
[24] Wormhole. Wormhole incident report. 2022. https://wormholecrypto.medium.com/wormhole-incident-report-02-02-22-ad9b8f21eec6
[25] Miao XL, Chang R, Pna SP, Zhao YW, Jiang LH. Modeling and security analysis of access control in trusted execution environment.
Ruan Jian Xue Bao/Journal of Software, 2023, 34(8): 3637–3658 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/
6612.htm [doi: 10.13328/j.cnki.jos.006612]
[26] Zou SR, Zheng GL. Comparison of Z and VDM with B. Computer Science, 2002, 29(10): 136–138 (in Chinese with English abstract).
[doi: 10.3969/j.issn.1002-137X.2002.10.041]
[27] Saaltink M. The Z/EVES system. In: Proc. of the 10th Int’l Conf. of Z Users. Reading: Springer, 1997. 72–85. [doi: 10.1007/
BFb0027284]
[28] Liu F, Yang J, Li ZB, Qi JY. A secure multi-party computation protocol for universal data privacy protection based on blockchain.
Journal of Computer Research and Development, 2021, 58(2): 281–290 (in Chinese with English abstract). [doi: 10.7544/issn1000-1239.
2021.20200751]
[29] Bowen JP. The Z notation: Whence the cause and whither the course? In: Proc. of the 1st Int’l School on Engineering Trustworthy
Software Systems. Chongqing: Springer, 2014. 103–151. [doi: 10.1007/978-3-319-29628-9_3]
[30] Cao Z, Wang H. Extending interface automata with Z notation. In: Proc. of the 4th Int’l IPM Conf. on Fundamentals of Software
Engineering. Tehran: Springer, 2011. 359–367. [doi: 10.1007/978-3-642-29320-7_25]
[31] Dimou C, Tzima F, Symeonidis AL, Mitkas PA. Performance evaluation of agents and multi-agent systems using formal specifications in
Z notation. In: Proc. of the 10th Int’l Workshop on Agents and Data Mining Interaction. Paris: Springer, 2014. 64–78. [doi: 10.1007/978-
3-319-20230-3_6]
[32] Klein MJ, Sawicki S, Roos-Frantz F, Frantz RZ. On the formalisation of an application integration language using Z notation. In: Proc. of
the 16th Int’l Conf. on Enterprise Information Systems. Lisbon: SCITEPRESS, 2014. 314–319. [doi: 10.5220/0004967003140319]
[33] Jamil A, Murtza Z, Nazir MK, Waseem M, Ghulam Z, Farooq RU. A generic formal specification of an infinite runner games for
handheld devices using Z-notation. In: Proc. of the 4th Int’l Conf. on Computer and Communication Systems (ICCCS). Singapore: IEEE,
2019. 409–413. [doi: 10.1109/CCOMS.2019.8821750]
[34] Oliveira M, Cavalcanti A, Woodcock J. Unifying theories in ProofPower-Z. In: Proc. of the 1st Int’l Symp. on Unifying Theories of
Programming. Walworth Castle: Springer, 2006. 123–140. [doi: 10.1007/11768173_8]
[35] Lv YY, Feng RT, Ma MD, Zhu MQ, Wu HW, Li XH. Reinventing multi-user authentication security from cross-chain perspective. IEEE
Trans. on Information Forensics and Security, 2024, 19: 8908–8923. [doi: 10.1109/TIFS.2024.3463533]
[36] Cremers CJF. The scyther tool: Verification, falsification, and analysis of security protocols. In: Proc. of the 20th Int’l Conf. on Computer
Aided Verification. Princeton: Springer, 2008. 414–418. [doi: 10.1007/978-3-540-70545-1_38]
[37] Song DX. Athena: A new efficient automatic checker for security protocol analysis. In: Proc. of the 12th IEEE Computer Security
Foundations Workshop. Mordano: IEEE, 1999. 192–202. [doi: 10.1109/CSFW.1999.779773]
[38] Zhang SJ, Lee JH. Double-spending with a Sybil attack in the Bitcoin decentralized network. IEEE Trans. on Industrial Informatics, 2019,
15(10): 5715–5722. [doi: 10.1109/TII.2019.2921566]
[39] Psaras I, Tsaoussidis V. Why TCP timers (still) don’t work well. Computer Networks, 2007, 51(8): 2033–2048. [doi: 10.1016/j.comnet.
2006.10.006]
[40] Xu SJ, Zhang LL, Wang LH, Mihaljević MJ, Zhang SH, Shao W, Wang QZ. Relay network-based cross-chain data interaction protocol
with integrity audit. Computers and Electrical Engineering, 2024, 117: 109262. [doi: 10.1016/j.compeleceng.2024.109262]
[41] Lv YY, Li XH, Wang YWB, Chen K, Hou Z, Feng RT. Cross-chain sharing of personal health records: Heterogeneous and interoperable
blockchains. In: Proc. of the 2024 IEEE Int’l Conf. on Bioinformatics and Biomedicine (BIBM). Lisbon: IEEE, 2024. 3588–3591. [doi:
10.1109/BIBM62325.2024.10822679]
[42] Pillai B, Biswas K, Hóu Z, Muthukkumarasamy V. The burn-to-claim cross-blockchain asset transfer protocol. In: Proc. of the 25th Int’l
Conf. on Engineering of Complex Computer Systems (ICECCS). IEEE, 2020. 119–124. [doi: 10.1109/ICECCS51672.2020.00021]
[43] Ding DH, Long B, Zhuo F, Li ZC, Zhang HW, Tian C. Lilac: Parallelizing atomic cross-chain swaps. In: Proc. of the 2022 IEEE Symp.
on Computers and Communications (ISCC). Rhodes: IEEE, 2022. 1–8. [doi: 10.1109/ISCC55528.2022.9912942]
[44] Vishwakarma L, Kumar A, Das D. CrossLedger: A pioneer cross-chain asset transfer protocol. In: Proc. of the 23rd IEEE/ACM Int’l
Symp. on Cluster, Cloud and Internet Computing (CCGrid). Bangalore: IEEE, 2023. 568–578. [doi: 10.1109/CCGrid57682.2023.00059]
[45] Wang F, Wu JL, Nan YH, Aafer Y, Zhang XY, Xu DY, Payer M. ProFactory: Improving IoT security via formalized protocol
customization. In: Proc. of the 31st USENIX Security Symp. Boston: USENIX Association, 2022. 3879–3896.
[46] Yin JQ, Fei Y. FVF-BIoT: A formal verification framework for blockchain-based IoT authentication. Software Quality Journal, 2024,