论文部分内容阅读
根据可信第三方（Trusted third part，TTP）参与通信的方式，安全协议可以分为在线TTP型和离线TTP型两类。分析了两类协议的优缺点，提出了一种复合型安全协议，在同一协议中结合了两种方式，方式的选择由消息发送方和接收方共同决定。该协议由4条规则组成。为了描述协议的动态运行过程，对SVO逻辑系统进行了扩充，增加了3条公理，用于刻划消息接收者的不可否认性。基于扩充后的SVO逻辑系统对复合型安全协议进行了形式化描述，证明了该协议具有不可否认性。