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

Formal Requirements and Verification for Security Protocols

该文采用近世代数和时序逻辑的方法提出并描述了密码协议的形式化安全需求,并在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.