论文部分内容阅读
为了对自动信任协商（ATN）的安全性进行形式化分析与验证，文中借鉴安全协议的形式化分析方法，提出一种用进程代数Applied7c演算对ATN建模并验证其安全性的方法．该方法将ATN形式化为两个协商者进程的并发执行，其中一个协商者的进程就是对其拥有的证书及授权策略的静态建模；ATN的安全性被定义为Applied7c演算的观察等价性，从而使该方法不仅能检查授权策略执行的安全性，而且能对协商者的隐私安全进行验证．借助安全协议的自动分析工具ProVerif，文中实现了对ATN安全性的自动分析．实验结果表明，用Ap