Search arXiv⌕ Search

arXiv · 2611.07170

Global Surveillance Under the Lens: Reconstructing Passive Dolev-Yao Intruders

Abstract

Global surveillance systems record large volumes of network traffic for retrospective analysis, but packet captures alone reveal little about protocol-level semantics. This paper presents an automated, specification-guided methodology for reconstructing passive Dolev-Yao intruder executions from captured network traffic and validating the reconstructed executions against a formal protocol specification. The framework takes a PCAP capture, an AnBx specification, and the associated deployment metadata; it extracts Java-serialised objects from TCP streams, reconstructs protocol sessions and channel-to-step assignments, and generates a passive intruder that evaluates the Dolev-Yao derived checks produced by the AnBx compiler. Three reconstruction challenges are addressed: multiple serialised objects and object references within a TCP stream, ambiguity in mapping interleaved connections to concurrent protocol sessions, and semantic validation of candidate reconstructions. We evaluate the methodology on 121 protocols from the AnBx test suite. For single-session captures, the standard JDK cryptographic provider recovers 97.8% of expected objects and achieves 94.2% successful reconstruction, where success requires complete object recovery and a clean passive-intruder execution. For the 112 parallel-capable protocols, the toolchain achieves 89.3% successful reconstruction for both two and three concurrent sessions, while recovering approximately 97.2% of expected objects. Experiments with mismatched protocol-role mappings and deliberately mutated traces show that the generated Dolev-Yao checks respond to semantic inconsistencies. By making the reconstruction step explicit, the solution produces protocol-level observations on which assessments of protocol resilience and the design of defensive countermeasures can be built.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Paolo Modesti. 2026-11-04. Global Surveillance Under the Lens: Reconstructing Passive Dolev-Yao Intruders. https://arxiv.org/abs/2611.07170

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

How to Backdoor Image Knowledge Distillation

Knowledge distillation is widely used to transfer behavior from a large teacher model to a smaller student. It is often assumed to be safe when the teacher is clean, because classic backdoor attacks rely on poisoned labels and triggers in supervised training, whereas distillation trains the student to match a teacher's outputs. We show that this assumption can fail when the distillation dataset itself is poisoned. Our attack injects triggered and manipulated images that a clean teacher already predicts as an attacker chosen target label, which causes the student to learn a backdoor even though the teacher remains unaffected. We evaluate this threat across multiple manipulation strategies, including targeted adversarial perturbations and targeted GAN based class transitions, and study how distillation settings influence both accuracy and attack success. We show that the attack remains effective even at a 10% poisoning rates. The results demonstrate that a clean teacher alone is not a sufficient safeguard: poisoned distillation data can produce a strongly backdoored student while maintaining competitive performance on clean images. These findings show that the integrity and provenance of distillation data are part of the security boundary of data intensive KD pipelines, even when the teacher itself is trusted.

cs.CR↗

Cryptanalysis of Isogeny-Based Quantum Money with Rational Points

Quantum money is a representative application in cryptography that utilizes quantum technology to achieve security that is unattainable with classical systems. Since the theoretical proposal by Wiesner in 1983, the most recent instantiation is the quantum money using class group actions on elliptic curves, proposed by Montgomery and Sharif in Asiacrypt'24. In this work, we propose a concrete cryptanalysis by leveraging the efficiency of evaluating division polynomials with the coordinates of rational points, offering a speedup of $O(\log^4p)$ compared to the brute-force attack. While the resulting attack still runs in exponential time, our method provides the first nontrivial algorithmic insight into their structural hardness. Furthermore, due to the algebraic properties of rational points and quadratic twists, our technique naturally yields a more efficient verification procedure for the underlying quantum money. We believe this new line of analysis opens promising directions for future research in elliptic-curve-based quantum cryptography.

cs.CR↗

Federated Learning in the Wild: A Comparative Study for Cybersecurity under Non-IID and Unbalanced Settings

Machine Learning (ML) techniques have shown strong potential for network traffic analysis; however, their effectiveness depends on access to representative, up-to-date datasets, which is limited in cybersecurity due to privacy and data-sharing restrictions. To address this challenge, Federated Learning (FL) has recently emerged as a novel paradigm that enables collaborative training of ML models across multiple clients while ensuring that sensitive data remains local. Nevertheless, Federated Averaging (FedAvg), the canonical FL algorithm, has shown poor convergence in heterogeneous environments characterised by non-independent and identically distributed (i.i.d.) data distributions and unbalanced dataset sizes across clients, conditions frequently observed in cybersecurity contexts. To overcome these challenges, several alternative FL algorithms have been developed, yet their applicability to network intrusion detection remains insufficiently explored. This study systematically evaluates a range of FL algorithms in the context of network intrusion detection for DDoS attacks. Using a dataset of recent network attacks, the evaluation considers detection performance, training time, and communication overhead under non-i.i.d. settings, providing practical insights into the selection of FL solutions for network intrusion detection.

cs.CR↗