论文部分内容阅读
安全协议的设计和分析是复杂而且容易出错的.使用形式化的语言有利于安全协议的正确性和完整性.现有的安全协议的描述方法大多很复杂而且容易导致二义,从而导致协议隐含着种种的安全隐患.引入了基于构造类别代数的形式化规范语言来规范安全协议,通过规则集合和公理集合对安全协议进行精确地描述,有利于协议设计地规范化和协议漏洞地发现,同时对Needham-Schroeder协议进行了形式化规范以进一步说明该形式化语言地使用.