安全协议的形式化需求及验证  

Formal Requirements and Verification for Security Protocols

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

机构地区：[1]北京航空航天大学,北京100083

出　　处：《计算机工程与应用》2002年第17期125-128,共4页Computer Engineering and Applications

摘　　要：该文采用近世代数和时序逻辑的方法提出并描述了密码协议的形式化安全需求,并在AT模型的基础上加入信任和知识的非单调逻辑,建立了安全协议的计算模型。利用该计算模型对Denning_Sacco公钥协议进行了验证,发现了对此协议的重放攻击,并对协议进行了修改。Using temporal logic and algebra,This paper illustrates the formal requirements for security protocols.By adding non-monotonic logic of belief and knowledge to the Abadi_Tuttle model of computation,the paper present s a model of computation for security protocols.Using this model,it verifies the well known Denning_Sacco Public-Key pro-tocol,discovers the replay attack upon the protocol,and adapt s it.

关 键 词：安全协议 形式化需求 验证 BAN逻辑 定理证明 密码协议 通信协议 

分 类 号：TN915.04[电子电信—通信与信息系统] TP393.08[电子电信—信息与通信工程]