近日，中国科学院大学密码学院在大语言模型辅助安全协议形式化建模与自动修复领域取得最新研究进展。由密码学院博士研究生张世聪作为第一作者撰写的论文《ProtoCase: Case-Based Repair for LLM-Generated Security Protocol Models》被 The 34th International Conference on Case-Based Reasoning（ICCBR 2026）接收。该研究聚焦大语言模型生成安全协议形式化模型过程中容易出现的结构和语义缺陷问题，提出了基于案例推理（Case-Based Reasoning, CBR）的自动修复框架，为安全协议形式化建模提供了新的思路。
ICCBR 2026于2026年8月13日至16日在德国不来梅举行。2026年8月，张世聪代表研究团队参会，并在大会上就该项研究工作作了学术报告。
Abstract: Recent pipelines use LLMs to generate Tamarin/SAPIC+ security protocol models from natural language, and the resulting models frequently contain structural and semantic defects that compromise verification and require systematic repair. We identify four conditions under which case-based reasoning can control the repair of such models: a finite operator space, decomposable adaptation, bounded LLM delegation, and deterministic verifier feedback. We present ProtoCase, a framework that instantiates these conditions in three phases: deterministic preconditioning, a single LLM call guided by a retrieved case, and deterministic cleanup. A quality-gated retain step feeds verified repairs into the case base so that subsequent retrievals return format-matched cases. In leave-one-out experiments on 18 benchmark protocols, single-pass repair produces models whose security properties match hand-crafted references for 11 of 18 protocols (from a baseline of 8 of 18), and retention raises this to a median of 15 of 18 over five random case-base orderings, outperforming a RAG baseline at 5 of 18. Results hold across five LLM backends.
论文信息：Shicong Zhang: “ProtoCase: Case-Based Repair for LLM-Generated Security Protocol Models,” in The 34th International Conference on Case-Based Reasoning（ICCBR 2026）
