电子合同的形式化安全验证方法

摘要

本发明公开一种电子合同的形式化安全验证方法，包括步骤1：找出合同中所有的承诺，按五元组写出承诺；步骤2：给每条承诺设定状态规则，以及状态间的逻辑关系；步骤3：将合同转化为承诺模型，并进一步采用CTL或LTL逻辑进行展开，设定好安全属性所期待的验证路径；步骤4：依据遍历算法，结合以概率为基础的权重进行判断；步骤5：得到各路径与其权重，以权重选取的标准得出承诺模型的利好或最优路径，并验证步骤3设定的验证路径为该最优路径，完成对承诺模型的验证。本发明根据智能合约的特点对承诺进行了重新定义，并在此基础上完成了智能合约的形式化定义，将以往繁杂的文本转变为计算机能理解的模型进行安全验证。

说明书

技术领域

本发明涉及智能合约技术领域，尤其涉及一种电子合同的形式化安全验证方法。

背景技术

“智能合约”的概念产生于1995年，由密码学家Szavo首次提出，他指出“智能合约通过使用协议和用户接口来促进合约的执行”。从本质上讲，智能合约是由事件驱动的、具备状态的、部署于可共享的分布式数据库上的计算机程序，现存智能合约的工作原理类似于其他计算机程序的IF-THen语句。智能合约只是以这种方式与真实世界的资产进行交互。当一个预先设定的条件被触发时，智能合约执行相应的合同条款。

传统的电子合同，其表述仍然以文字为载体，通过律师事务所的律师进行逐行逐句地分析，某些合同过于简单但数量巨大，某些合同又十分复杂，进而让律师的验证效率逐渐低下。

发明内容

针对上述现有技术的不足，本发明提供一种电子合同的形式化安全验证方法。

为解决上述技术问题，本发明所采取的技术方案是：电子合同的形式化安全验证方法，包括如下步骤：

步骤1：将合同电子化，找出合同中所有的承诺，按五元组写出承诺；

所述五元组为C(x,y,p,r,c(oc[]&tc))形式，其含义是承诺人x(promisor)向被承诺人y(promisee)做出承诺，如果前提p(premise)达成，就产生结果r(result)；

其中，前提p和结果r的值是布尔值，值为true表示前提已达成或结果已完成，值为false表示前提未达成或结果未完成；c(constraints)表示承诺的条例，值为true，承诺才会有效；其中oc和tc是与的关系表示：tc(time-constraints)表示该承诺的有效期，当tc为true时，承诺才会有效；oc(other-constraints[])表示该承诺的其他要求条例，当里面每一项均为true时，承诺才会有效；

承诺有效期tc是一个二元组tc:＝(pdact，pdbas)，其中，pdact表示承诺进入激活act状态之后，对前提p的完成时间限制；pdbas表示承诺进入就绪bas状态之后，对结果r的完成时间限制；若这两个限制均满足，tc为true；否则，tc为false。

例如，tc＝(24,24)表示前提p需要在承诺进入激活状态24h(默认单位为h)之内达成(即pdact＝24),否则承诺将进入过期状态；结果r需要在承诺进入到就绪状态之后24h之内完成(即pdbas＝24),否则承诺进入违约状态。在承诺中,前提或结果可能是预期的动作。例如,商家a向客户b做出一个承诺，如果b在系统上预存100元货物钱，a就给b寄出相应货物。这里，前提是预存钱的动作(b在系统上预存100元钱)，而结果是寄货物的动作(a给b寄出购买的货物)。

步骤2：给每条承诺设定状态规则，以及状态间的逻辑关系；

所述状态规则包含有5种不同的状态，分别如下：

1)激活act状态：前提p和结果r都为false，未出现违约；表示承诺有效，在等待前提p的达成和结果r的完成；

2)就绪bas状态：前提p为true，结果r为false未出现违约；表示承诺已生效且前提p已经达成,在等待结果r的完成；

3)满足sat状态：前提p和结果r都为true，表示前提p已达成，结果r也已完成，承诺已被履行；

4)过期exp状态：前提p和结果r都为false，出现违约；表示在承诺失效时，前提p未能达成而结果r也未能完成；

5)违约vio状态：前提p为true，但结果r为false，出现违约；表示当承诺失效时，尽管b已达成了前提p，但a仍然未履行其承诺完成结果r，已经违约。

所述5种不同状态之间的逻辑关系如下：

