2026/07/18 by Luiz C. F. Fernandez, Mario R. F. Benevides
Computer Science · #Advanced Authentication Protocols Security #Communications protocol #Cryptographic protocol #Description logic #Dynamic logic (digital electronics) #Formal Methods in Verification #Linear temporal logic #Logic, Reasoning, and Knowledge #Multimodal logic #Operator (biology) #Protocol (science) #Temporal logic
paper · pdf · doi:10.4204/eptcs.449.4
published in Electronic Proceedings in Theoretical Computer Science 449, 55-70 (Open Publishing Association)
openalex publication_date 2026/07/18 · openalex created_date 2026/07/24 · openalex updated_date 2026/08/05
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.