该论文聚焦于安全协议执行中的细粒度可追踪性问题，提出了一种新的形式化框架，用于在协议执行中精确追踪参与方的身份、行为及其状态变化。研究背景是现有协议追踪技术通常粒度较粗，难以应对复杂攻击场景（如混淆代理、重放攻击）。核心方法包括定义一种扩展的迹语义（trace semantics），并引入可追踪性属性（trackability properties）的细粒度分类。通过案例研究（如Needham-Schroeder协议）验证了框架的有效性。实验表明，该方法能够揭示协议设计中隐藏的追踪漏洞，为改进协议安全性提供指导。主要贡献是建立了一个系统化的细粒度可追踪性分析理论，并提供了自动化工具原型。适合安全协议设计者、形式化验证研究人员以及关注隐私与问责制的安全分析师阅读。