Dynamic Logic with Parallel Operator for Verifying Communication Protocols
Source: arXiv:2607.20180 · Published 2026-07-22 · By Luiz C. F. Fernandez, Mario R. F. Benevides
TL;DR
This paper addresses the formal verification of cryptographic communication protocols, focusing on reasoning about authenticity and safety properties under adversarial conditions. It presents Dynamic Dolev-Yao Logic (DDYL), an extension of Propositional Dynamic Logic (PDL) with parallel composition operators enriched by concepts from the Dolev-Yao intruder model. The key contribution lies in combining program actions, communication, concurrency, and cryptographic deductions in a unified formal framework. The authors provide a complete axiomatization of this logic and introduce a tailored tableaux calculus for it, proving soundness, completeness, and termination properties rigorously. An example involving encrypted messages between an agent and an intruder illustrates the logic's practical verification capability. This work bridges logical program reasoning with classical intruder models to enable more expressive and automated reasoning about security properties in communication protocols.
Key findings
- DDYL combines process algebra style parallel operators and communication actions with dynamic logic to model cryptographic protocols under an active intruder.
- The logic is completely axiomatizable by integrating PDL axioms with Dolev-Yao epistemic axioms, soundness and completeness follow directly from prior results.
- The proposed tableaux calculus extends existing prefixed tableau methods with rules for encryption, decryption, pairing, and parallel composition, integrating intruder reasoning.
- Soundness and completeness of the tableaux calculus are formally proved through preservation of satisfiability and construction of models from open branches.
- Termination of the tableaux procedure is guaranteed by loop checking and prefix reduction strategies adapted from modal logic tableaux.
- Example 2 demonstrates the intruder’s ability to derive secret M in a parallel composition protocol scenario, showing the practical applicability of the method.
- The Expansion Law for parallel composition (Theorem 1) is utilized to faithfully capture concurrent protocol executions in logical formulas.
- The tableaux rules handle communication actions including ε-transitions (τ) and termination (END), modeling protocol communication steps precisely.
Threat model
An active Dolev-Yao intruder with full network control can intercept, modify, replay, and inject messages arbitrarily. The intruder can perform logical deductions based on intercepted messages and known keys but cannot break cryptographic primitives (modeled as perfect encryption). The system assumes honest agents follow the protocol and possess private keys securely. The adversary’s unknown is the content of encrypted messages where keys are unknown unless deduced logically. This matches the classical symbolic intruder model widely used in formal protocol analysis.
Methodology — deep read
Threat Model & Assumptions: The adversary corresponds to a Dolev-Yao intruder with capabilities to intercept, initiate, and alter messages using perfect cryptographic primitives. The model assumes agents with private/public key pairs, and the intruder operates under a deductive system reflecting standard inference rules (e.g., decryption with corresponding private keys). The adversary is assumed to control the network, enabling concurrency and interaction but cannot break encryption by cryptanalysis.
Data / Formal Objects: The logic formulas are constructed over a countable set of propositions, finite sets of agents and cryptographic keys, and process terms involving communication actions. States represent protocol configurations; transitions model communication or internal steps.
Architecture / Algorithm: DDYL extends standard Propositional Dynamic Logic (PDL) by introducing a parallel composition operator (∥) inspired by process algebras. Protocol processes are modeled as sequences, choices, tests, and parallel executions of action-labeled transitions, with semantics given via labeled transition relations in Kripke-style models. The valuation function enforces cryptographic semantic properties (e.g., knowledge of encrypted messages implies knowledge of keys and plaintexts).
Training / Implementation Regime: N/A (logic and calculus development rather than statistical training).
Evaluation Protocol: The authors develop a prefixed tableaux calculus extending prior methods to handle the new operators and semantics. Soundness is shown by demonstrating rules preserve satisfiability of branches. Completeness is proved by constructing models from open, complete tableau branches. Termination is ensured by loop-checking via prefix reductions and copy detection. The calculus is demonstrated with an explicit example of a Man-in-the-Middle style protocol involving agent A and intruder Z.
Reproducibility: The paper does not release code or datasets as it is a theoretical logic contribution. The inference rules, axioms, and calculus are formally defined and proofs are sketched or referenced for completeness.
Concrete Example Walkthrough: The example protocol where agent A sends encrypted messages to intruder Z is modeled by parallel processes πA and πZ interacting over communication ports with message expressions constructed from agents and keys. The tableaux procedure is applied stepwise, using rules for parallel composition expansions, encryption/decryption axioms, and communication actions, ultimately deriving a closed tableau indicating the intruder can access the secret message M. This illustrates the procedure's ability to verify protocol properties under intruder interference.
Technical innovations
- Integration of Dolev-Yao intruder model concepts into Propositional Dynamic Logic extended with parallel operators for concurrency.
- Complete axiomatization combining epistemic logic for knowledge with dynamic logic for communication and process actions.
- Prefixed tableaux calculus extended with novel rules for encryption, decryption, pairing, and parallel composition that preserve satisfiability and allow automated proof search.
- Formal proof of termination based on prefix reduction and loop checking adapted to the extended logic with concurrency.
- Use of the Expansion Law tailored for parallel operators to decompose concurrent protocol executions into summations of labeled action sequences.
Limitations
- The logic excludes iteration and while constructs due to increased computational complexity; these are noted as future work.
- No implementation or performance benchmarks of the tableaux method on realistic or industrial-scale protocols.
- No empirical evaluation with explicit adversarial simulation or adaptation to probabilistic or computational cryptography models.
- Completeness and soundness proofs rely heavily on prior work, so the novelty is in integration rather than new foundational proofs.
- The method addresses symbolic Dolev-Yao intruder capabilities but not side-channel, timing, or cryptanalytic attacks.
Open questions / follow-ons
- How can iteration and while constructs be integrated into the logic and tableaux method without exploding computational complexity?
- What is the exact computational complexity class of the validity and model checking problems for DDYL?
- How can the framework be extended or adapted to computational (probabilistic) cryptographic models beyond symbolic Dolev-Yao?
- Can the method scale to more complex multi-party protocols or real-world protocol standards with richer state spaces?
Why it matters for bot defense
For practitioners in bot defense and CAPTCHA systems, this paper provides a rigorous formal framework for reasoning about the security and authenticity of communication protocols subject to adversarial interference. While not directly about CAPTCHA or bot detection, the logic and tableaux approach enable precise symbolic analysis of protocol steps where attacker actions are modeled explicitly, including concurrent interactions. This can inform design and verification of challenge-response protocols, authentication handshakes, or nonce-based schemes that underlie bot defenses. The integration of concurrency operators supports reasoning about parallel or overlapping protocol executions, which is relevant to real-world systems interacting with multiple clients or bots simultaneously. However, the symbolic Dolev-Yao setting abstracts away from computational subtleties and practical deployment constraints common in bot defense engineering. Nevertheless, adopting such formal verification techniques can improve confidence in proposed CAPTCHA or challenge protocols by detecting subtle attack vectors related to concurrency and intruder manipulation of messages early in the design.
Cite
@article{arxiv2607_20180,
title={ Dynamic Logic with Parallel Operator for Verifying Communication Protocols },
author={ Luiz C. F. Fernandez and Mario R. F. Benevides },
journal={arXiv preprint arXiv:2607.20180},
year={ 2026 },
url={https://arxiv.org/abs/2607.20180}
}