基于安全协议操作语义模型的组合协议分析及验证

摘要：

协议的可组合性问题是安全协议形式化分析及验证领域的一个公开问题,通过提出采用安全协议的操作语义模型对组合协议进行形式分析和验证,建立了Yahalom和Denning-Sacco组合协议的操作语义模型,并用基于操作语义模型的自动化验证工具Scyther验证了其安全性,发现了一个针对Yahalom协议机密性的组合攻击.结果表明,操作语义模型是分析与验证组合协议的一种可行方法.

关键词：组合协议、协议分析、操作语义模型、Scyther

所属期刊栏目：27

分类号：TP393.04(计算技术、计算机技术)

资助基金：广西自然科学基金054205;广西研究生教育创新计划2007105950812M17

在线出版日期：2007-12-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：378-382