Migrating to Hybrid Cryptography in Practice: The TutaCrypt Protocol and Its Security

Tlcp hardening with formal analysis and post-quantum design

Transport Layer Cryptography Protocol (TLCP) is a secure communication protocol developed in China, featuring a dual-certificate architecture and incorporating ShangMi cryptographic algorithms. It has been widely deployed in security-critical domains such as finance, government, and energy. Despite its practical significance, TLCP did not undergo comprehensive formal analysis during its standardization process, leaving potential design-level vulnerabilities insufficiently explored. Moreover, the advent of quantum computing poses fundamental challenges to the classical cryptographic primitives employed by TLCP, motivating the need for both systematic security evaluation and post-quantum enhancements. To address these gaps, we first construct the comprehensive formal model of TLCP, covering certificate-based and identity-based cipher suites as well as its distinctive dual-certificate mechanism, under a realistic threat model and security assumptions that capture both classical and quantum adversaries. Based on this model, we conduct an automated security analysis using ProVerif, identifying nine potential attack vectors and deriving five concrete mitigation recommendations. Finally, motivated by the analysis results and the limitations of incremental fixes against quantum threats, we propose KEMTLCP, a post-quantum secure variant of TLCP that leverages key encapsulation mechanisms (KEMs) for both key exchange and authentication while preserving TLCP’s architectural principles through a novel explicit authentication mechanism. We further provide a security proof for the core authentication mechanism, show that KEMTLCP effectively mitigates the majority of identified vulnerabilities through formal analysis, and evaluate its practical performance.

SUST Journal of Science and Technology

Formal Security Analysis of the Olvid Messenger

Privacy Pass is Anamorphic: Practical Consequences and Attacks in the Black-box Model

It is proved that the three most prominent variants of Privacy Pass are anamorphic, which makes it insecure in a model where user's device or client application is working against them and can also be used to achieve a private metadata-like functionality.

FINGERTRAP: A Self-Defending Cryptographic Protocol for Network Communications

Fingertrap is a network encryption and authentication protocol that extends the X3DH and Double Ratchet frameworks with three novel mechanisms inspired by the Chinese finger trap (zhĭ wăng): a friction ratchet that exponentially increases computational cost for each failed authentication attempt; a recursive annihilation protocol that irreversibly destroys all cryptographic state after a configurable failure threshold; and a commit-then-challenge handshake that requires a counterintuitive “inward” action for legitimate authentication. A bidirectional weave hash extends the Double Ratchet’s transcript binding to cover every message in both directions. Together, these mechanisms provide per-message forward secrecy, post-compromise security (self-healing), clock-free operation, and a self-destruct capability. The individual ingredients-client puzzles, key erasure, and ratcheting-each build on established lines of work; their combination into a single stateful protocol, in which failed authentication attempts cryptographically tighten the session state and ultimately destroy it, is not to our knowledge offered by deployed transport protocols such as TLS 1.3, Signal, or WireGuard. The design targets deployments in which interception or capture of a device implies endpoint compromise, such as Unmanned Aerial Vehicle (UAV) telemetry links and body-worn sensors, where denial of exploitation requires guaranteed loss of past and future session material. We describe the full protocol, provide game-based security arguments under an explicit adversarial model, give analytic cost estimates for the friction mechanism, analyse the denial-of-service surface and a two-layer mitigation strategy, and specify a post-quantum extension using hybrid X25519/ML-KEM-768 ratcheting.

Post-Quantum Cryptography Migration in Internet Protocols: A Review of ML-KEM Hybrid Key Exchange in TLS and SSH

Internet public-key cryptography faces long-term risk from quantum computers, especially when traffic can be collected now and decrypted later. After the NIST post-quantum cryptography standards, the deployment task has shifted from algorithm selection to protocol migration. This paper reviews ML-KEM hybrid key exchange in TLS and SSH through a standards-first narrative review and protocol comparison. It synthesizes NIST standards, RFCs and IETF drafts, experiments, measurements, and primary deployment reports. The paper develops a deployment-readiness framework with four layers: security continuity, protocol integration, operational observability, and crypto-agility. The analysis shows hybrid key exchange represents the most feasible short-term solution, as it introduces post-quantum confidentiality without discarding existing elliptic curve security guarantees. However, hybrid deployment does not provide full post-quantum security. The review argues that readiness depends on protocol binding, implementation behavior, monitoring, and governance as much as on algorithm strength. Handshake size, middlebox compatibility, implementation safety, telemetry, authentication migration, and organizational crypto-agility determine whether migration can progress without weakening current Internet security.