抽象状态机下认证协议新的语义模型

为了简洁而正确的表达一个密码协议，选择一个具有比较自然语义的模型是十分必要的。不仅如此，一个恰当的模型须便于安全性质的分析，因此，具有一定的表达能力是十分必要的。为了探讨适合的方法和工具，人们使用各种各样的形式化工具来表达、分析密码协议的安全性。目前主要的方法包括逻辑的方法，如BAN逻辑，SVO等；基于模型检测的方法，如FDR工具，基于定理证明的和代数方法等等。各种方法都具有自己的优势和缺陷。探讨不同的方法和工具对于密码协议的描述和分析具有重要的意义。并可借此发现和发明好的模型和方法。