PCL-Based HZ Logic and Its Automated Verification Method

doi:10.3969/j.issn.1671-1122.2026.05.012

Abstract

Abstract:

With the rapid development of new technologies, the complexity of security protocols has been increasing, posing unprecedented challenges for formal analysis. In recent years, automated verification technology has made significant progress in the field of security protocol security testing, becoming a hot research topic. This paper proposed a PCL-based HZ logic and its automated verification method, and demonstrated the effectiveness of the proposed method in verifying the confidentiality and authentication of communication protocols through the application case of the provably secure and lightweight authentication (PSLA) protocol. By constructing an attacker model, this paper simulates eavesdropping attacks, man-in-the-middle attacks, and replay attacks, and automatically verifies the security of PSLA under different attack scenarios. This provides an efficient and automated solution for the security analysis of secure authentication protocols, enhancing the security and practicality of protocol design.

Key words: HZ logic, protocol composition logic, security protocol, attack model, automated verification

CLC Number:

TP309

ZHANG Zhengzhuo, WU Qianqian, YUAN Yubo, HUANG Xin. PCL-Based HZ Logic and Its Automated Verification Method[J]. Netinfo Security, 2026, 26(5): 819-830.

Figures/Tables 6

References 25

[1]	Ge Yi, Huang Wenchao, Xiong Yan. Research on Formal Auxiliary Modeling Based on Secure Protocol Code[J]. Application Research of Computers, 2023, 40(4): 1189-1193, 1202.
	葛艺, 黄文超, 熊焰. 基于安全协议代码的形式化辅助建模研究[J]. 计算机应用研究, 2023, 40(4):1189-1193,1202.
[2]	BRAUER W, REISIG W, ROZENBERG G. Petri Nets: Central Models and Their Properties: Advances in Petri Nets 1986, Part I Proceedings of an Advanced Course Bad Honnef, 8-19. September 1986[M]. Heidelberg: Springer, 2006.
[3]	Yin Anqi, Guo Yuanbo, Wang Ding, et al. Provably Secure Anti-quantum Two-server Password Authenticated Key Exchange Protocol[J]. Journal on Communications, 2022, 43(3): 14-29. doi: 10.11959/j.issn.1000-436x.2022052
	尹安琪, 郭渊博, 汪定, 等. 可证明安全的抗量子两服务器口令认证密钥交换协议[J]. 通信学报, 2022, 43(3):14-29. doi: 10.11959/j.issn.1000-436x.2022052
[4]	Paulson L C.Proving Properties of Security Protocols by Induction[C]// IEEE. The 10th Computer Security Foundations Workshop. New York: IEEE, 1997: 70-83.
[5]	Gong Xiang, Feng Tao, Du Jinze. Formal Modeling and Security Analysis Method of Security Protocols Based on CPN[J]. Journal on Communication, 2021, 42(9): 240-254.
	龚翔, 冯涛, 杜谨泽. 基于CPN的安全协议形式化建模及安全分析方法[J]. 通信学报, 2021, 42(9):240-253. doi: 10.11959/j.issn.1000-436x.2021175
[6]	Zhong Xiaomei, Xiao Meihua, Li Wei, et al. Formal Analysis and Improvement of RFID Ultra-Lightweight Authentication Protocol RCIA[J]. Chinese Journal of Electronics, 2018, 28(12): 2183-2192.
	钟小妹, 肖美华, 李伟, 等. RFID超轻量级认证协议RCIA形式化分析与改进[J]. 计算机工程与科学, 2018, 28(12):2183-2192.
[7]	Burrows M, Abadi M, Needham R. A Logic of Authentication[J]. ACM Transactions on Computer Systems (TOCS), 1990, 8(1): 18-36. doi: 10.1145/77648.77649 URL
[8]	Yao Mengmeng, Tang Li, Ling Yongxing, et al. Research on Formal Analysis of Security Protocols Based on Strand Space[J]. Information Network Security, 2020, 20(2): 30-36.
	姚萌萌, 唐黎, 凌永兴, 等. 基于串空间的安全协议形式化分析研究[J]. 信息网络安全, 2020, 20(2):30-36.
[9]	Burrows M, Abadi M, Needham R. A logic of authentication[J]. The Royal Society of London. Series A, Mathematical and Physical Sciences. 1989, 426(1871): 233-271.
[10]	LI Gong, Needham R M, Yahalom R.Reasoning about Belief in Cryptographic Protocols[C]//IEEE. IEEE Symposium on Security and Privacy. New York: IEEE, 1990: 234-248.
[11]	Abadi M, Tuttle M R. A Semantics for a Logic of Authentication[C]//ACM. The 10th Annual ACM Symposium on Principles of Distributed Computing. New York: ACM, 1991: 201-216.
[12]	VAN O P. Extending Cryptographic Logics of Belief to Key Agreement Protocols[C]//ACM. The 1st ACM Conference on Computer and Communications Security. New York: ACM, 1993: 232-243.
[13]	Shu Nina, Wang Yadi. Formal Logical Analysis Method of Authentication Protocols—A Review of BAN Logic[J]. Application Research of Computers, 2002, 19(9): 17-20.
	束妮娜, 王亚弟. 认证协议的形式逻辑分析方法——BAN类逻辑综述[J]. 计算机应用研究, 2002, 19(9): 17-20.