如果在创建承诺时，前提p和结果r都为false，承诺进入激活act状态，将这样的承诺称为有条件承诺，也就是承诺人履行该承诺存在前提条件；如果前提p为true，结果r为false，承诺进入就绪bas状态，将这样的承诺称为无条件承诺，也就是承诺人将无条件履行该承诺；

在激活act状态下，如果出现违约，前提p和结果r都未能达成即为false，承诺进入了过期exp状态，此时承诺已经失效；在激活act状态下，如果前提p达成即p＝true，该承诺变成无条件承诺，进入就绪bas状态；

在就绪bas状态下，如果出现违约，结果r依然未能完成即r＝false，承诺进入违约vio状态，表示承诺人已违约；在就绪bas状态下，未出现违约，承诺人完成了结果r即r＝true，进入满足sat状态，表示承诺人履行了其承诺。

步骤3：将合同转化为承诺模型，即一个有限状态自动机；并进一步采用CTL逻辑或LTL逻辑进行展开，设定好安全属性所期待的验证路径，过程如下：

步骤3.1：根据设定好的五元组结合其中的逻辑关系，以其中的动作为方向，以五元组集合C(x,y,p,r,c(oc[]&tc)为状态节点，构建承诺模型的有限状态自动机形式；

所述步骤3.1中动作表示为：

action:＝actname(executor,object,input,output)

其中，actname是动作的名称，executor是动作的执行者，object是动作的作用对象，input是输入参数，output是输出参数；其中actname和exectuor是必需的，而object、input和output都是可选的；

所述动作的值是一个布尔值，action＝fasle表示没有完成该动作，action＝true表示该动作已完成；动作的默认值为false。

例如,transfer(a,b,10,receipt)表示a向b转账10元的动作,其中,transfer是动作名,a是动作的执行者,b是动作的作用对象,10是输入参数,receipt(收据)是输出参数。transfer(a,b,10,receipt)的默认值是false,表示b还没有收到a转过来的10元钱,也就是动作还未完成。如果transfer(a,b,10,receipt)＝true,则表示该动作已经完成(a收到b转账过来的10元钱)。

步骤3.2：将该有限状态自动机形式当作图论中的树的节点进行展开，并将动作当作该树的有向邻边进行向下延伸，根节点为所有状态的开始，因此是状态的全集；子节点为合约会经历的中间过程，叶子节点为合约的结束情形；

步骤3.3：使用CTL逻辑或LTL逻辑，根据逻辑假定路径最优条件，该条件是指定的某一路径节点的限制；将需要验证的性质当作原子命题，结合CTL或LTL的逻辑连接符与模态算子描述产生所期待的路径，该安全性质即为该路径根据CTL逻辑或LTL逻辑所满足的逻辑表达式为真。

所述CTL的逻辑连接符包括：not(非)、or(或)、and(与)，CTL的模态算子包括：E(Exists a path)、A(All paths)、X(Next-time)、U(Until)、F(Future)、G(Global)；

所述LTL的逻辑连接符包括：not(非)、or(或)、and(与)，LTL的模态算子包括：G(Always)、F(eventually)、X(Next-time)、U(Until)。

所述需要验证的性质包括：合同的逻辑陷阱、合同中涉及利益的安全性质，例如商品合同中涉及交易的利润公式是否合理、贷款合同中的日利率是否过高等，将这些性质通过命题形式化体现。

步骤4：依据遍历算法，将有限的所有路径进行筛选，结合以概率为基础的权重进行判断，过程如下：

步骤4.1：设置一个参数函数(f(S

步骤4.2：所有的路径用路径总集合表示：Path＝{P

步骤4.3：通过深度遍历算法或层次遍历算法，得到每一条路径的权重求和，每一个状态节点本身根据其动作的影响设置一个合理的值，该值为布尔变量，即0或1；于是第k条路径的权重和为：

步骤5：根据步骤4得到的各路径与其权重，以权重选取的标准得出承诺模型的利好或最优路径，并验证步骤3设定的验证路径为该最优路径，完成对承诺模型的验证，过程如下：

步骤5.1：所有路径与其权重和构成二元组集合：{

步骤5.2：设定标准函数f(Z)，以权重选取的标准得出承诺模型的利好或最优路径，最简单的标准函数为：Max(Z)；

步骤5.3：根据权重标准函数得到的路径与步骤3中设定的路径进行比较，并根据得到的路径判断与设定路径逻辑表达式是否符合，符合则验证通过；

步骤5.4：如果不符合，则进行人工进一步审核；或调整参数函数与标准函数，进行再一次验证。

采用上述技术方案所产生的有益效果在于：

1、本发明提供的方法以承诺(commitment)作为基本元素来构建智能合约。承诺是商务合同的基本单位，表示一方对另一方的义务。一份合同通常由一组相互关联的承诺组成。在人工智能领域，有不少关于形式化描述商业承诺的工作。将承诺用于描述智能合约，根据智能合约的特点对承诺进行了重新定义，并在此基础上完成了智能合约的形式化定义。

2、本发明提供的方法将传统合同转化为承诺模型，而承诺模型又能看成是一个有限状态自动机。根据这个有限状态自动机，能将以往繁杂的文本转变为计算机能理解的模型进行安全验证，将之进行验证便简便许多。

附图说明

图1为本发明实施例中电子合同的形式化安全验证方法的流程图；

图2为本发明实施例中5种不同状态之间的逻辑关系图；

图3为本发明实施例中乘机人与保险公司之间合同的承诺模型；

图4为本发明实施例中通过遍历算法得到承诺模型中所有的路径图；

图5为本发明实施例中对每一条路径进行权重求和示意图。

具体实施方式

下面结合附图和实施例，对本发明的具体实施方式作进一步详细描述。以下实施例用于说明本发明，但不用来限制本发明的范围。

如图1所示，本实施例的方法如下所述。

步骤1：将合同电子化，找出合同中所有的承诺，按五元组写出承诺；

所述五元组为C(x,y,p,r,c(oc[]&tc))形式，其含义是承诺人x向被承诺人y做出承诺,如果前提p达成,就产生结果r；

其中，前提p和结果r的值是布尔值，值为true表示前提已达成或结果已完成，值为false表示前提未达成或结果未完成；c表示承诺的条例，值为true，承诺才会有效；其中oc和tc是与的关系表示：tc表示该承诺的有效期，当tc为true时，承诺才会有效；oc表示该承诺的其他要求条例，当里面每一项均为true时，承诺才会有效；

承诺有效期tc是一个二元组tc:＝(pdact，pdbas)，其中，pdact表示承诺进入激活act状态之后，对前提p的完成时间限制；pdbas表示承诺进入就绪bas状态之后，对结果r的完成时间限制；若这两个限制均满足，tc为true；否则，tc为false。

本实施例中，以乘机人与保险公司之间的合同为例，找出合同中的所有承诺，如下所示：

C3:乘机人向系统s承诺：购买的航班在24h内计划起飞；

C4:乘机人b向系统s承诺：如果C3进入满足状态(即买了机票，需24h内)则乘机人b将在购票后0.5h内向系统s存5元；

C5:保险公司a向系统s承诺：如果24h内C3，C4进入满足状态，则保险公司a在1h内向系统s存20元；

C6:系统s向乘机人b承诺：如果C5违约，则系统s将在2h内将5元返回乘机人b；

C7:系统s向乘机人b承诺：如果C5处于满足状态且满足赔偿条件且未过1d则给乘机人b20元，给保险公司5元；

C8:系统s向乘机人b承诺：如果C5处于满足状态且满足不赔偿条件或过1d则给保险公司a25元。

步骤2：给每条承诺设定状态规则，以及状态间的逻辑关系；

所述状态规则包含有5种不同的状态，分别如下：

1)激活act状态：前提p和结果r都为false，未出现违约；表示承诺有效，在等待前提p的达成和结果r的完成；

2)就绪bas状态：前提p为true，结果r为false未出现违约；表示承诺已生效且前提p已经达成,在等待结果r的完成；

3)满足sat状态：前提p和结果r都为true，表示前提p已达成，结果r也已完成，承诺已被履行；

4)过期exp状态：前提p和结果r都为false，出现违约；表示在承诺失效时，前提p未能达成而结果r也未能完成；

5)违约vio状态：前提p为true，但结果r为false，出现违约；表示当承诺失效时，尽管b已达成了前提p，但a仍然未履行其承诺完成结果r，已经违约。

