Theses and Dissertations

ORCID

https://orcid.org/0000-0003-2182-6496

Advisor

Mittal, Sudip

Committee Member

Zieglar, Edward

Committee Member

Trawick, George

Committee Member

Gudla, Charan

Date of Degree

5-15-2026

Original embargo terms

Immediate Worldwide Access

Document Type

Dissertation - Open Access

Major

Computer Science

Degree Name

Doctor of Philosophy (Ph.D.)

College

James Worth Bagley College of Engineering

Department

Department of Computer Science and Engineering

Abstract

Formal verification can prove the security properties of cryptographic protocols, but translating natural language specifications into formal models requires specialized expertise, limiting the broader adoption of formal verification methods. This dissertation investigates whether large language models (LLMs) can lower this barrier by automatically generating Cryptographic Protocol Shapes Analyzer (CPSA) models from natural language protocol specifications. We evaluate three complementary strategies for improving LLM-based CPSA code generation through systematic experimentation across 104 protocols and 15 language models. First, we analyze prompt engineering and find that moderate structured guidance yields the most accurate outputs, while excessive prompt complexity degrades performance. Second, we evaluate static context augmentation and demonstrate that curated reference examples improve outputs, with benefits concentrated among weaker models and diminishing returns for frontier models already at ceiling. Third, we investigate supervised fine-tuning and show that training a smaller model on domain-specific examples dramatically improves its base performance, achieving results equivalent to models 9× larger. Our results reveal that content type dominates content volume: reference examples improve generation while prescriptive instructions degrade it, despite similar token counts. We also demonstrate that domain-specific fine-tuning can substitute for substantial parameter scaling, enabling local deployment on modest hardware. Together, these findings establish empirical foundations for LLM-assisted formal specification synthesis and provide practical deployment pathways ranging from 71\% syntactically valid outputs with a locally fine-tuned model to 97\% with frontier models. The benchmark dataset, evaluation framework, and fine-tuned model are publicly available to support future research.

Download

Share

COinS