Qionglu Zhang | Searcharxiv

arXiv2026

A Drop-in KEM Replacement for Client Signatures in Post-Quantum SSH

The transition to post-quantum cryptography is reshaping the Secure Shell (SSH) protocol for remote administration. Post-quantum key exchange has been deployed in OpenSSH and is being standardized, while SSH authentication largely remains a signature-replacement effort. This path preserves the familiar public-key credential model, but inherits the size and computation overhead of post-quantum signatures, which can increase latency, traffic, and server-side load. KEM-based authentication offers a natural alternative to this signature-centric path, and SSH makes this especially attractive at the user-authentication layer, which is method-extensible, separated from transport-layer key exchange and host-key authentication, and already protected by the established channel. We present a drop-in KEM-based user-authentication method for SSH that replaces client public-key signatures with a session-bound challenge-response proof. The method fits into SSH's existing user-authentication framework, preserving the public-key credential model and enabling incremental deployment alongside existing methods. We provide a reduction-based security argument in the post-quantum ACCE framework, implement the design in OpenSSH using liboqs, and evaluate it under representative RTTs, TCP initial-window settings, and post-quantum migration configurations. Our results show that KEM-based authentication is competitive with compact signature-based authentication under representative network settings, while reducing median handshake latency by up to about 10% against large-signature hybrid baselines. The advantages are clearer when post-quantum signatures stress transmission or computation: median latency under small TCP initial windows falls by up to 7.3% versus ML-DSA and 17.9% versus SLH-DSA, while server-side online cryptographic cost is 59.1% lower than that for ML-DSA in the same NIST category.

cs.CR↗

arXiv2026

CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes

Manual formal analysis of cryptographic schemes is labor-intensive and requires substantial expertise. While model-checking tools (e.g., Scyther and Tamarin) and computational-security tools (e.g., CryptoVerif and EasyCrypt) improve the automation of security proofs, they still rely on experts to abstract schemes and write tool-specific formal descriptions. Large language models (LLMs) are a promising alternative, but their effectiveness in this domain remains unexplored due to the absence of standardized evaluation methodologies. To fill this gap, we introduce CrypFormBench (C.F.B for short), a comprehensive benchmark jointly covering symbolic and computational security to evaluate five core LLM capabilities: interpretation, generation, completion, transformation, and correction. It comprises 700 instances spanning 677 schemes, 7 mainstream formal verifier languages, and 160 security properties. The evaluation of 9 state-of-the-art LLMs reveals that most of them perform well on interpretation and completion, given their code-awareness advantages, but struggle with generation, transformation, and correction. Overall, their performance remains limited, with Claude-3.5 achieving the highest score at 48.7 out of 100. We further provide practical guidance, e.g., few-shot prompting, Pass@K sampling, and lightweight fine-tuning, to mitigate the executability bottleneck and improve tool-usable outputs. Taken together, our benchmark and analyses offer a grounded view of current progress and concrete directions toward reliable LLM-assisted formal cryptographic analysis.

cs.CR↗