论文部分内容阅读
在本论文中我们提出了一种通用的,可扩展的分析和检查加密协议的方法。我们的方法就是用CPAL(Cryptographic Protocol Analysis Language)语言来表示协议,将Hoare和Dijkstra在形式语义方面的理论应用到该语言,分析该语言的形式语义,定义每种语句的最弱前置条件。我们定义协议的失败条件作为后置条件,对加密系统的有关公理进行扩展,并用来对最弱前置条件进行推理证明,如果证明成功说明该协议会受到某个攻击。