Search arXiv⌕ Search

arXiv · 0709.1080

On the Protocol Composition Logic PCL

Abstract

A recent development in formal security protocol analysis is the Protocol Composition Logic (PCL). We identify a number of problems with this logic as well as with extensions of the logic, as defined in [DDMP05,HSD+05,He05,Dat05,Der06,DDMR07]. The identified problems imply strong restrictions on the scope of PCL, and imply that some currently claimed PCL proofs cannot be proven within the logic, or make use of unsound axioms. Where possible, we propose solutions for these problems.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Cas Cremers. 2008-02-22. On the Protocol Composition Logic PCL. https://arxiv.org/abs/0709.1080

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

KEEP EXPLORING

Related papers

When Authentication Is Not Enough: Breaking Behavior-Based Driver Authentication Systems

Researchers extensively explored behavior-based driver authentication systems in vehicles. Pushed by advances in Artificial Intelligence (AI), these systems employ powerful models to identify drivers based on unique biometric behaviors. However, existing work prioritizes AI performance metrics, neglecting secure integration with real-world automotive environments and the threat of adversarial attacks that can fool the authentication system. In this paper, we propose for the first evasion attacks against behavior-based driver authentication systems, allowing an attacker to impersonate the legitimate driver. Our attacks exploit long-standing CAN bus weaknesses that allow the injection of forged frames without jeopardizing the attacker's safety while stealing the vehicle. When legitimate data samples are available, we propose \textbf{SMARTCAN}, a safety-aware replay attack. If the attacker can only use the authenticator as an oracle, we propose \textbf{GANCAN}, which trains a Generative Adversarial Network's generator using reinforcement learning on the authenticator's responses. Our attacks achieve a success rate up to 100\% against all the considered models and, in the worst case, require 22 minutes to steal a vehicle. Acknowledging our identified vulnerabilities, we discuss the requirements for a safe and effective deployment of these systems in real-world scenarios.

cs.CR↗

A CRT Framework for Montgomery-Type Modular Reduction

Montgomery reduction is one of the fundamental techniques for efficient modular arithmetic. In this paper, we present a new interpretation of Montgomery-type reduction algorithms through the Chinese Remainder Theorem (CRT). We show that the classical Montgomery reduction algorithm arises naturally from the CRT identity, which further reveals a common algebraic invariant underlying a family of Montgomery-type reduction algorithms. This leads to a unified CRT framework for their derivation, analysis, and verification. Within this framework, several recent variants of Montgomery reduction are interpreted in a uniform manner, their correctness proofs become transparent, and their differences are seen to lie only in the representation of the correction term and the evaluation of a common CRT quotient. The framework also provides a convenient tool for analyzing existing reduction algorithms, allowing incorrect parameter ranges to be identified and counterexamples to be constructed naturally.

cs.CR↗

Cover-Parameterised Multichannel Hybrid Steganography: Compositional Security, Detectability, and Robustness

Secure covert communication across multiple observable channels requires concealing both the transmitted objects and the relationships among them while resisting active manipulation. This paper introduces a cover-parameterised multichannel hybrid steganographic framework that combines message-independent cover synthesis with adaptive cover modification. Synthesised cover-parameter objects condition a keyed QIM-style mask, and the resulting masked payload is embedded into an existing image using QIM-Fused-CF, which integrates fused S-UNIWARD/MiPOD distortion costs, complexity-aware region refinement, SLIC-guided constraints, and syndrome-trellis coding. The protocol distributes each authenticated epoch across three channels and incorporates freshness verification, bounded scheduling, synchronisation, and re-synchronisation. We formalise cover-parameter indistinguishability $(\textsf{CP-IND})$ and unlinkability $(\textsf{CP-UNL})$, multichannel trace indistinguishability $(\textsf{IND-STEGO-MC})$, and an active $\textsf{MC-ATTACK}$ model covering message recovery, replay, and authenticated substitution. The resulting bounds separate masking, embedding, scheduling, authentication, and receiver-state contributions. Experiments on 10,000 BOSSBase images achieve zero bit-error rate for all valid embeddings and structural similarity above $0.9995$ across payloads of $0.10$--$0.40$~bpp. At $0.10$ and $0.20$~bpp, SRM+EC, Ye-Net, and Yedroudj-Net produce AUC values of $0.5017$--$0.5444$ and $0.5424$--$0.5678$, respectively, whereas detectability increases substantially at $0.40$~bpp. These results identify a practical low-to-moderate-payload operating region and demonstrate that secure multichannel steganography requires the joint design of synthesis, masking, embedding, scheduling, authentication, and receiver state.

cs.CR↗