基于CSP#和LTL逻辑的多方合同签署协议公平性验证方法

摘要

本发明公开了一种基于CSP#和LTL逻辑的多方合同签署协议公平性验证方法，该方法包括以下步骤：步骤一、用CSP#语言对多方合同签署协议进行建模；步骤二、用线性时序逻辑（LTL）对协议的公平性进行形式化描述，具体包括状态约减和协议公平性描述；步骤三、实现PAT平台上的模型检测，给出公平性验证和可视化攻击路径。本发明只需在协议规则的基础上，输入协议CSP#模型和LTL公平性描述，即可实现公平性自动验证，操作简单，能够切实验证协议性质；并针对状态空间爆炸问题给出了状态约减规则，较好的完成了状态分支约减，同时减小了时空复杂度。并给出自动跟踪攻击路径来方便协议的改进和完善。

主权项

一种基于CSP#和LTL逻辑的多方合同签署协议公平性验证方法，其特征在于，该方法包括以下步骤： 步骤(1)、用CSP#语言对多方合同签署协议进行建模，建立的协议结构模型为Kripke四元组M，令AP为原子命题集合M＝(S,S₀,R,L)，其中：S是协议状态的有限集合；是协议初始状态的集合；是状态转移函数；L：S→2^AP是标记函数，用于标记在某个状态下位真的原子命题的集合；并且，该模型满足以下假设，即：假设一：协议参与者之间的信道是不可靠的，即传输的消息可能会延迟或者丢失。但参与者与可信第三方之间的信道是可恢复信道；假设二：协议参与者可能是不诚实的，但多个参与者中至少有一个是诚实的，可信第三方是诚实的。诚实的参与者将严格按照协议规定执行操作，不诚实者也可以是合法用户，拥有自己的公钥和私钥，以及定义针对协议的不诚实参与者是安全的； 步骤(2)、对于协议系统S，用LTL线性时序逻辑可以将协议参与者P_i的公平性描述，模型表示如下： 强公平性模型： 弱公平性模型： 根据上述公式P_i的公平性描述为：在协议中止时，如果P₁，P₂，...，P_i‑1，P_i+1，...，P_n中的任意一位参与者获得了P_i的数字签名则一定存在一条路径使得P_i能够获得P₁，P₂，...，P_i‑1，P_i+1，...，P_n对合同m的签名；然后进行上述模型检测的状态约减，即采用Move‑One‑Step方法根据操作语义规则产生所有可以转换到目标状态的中间状态，并以Encode‑State方法为基础对目标状态进行布尔公式编码。