arXiv subjects

Xianhui Lu

Publications and source records attributed to Xianhui Lu.

3 recordsLinked to original sources

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↗

arXiv2023

Approaching Shannon's One-Time Pad: Metrics, Architectures, and Enabling Technologies

The rapid development of advanced computing technologies such as quantum computing imposes new challenges to current wireless security mechanism which is based on cryptographic approaches. To deal with various attacks and realize long-lasting security, we are in urgent need of disruptive security solutions. In this article, novel security transmission paradigms are proposed to approach Shannon's one-time pad perfect secrecy. First, two metrics, termed as Degree-of-Approaching (DoA) and Degree-of-Synchronous-Approaching (DoSA), are developed to characterize the closeness between the achieved security strength and perfect secrecy. These two metrics also serve as a guideline for secure transmission protocol design. After that, we present two paths towards Shannon's one-time pad, i.e., an explicit-encryption based approach and an implicit-encryption based approach. For both of them, we discuss the architecture design, enabling technologies, as well as preliminary performance evaluation results. The techniques presented in this article provide promising security-enhancing solutions for future wireless networks.

cs.CR↗