所述5种不同状态之间的逻辑关系如图2所示，关系如下：

如果在创建承诺时，前提p和结果r都为false，承诺进入激活act状态，将这样的承诺称为有条件承诺，也就是承诺人履行该承诺存在前提条件；如果前提p为true，结果r为false，承诺进入就绪bas状态，将这样的承诺称为无条件承诺，也就是承诺人将无条件履行该承诺；

在激活act状态下，如果出现违约，前提p和结果r都未能达成即为false，承诺进入了过期exp状态，此时承诺已经失效；在激活act状态下，如果前提p达成即p＝true，该承诺变成无条件承诺，进入就绪bas状态；

在就绪bas状态下，如果出现违约，结果r依然未能完成即r＝false，承诺进入违约vio状态，表示承诺人已违约；在就绪bas状态下，未出现违约，承诺人完成了结果r即r＝true，进入满足sat状态，表示承诺人履行了其承诺。

步骤3：将合同转化为承诺模型，即一个有限状态自动机；并进一步采用CTL逻辑进行展开，设定好安全属性所期待的验证路径，过程如下：

步骤3.1：根据设定好的五元组结合其中的逻辑关系，以其中的动作为方向，以五元组集合C(x,y,p,r,c(oc[]&tc)为状态节点，构建承诺模型的有限状态自动机形式；

所述步骤3.1中动作表示为：

action:＝actname(executor,object,input,output)

其中，actname是动作的名称，executor是动作的执行者，object是动作的作用对象，input是输入参数，output是输出参数；其中actname和exectuor是必需的，而object、input和output都是可选的；

所述动作的值是一个布尔值，action＝fasle表示没有完成该动作，action＝true表示该动作已完成；动作的默认值为false。

步骤3.2：将该有限状态自动机形式当作图论中的树的节点进行展开，并将动作当作该树的有向邻边进行向下延伸，根节点为所有状态的开始，因此是状态的全集；子节点为合约会经历的中间过程，叶子节点为合约的结束情形；

步骤3.3：使用CTL逻辑或LTL逻辑，根据逻辑假定路径最优条件，该条件是指定的某一路径节点的限制；将需要验证的性质当作原子命题，结合CTL或LTL的逻辑连接符与模态算子描述产生所期待的路径，该安全性质即为该路径根据CTL逻辑或LTL逻辑所满足的逻辑表达式为真。

所述CTL的逻辑连接符包括：not(非)、or(或)、and(与)，CTL的模态算子包括：E(Exists a path)、A(All paths)、X(Next-time)、U(Until)、F(Future)、G(Global)；

所述LTL的逻辑连接符包括：not(非)、or(或)、and(与)，LTL的模态算子包括：G(Always)、F(eventually)、X(Next-time)、U(Until)。

本实施例中，得到乘机人与保险公司合同的承诺模型如图3所示，其中：

买保险进入S0；

S0：如果乘客b没买票就进入S1；如果乘客b买了票就进入S2；

S2：如果乘客b没在规定时间交定金进入S3；如果乘客b交了定金进入S4；

S4：如果保险公司没在规定时间交定金进入S5；如果保险公司交了定金进入S6；

S5：如果系统返回给用户钱进入S7；

S6：如果满足赔偿条件且未过1d进入S8；如果飞机没延误进入满足不赔偿条件或过1d进入S9；

S8：如果系统给钱进入S10；

S9：如果系统给钱进入S11。

按合同写出状态转换的动作，例如：

S0—>S1action:＝breakcontract(b,s,break)，乘客b告知系统s没买票(break)。

步骤4：依据遍历算法，将有限的所有路径进行筛选，结合以概率为基础的权重进行判断，过程如下：

步骤4.1：设置一个参数函数(f(S

步骤4.2：所有的路径用路径总集合表示：Path＝{P

步骤4.3：通过深度遍历算法或层次遍历算法，得到每一条路径的权重求和，每一个状态节点本身根据其动作的影响设置一个合理的值，该值为布尔变量，即0或1；于是第k条路径的权重和为：

本实施例中，根据形式化验证过程，这棵树是有限的路径的，路径数量级很小，因此使用深度搜索优先算法即可，将所有路径遍历如图4所示。根据实际情况的航班信息如误点率、旅客准时程度等影响因素，我们根据合同条例，设置好参数函数f(S

步骤5：根据步骤4得到的各路径与其权重，以权重选取的标准得出承诺模型的利好或最优路径，并验证步骤3设定的验证路径为该最优路径，完成对承诺模型的验证，过程如下：

步骤5.1：所有路径与其权重和构成二元组集合：{

步骤5.2：设定标准函数f(Z)，以权重选取的标准得出承诺模型的利好或最优路径，最简单的标准函数为：Max(Z)；

步骤5.3：根据权重标准函数得到的路径与步骤3中设定的路径进行比较，并根据得到的路径判断与设定路径逻辑表达式是否符合，符合则验证通过；

步骤5.4：如果不符合，则进行人工进一步审核；或调整参数函数与标准函数，进行再一次验证。

本实施例中，例如起始状态节点不涉及金钱仅表示承诺的开始，则令S0＝0。

因此，我们对于其中每一条路径进行权重求和如图5所示，如果最后我们的目标是使得购险者不会受损，则：Target＝max{Z