TL;DR
The first formal security analysis of the cryptographic core of Olvid, an end-to-end encrypted messaging app notably used by French government officials, including ministers, shows that Olvid is not secure in modern security models such as eCK and reveals a potential timing leakage.
This work presents the hybrid key establishment protocol TutaCrypt in a form that enables rigorous cryptographic analysis and defines two Bellare–Rogaway-style security models that precisely characterize the provided security guarantees.
The 5G EAP-TLS protocol is one of the three protocols standardised by 3GPP for use in 5G networks. Although this protocol inherently ensures security, authentication, and data integrity, recent studies have shown that it still faces several vulnerabilities, including Man-in-The-Middle attacks, user impersonation, and replay attacks. This paper presents a detailed description of the steps in the modified EAP-TLS protocol, which addresses these issues by directly binding the digital certificate to the subscriber’s SUCI identity to prevent user impersonation, binding the session key to both the certificate and the identity to ensure resistance against Man-in-The-Middle attacks, and introducing a nonce value to prevent the reuse of old packets in replay attacks. The paper employs the Proverif tool as a formal verification approach to evaluate the security of the modified 5G EAP-TLS protocol. The verification outcomes indicate that the proposed protocol satisfies the specified security properties, including the confidentiality of the session key (KSESSION), the subscriber identity (SUPI), the pre-master key (RPREKEY), as well as other relevant security requirements.
A hybrid key exchange protocol combining DHKE with Learning With Errors (LWE), a lattice-based post-quantum primitive that provides authentication via a Public Key Infrastructure together with CRYSTALS-Dilithium digital signature, resilience against MITM attacks, and robustness against classical and quantum threats.
The Agent2Agent (A2A) protocol, now governed by the Linux Foundation, is an open standard that enables autonomous AI agents to discover, authenticate with, and delegate tasks to one another across organizational boundaries. Designed to complement the Model Context Protocol (MCP) for tool integration, A2A is rapidly emerging as the horizontal communication layer of the multi-agent ecosystem. Yet the protocol's security has received no systematic analysis. This paper presents A2ABreak, the first rigorous systematic security analysis of the A2A protocol. We introduce a novel framework that utilizes an LLM-assisted extraction of a verified finite-state machine directly from the natural-language specification, producing a unified model of 37 states and 76 transitions from 929 formalized statements, and then systematically reasons over this model to discover protocol-level vulnerabilities through adversarial verification, under a full-compliance assumption. Our analysis uncovers 11 new vulnerabilities, each exploitable by a specification-compliant adversary without requiring any implementation flaw. Among the findings are cross-client context injection through unprotected context identifiers, credential harvesting via multi-hop identity loss in delegation chains, and data exfiltration through rogue agents advertising unattested capability claims. A2ABreak achieves 73.3% precision and 84.6% F1 against independent expert review, while a zero-shot LLM baseline operating over the same specification produces zero confirmed findings, demonstrating that explicit formal grounding is essential for sound protocol security analysis.
The Secure Hardware Extension (SHE) provides crucial functionalities such as error-detection, authorization, and authentication of messages exchanged between Electronic Control Units (ECUs) over the Controller Area Network (CAN) bus with the help of Advanced Encryption Standard (AES) cryptographic cores. However, the security guarantees of SHE can be entirely compromised if an adversary with physical access to the vehicle extracts the secret key using power or electromagnetic side-channel measurements. While countermeasures like Threshold Implementation (TI) and Domain-Oriented Masking (DOM) offer robust protection, they are impractical for SHE due to the stringent resource constraints and real-time safety requirements of automotive systems. To address this critical vulnerability, this article explores the concept of re-keying, utilizing two rounds of AES hardware as a lightweight key derivation function. This approach eliminates the need for additional key exchanges between the sender and receiver. Our experimental results, supported by theoretical analysis, indicate that re-keying every 10 encryptions provides a practical and secure solution that limits the effectiveness of side-channel attacks; leakage analysis performed on over 1,000,000 electromagnetic (EM) traces for this configuration revealed no detectable leakage. These findings are supported by real-world side-channel attack experiments conducted on a prototype implemented on the Cora-Z7 platform, built on Xilinx’s Zynq-7000 system featuring a single or dual-core 667 MHz ARM Cortex-A9 processor and Artix-7 FPGA. The proposed lightweight architecture, named LISHARK, maintains the same area footprint as a standalone AES core, making it significantly more efficient compared to TI and DOM. Measurements show that when integrated with the Secure Onboard Communication (SecOC) protocol, the design achieves end-to-end message authentication in approximately 90 microseconds, well within the industry-standard threshold of 10 milliseconds.
PEACE is presented, an authentication mechanism for blockchains that combines the practicality of traditional Web systems with decentralization and privacy-preservation, building on a recent groundbreaking zkLogin protocol.
We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.
