Current formal verification of security protocols relies on specialized researchers and complex tools, inaccessible to protocol designers who informally evaluate their work with emulators. This paper addresses this gap by embedding symbolic analysis into the design process. Our approach implements the Dolev-Yao attack model using a variant of CSP based on Interaction Trees (ITrees) to compile protocols into animators -- executable programs that designers can use for debugging and inspection. To guarantee the soundness of our compilation, we mechanised our approach in the theorem prover Isabelle/HOL. As traditionally done with symbolic tools, we refer to the Diffie-Hellman key exchange and the Needham-Schroeder public-key protocol (and Lowe's patched variant). We demonstrate how our animator can easily reveal the mechanics of attacks and verify corrections. This work facilitates security integration at the design level and supports further security property analysis and software-engineered integrations.

翻译：当前安全协议的形式化验证依赖于专业研究人员和复杂工具，使得协议设计者难以访问，他们通常只能通过模拟器非正式地评估其工作。本文通过将符号分析嵌入设计过程来解决这一差距。我们的方法基于交互树（ITrees）的CSP变体实现Dolev-Yao攻击模型，将协议编译为动画器——设计者可用于调试和检查的可执行程序。为确保编译的可靠性，我们在定理证明器Isabelle/HOL中对方法进行了机械化验证。遵循符号工具的传统验证方式，我们以Diffie-Hellman密钥交换协议和Needham-Schroeder公钥协议（及Lowe修补变体）为案例。我们展示了动画器如何轻松揭示攻击机制并验证修正方案。这项工作促进了设计层面的安全集成，并支持进一步的安全属性分析与软件工程化集成。