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

Hierarchy Requirements and Verification for Cryptographic Protocols

作　　者：刘怡文[1] 李伟琴[1] 

机构地区：[1]北京航空航天大学计算机科学与工程系

出　　处：《北京航空航天大学学报》2002年第5期589-592,共4页Journal of Beijing University of Aeronautics and Astronautics

摘　　要：将密码协议的安全需求分为浅层需求和深层需求 2个层面 ,阐述了密码协议的分层安全需求 .采用近世代数和时序逻辑的方法定义了形式化描述语言 ,并形式化地描述了密码协议的分层安全需求 .将类BAN逻辑与模型检查相结合 ,在Abadi Tuttle模型的基础上建立密码协议的计算模型 .以Otway Rees协议为例 。The security requirements for cryptographic protocols were divided into shallow requirements and deep requirements. The hierarchy security requirements were illustrated. Using temporal logic and algebra, a formal requirement language was presented and used to describe the formal hierarchy requirements for cryptographic protocols. A model of computation was developed by modifying and extending the Abadi and Tuttle model, combining BAN logic and the NRL Protocol Analyzer. Using this model and theorem proving techniques, the formal requirements of the Otway Rees protocol was verified.

关 键 词：密码协议 安全需求 逻辑代数 形式语言 模型检查 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]