Rui Zhang

Yihang Jiang, Xiaoyang Li, Guangxu Zhu et al.

The emergence of the \textit{low-altitude economy} (LAE) calls for highly integrated and reliable wireless systems that can simultaneously support \textit{communication and sensing} (C\&S) functions. Although \textit{integrated sensing and communication} (ISAC) has been widely studied, most existing works focused on link-level or single-cell architectures in terrestrial environments, leaving the potential of network-level cooperative air-ground ISAC largely unexplored. To bridge this gap, a heterogeneous air-ground ISAC network architecture based on \textit{coordinated multipoint} (CoMP) is proposed, which incorporates a cooperative hybrid mono/bi-static sensing scheme to enhance spatial diversity and sensing capability. In the proposed architecture, a two-tier \textit{base station} (BS) deployment is adopted: master BSs are arranged in a hexagonal lattice, while slave BSs follow a Poisson point process distribution. This structure concurrently supports communication for terrestrial users and sensing for aerial targets. A holistic performance analysis framework for both C\&S is further developed, accounting for key channel and network parameters. Simulation results reveal inherent trade-offs between C\&S performance, especially under multi-BS cooperation and varying network density. These findings provide practical guidance for the deployment of scalable and efficient ISAC networks in LAE scenarios.

Zhaoxuan Li, Qionglu Zhang, Hengyuan Liu et al.

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.