非否认协议中认证保密性的设计与形式化分析

探讨了非否认协议的保密性认证目标,用攻击的方法验证了a（0）协议在认证保密性方面的不足;对其消息格式和会话密钥建立后确认方式做了修改,提出了na（0）协议;进一步运用svo逻辑对na（0）协议进行了形式化的分析,验证了na（0）协议满足主体身份的认证性和会话密钥的保密性。