天辅逻辑论坛：基于动态认知逻辑的非单调密码协议分析

密码协议本身的安全问题一直以来都倍受关注。逻辑分析能够有效地发现密码协议的潜在缺陷，避免使用不安全协议带来的损失。具有知识非单调性的密码协议的分析需要能够表示非单调性的逻辑。我们将首先用“forget”扩展动态认知逻辑语言并给出其精确的语法和语义描述具有知识非单调性的密码协议，其次用克里普克(Kripke)模型结合寄存器模型表示协议中各主体的知识以及协议运行过程中主体知识的变化，协议整个运行过程被完全地形式化。这个形式化过程就是对协议的分析过程，协议运行的最后一步形式化结果即为协议的分析结果，因此协议的安全性也在模型图中自然呈现，并进一步表明我们的分析是有效的。