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