AI 中文总结
研究用带并行运算符的动态逻辑验证加密协议，通过引入相关概念扩展现有逻辑并获完整公理化，开发表演算并证明其具有终止性、可靠性和完备性，为协议验证提供了有效方法。
AI 中文摘要
本文提出一种带并行运算符的动态逻辑，用于形式化验证加密协议的真实性和安全性属性。该逻辑纳入通信动作，专为在对抗环境中推理协议执行而设计。通过引入源自Dolev - Yao入侵者模型的概念扩展现有带并行运算符的动态逻辑，得到扩展系统的完整公理化。还为该逻辑开发了表演算并证明其终止性、可靠性和完备性。
英文摘要
In this paper, we present a dynamic logic with parallel operators for the formal verification of authenticity and safety properties of cryptographic protocols. The logic incorporates communication actions and is specifically designed to reason about protocol executions in adversarial environments. We extend an existing dynamic logic with parallel operators by introducing concepts derived from the Dolev-Yao intruder model. As the underlying logic is completely axiomatizable, we obtain a complete axiomatization for the extended system. Furthermore, we develop a tableau calculus for the proposed logic and prove its termination, soundness, and completeness.
CommentsIn Proceedings LSFA 2026, arXiv:2607.15904
Journal refEPTCS 449, 2026, pp. 55-70
