密码协议的分层安全需求及验证

摘要：

将密码协议的安全需求分为浅层需求和深层需求2个层面,阐述了密码协议的分层安全需求.采用近世代数和时序逻辑的方法定义了形式化描述语言,并形式化地描述了密码协议的分层安全需求.将类BAN逻辑与模型检查相结合,在Abadi-Tuttle模型的基础上建立密码协议的计算模型.以Otway-Rees协议为例,利用该计算模型和定理证明技术对密码协议进行了多层需求验证.

关键词：逻辑代数、形式语言、定理证明、模型检查

所属期刊栏目：28

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

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

页数：共4页

页码：589-592