基于一阶逻辑的非否认协议模型

？为了将密码协议的非否认性和公平性统一在一个框架之下更好地进行分析，提出了一套适用于分析非否认性和公平性的一阶逻辑语法和语义。在此基础上建立了一个用于分析非否认性和公平性的一阶逻辑模型，并以fairzg非否认协议为例进行了分析，发现了该协议的一个已知攻击，证明了模型的有效性和正确性。