[14]	SYVERSON P F, VAN OORSCHOT P C, MEADOWS C. A Unified Logic for Cryptographic Protocols[J]. ACM Transactions on Information and System Security (TISSEC), 1996, 1(1): 3-40. doi: 10.1145/290163.290164 URL
[15]	Cheng Huaqing. Logical Methods and Philosophical Implications of Cryptographic Protocol Analysis[J]. Journal of Guizhou Engineering Application Technology College, 2017, 35(6): 63-68.
	程华清. 密码协议分析的逻辑方法及其哲学意蕴[J]. 贵州工程应用技术学院学报, 2017, 35(6): 63-68.
[16]	Bieber P.A logic of communication in hostile environments[C]//IEEE. The Computer Security Foundations Workshop III. New York: IEEE Computer Society, 1990: 14-22.
[17]	Gaarder K, Snekkenes E. Applying a Formal Analysis Technique to the CCITT X. 509 Strong Two-Way Authentication Protocol[J]. Journal of Cryptology, 1991, 3(2): 81-98. doi: 10.1007/BF00196790 URL
[18]	Datta A, Derek A, Mitchell J C, et al. Protocol Composition Logic (PCL)[J]. Electronic Notes in Theoretical Computer Science, 2007, 172: 311-358. doi: 10.1016/j.entcs.2007.02.012 URL
[19]	MEADOWS C, PAVLOVIC D.Deriving, Attacking and Defending the GDOI Protocol[C]//Springer. The 9th European Symposium on Research in Computer Security (ESORICS 2004). Heidelberg: Springer, 2004: 53-72.
[20]	Zhang Bingtao, Wang Xiaopeng, Wang Lyucheng. A Secure Authentication and Key Agreement Scheme for WMN Based on Protocol Composition Logic[J]. Journal of Computer Applications, 2017, 34(8): 2473-2477.
	张冰涛, 王小鹏, 王履程. 协议组合逻辑安全的WMN认证密钥协商方案[J]. 计算机应用研究, 2017, 34(8):2473-2477.
[21]	Li Xuefeng. Improved Neuman-Subblebine Protocol and Its PCL Proof[J]. Journal of Qinghai University, 2018, 36(6): 46-51.
	李学峰. 改进的Neuman-Stubblebine协议及其PCL证明[J]. 青海大学学报, 2018, 36(6):46-51.
[22]	Chai Sheng, Yin Haotian, Xing Bin, et al. Provably Secure and Lightweight Authentication Key Agreement Scheme for Smart Meters[J]. IEEE Transactions on Smart Grid, 2023, 14(5): 3816-3827. doi: 10.1109/TSG.2023.3234000 URL
[23]	Hoare C A R. Communicating Sequential Processes[M]. Englewood Cliffs: Prentice-Hall, 1985.
[24]	DATTA A. Security Analysis of Network Protocols: Compositional Reasoning and Complexity-Theoretic Foundations[D]. Palo Alto: Stanford University, 2005.
[25]	DOLEV D, Andrew C Y. On the Security of Public Key Protocols[J]. IEEE Transactions on Information Theory, 1983, 29(2): 198-208. doi: 10.1109/TIT.1983.1056650 URL

类别	符号	描述
(动作) α ::=	send X receive X verify u,u, K	发送一个项 X 接收一个项并保存至变量 X中使用密钥 K 验证项 u 的签名
(链) S ::=	[a₁,…,a_n]_P	链内按照顺序执行的动作a₁,…, a_n
(角色) R ::=	(x)S(t)	拥有信息向量和动作向量的参与者
行为	—	等同于动作
线索	—	没有自由变元的串,即行为序列
线索空间	—	线索的多集
事件	—	行为的基本替换实例
迹	trace	一个运行中某些线程的事件列表
全迹	—	单个通信参与者的所有状态集合

符号	含义
${{r}_{A}}$、${{r}_{B}}$	随机数,由用户A和服务器B分别生成,用于生成临时密钥和计算中间值
${{T}_{A}}{{T}_{B}}$	时间戳,用于防止重放攻击,由用户A和服务器B分别生成
$RI{{D}_{A}}$	用户A的身份标识
$se{{S}_{\text{1}}}{{S}_{\text{2}}}{{S}_{A}}{{S}_{B}}$	哈希值
${{t}_{A}}$、${{t}_{B}}$	临时私钥
${{Z}_{A}}{{Z}_{B}}$	哈希值
${{K}_{A}}{{K}_{B}}$	会话密钥
$G$	椭圆曲线上的基点,其阶数为素数
${{d}_{A}}{{d}_{B}}$	私钥
${{P}_{A}}{{P}_{B}}$	公钥
$UV$	在认证和密钥协商阶段计算的两个秘密
${{R}_{A}}{{R}_{B}}$	密钥协商过程中使用的椭圆曲线点,用于在用户和服务器之间安全地交换信息
$X\|\|Y$	x和y的连接
$\oplus $	按位异或运算
${{H}_{\text{1}}}{{H}_{\text{2}}}$	哈希函数
$KDF$	密钥派生函数
$O$	椭圆曲线上的无穷点或零点。在验证步骤中,如果计算结果为零点 O,则验证失败,需要终止协议。该点用于确保计算过程中的正确性和安全性
${{x}_{\text{1}}}{{y}_{\text{1}}}$	由用户A生成的临时椭圆曲线点${{R}_{A}}$的坐标