安全协议验证的归纳方法与串空间形式化比较
Journal of Computer Research and Development（2008）
摘要
使用归纳方法和串空间分别将NSL(Needham-Schroeder-Lowe)协议及其正确性在辅助证明系统Agda中形式化,并比较了这两种安全协议验证法,证明两种方法形式化的正确性和攻击者能力是相同的.
更多查看译文
关键词
inductive method,type theory,strand space,cryptographic protocol
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要