CN109347651A

CN109347651A - 基于msvl的区块链系统建模和安全性验证的方法及系统

Info

Publication number: CN109347651A
Application number: CN201810981891.1A
Authority: CN
Inventors: 王小兵; 朱云凯; 段振华; 赵亮; 田聪; 张南
Original assignee: Xidian University
Current assignee: Xidian University
Priority date: 2018-08-27
Filing date: 2018-08-27
Publication date: 2019-02-15
Anticipated expiration: 2038-08-27
Also published as: CN109347651B

Abstract

本发明属于形式化方法领域，公开了一种基于MSVL的区块链系统建模和安全性验证的方法及系统，在MC中用MSVL对区块链系统建模，用程序p表示；用PPTL描述区块链系统的性质，用公式φ表示；在MC中，加入MSVL的建模程序p和用PPTL描述的性质φ，验证区块链系统的安全性。本发明的区块链用MSVL程序进行建模，区块链的安全性性质用PPTL描述，而PPTL为PTL的命题子集，MSVL为PTL的可执行子集，因而MSVL和PPTL可以统一在MC中执行，相比于其他方法，本发明不需要使用另外的形式语言，也不需要调用另外的工具及大量的手工证明，只需要提供待验证性质的PPTL公式，证明过程由MC自动完成。

Description

基于MSVL的区块链系统建模和安全性验证的方法及系统

技术领域

本发明属于计算机辅助设计技术领域，尤其涉及一种基于MSVL的区块链系统建模和安全性验证的方法及系统。

背景技术

目前，业内常用的现有技术是这样的：目前，用到区块链技术的系统应用的技术发展可以大致分为三个阶段。第一个阶段主要发展为数字加密货币系统；第二个阶段主要发展为金融系统；第三个阶段主要发展为区块链社会。目前正处于二阶段的初期，并且一定不会长期处于该时期。区块链是以时间线索来组织数据，并且每隔一段时间将数据进行打包成区块，再以链条和时间顺序链接这些区块而成的特定数据结构，保证了其可追溯性，并且以密码学的方式保证其不可篡改和不可伪造，是一个分布式、去中心化、公开共享的总账本。区块链的数据结构可简单的描述如下：一种基于时间戳的链式结构，区块链的基本组成单位是区块，区块有包含了区块头和区块体，区块头包含六个基本要素：前一区块的摘要值，是经过hash加密后的固定长度的字符串；时间戳；挖矿难度；该区块中交易打包的摘要值；经过挖矿大量的计算后得到的随机数；本区块链的摘要值。区块体只要包含了该时间段的所有交易，使用Merkle树的数据结构，所有交易是Merkle树的叶子结点，然后每两个结点生成一个父亲结点，依次类推直到生成根结点。

区块链具有五大特性：去中心化、时序数据、集体维护、可编程、安全可信。即便是区块链具有以上五大特性并且区块链技术被广泛的应用，但是区块链技术仍然存在着安全方面的问题，不同技术层面都可能存在安全问题。在节点层，与传统服务器的安全防范措施相比，区块链系统中的每一个计算节点可以说都是“裸奔”的，每一个计算节点很容易受到各种非法攻击。在合约层，以太坊上的智能合约，可能只是一段js代码，存在很多潜在的漏洞，这些漏洞很容易被人利用。在数据层，用户在区块链上的账户名需要公布出来，通过用户的账户名，很容易获得用户的账户的交易信息和账户余额，隐私问题也是个大问题。因此，区块链系统是一个分布式系统，它增加了威胁和风险的可能，就系统本身而言，是降低了安全性而不是增加了安全性。所以对区块链进行安全验证是非常有必要的。

2016年黑客通过The Dao，利用智能合约中的漏洞，成功盗取360万以太币。TheDAO事件发生后，以太坊创始人VitalikButerin提议修改以太坊代码，对以太坊区块链实施硬分叉，将黑客盗取资金的交易记录回滚，在得到社区大部分矿工支持的同时也遭到了少数人的强烈反对，最终导致了以太坊社区的分裂。2017年7月19日，多重签名钱包Parity1.5及以上版本出现安全漏洞，15万个ETH被盗，共价值3000万美元。两次被盗事件都是因为区块链系统中的漏洞，由此可见，加强各技术层的安全性能是提高区块链安全的重要保证，其中形式化验证是解决区块链系统安全性审核的一个有效方法。形式化验证就是基于已建立的形式化规格，对所规格系统的相关特性进行分析和验证，以评判系统是否满足期望的特性。形式化验证并不能完全确保系统的性能正确无误，但是可以最大限度地理解和分析系统，并尽可能地发现其中的不一致性、模糊性、不完备性等错误。形式化验证的主要技术包括模型验证和定理证明。本发明正是从这个方面入手，打造一个形式化验证的模型框架，用形式化验证的方式去验证系统可能存在的漏洞。

综上所述，现有技术存在的问题是：现有的区块链技术存在很容易获得用户的账户的交易信息和账户余额，安全性较低。

发明内容

针对现有技术存在的问题，本发明提供了一种基于MSVL的区块链系统建模和安全性验证的方法及系统。

本发明是这样实现的，一种基于MSVL的区块链系统建模和安全性验证的方法，所述基于MSVL的区块链系统建模和安全性验证的方法在MC中用MSVL对区块链系统建模，用程序p表示；用PPTL描述区块链系统的性质，用公式φ表示；在MC中，加入MSVL的建模程序p和用PPTL描述的性质φ，验证区块链系统的安全性。

进一步，所述基于MSVL的区块链系统建模和安全性验证的方法利用MSVL程序p对区块链系统进行建模；利用PPTL公式φ描述区块链系统的性质。

进一步，所述基于MSVL的区块链系统建模和安全性验证的方法包括以下步骤：

步骤一，使用MSVL语言对区块链系统建模，数据结构中的结构体表示区块链系统中的区块、交易、用户以及用户间的通信；在建模中，用函数表示区块链系统中的基本操作；使用数据结构中的图结构建模p2p网络，顶点的集合即用户集；

步骤二，分别从数据层，网络层，共识层，激励层，合约层找用户关心的性质，采用PPTL公式描述，对区块链建模系统的安全性进行验证；

步骤三，将建模的MSVL程序和描述性质的PPTL公式在MC验证，检查区块链系统的安全性性质是否满足。

进一步，使用MSVL语言对区块链系统建模的区块链系统中的用户类型分为四种，分别用四个参数表示具体为：

k1：表示用户有无路由功能，决定了该用户能否与其他用户通信；

k2：表示用户有无钱包功能，决定了该用户能否与其他用户交易；

k3：表示用户有无挖矿功能，决定了该用户是否具有获取奖励的资格及共识机制是否有效；

k4：表示用户有无管理功能，决定了该用户是否具有发行货币的权利；

使用数据结构中的结构体表示区块链系统中的区块、交易、用户以及用户间的通信，具体为：

区块链中的区块信息用结构体structBlock表示；

区块链中的交易信息用结构体structTrade表示；

区块链中的用户信息用结构体structNodes表示；

区块链中的用户间通信用结构体struct Edges表示；

区块链系统中的功能用函数表示，具体为：

functionpass表示进入区块链系统的一个简单的身份认证函数；

function BAAC_max表示区块链系统的共识机制-活跃度与信用度的权衡比较算法，用来计算出获得奖励的矿工；

functionpay表示一条交易中的转账支付的函数；

functionrecord表示生成新区块前的所有交易记录的函数；

functionp2p表示p2p网络用户结点及其相互通信的遍历检测函数。

进一步，PPTL公式根据具体要验证的安全性性质确定，首先根据需要验证的性质，定义命题；然后根据命题的逻辑关系，得出相应合理的PPTL公式。

进一步，用MSVL对需要进行验证的区块链系统进行建模的方法具体包括：

(1)建模程序中的用户类型用四个参数表示：

k1：用户有无路由功能，；k2：用户有无钱包功能；k3：用户有无挖矿功能；k4：用户有无管理功能；

(2)定义四个结构体来表示区块链系统中的用户、交易、区块；结构体structBlock：区块链中的区块信息用结构体struct Block表示，结构体包括五个成员：ID用来表示当前区块的摘要值；preID用来表示前一区块的摘要值；Ntrade用来表示所有交易的交易打包摘要值，即Merkle树根结点的hash值；x用来表示挖矿过程生成的随机数；t用来表示时间戳；

(3)区块链系统中的功能用函数表示，具体为：

functionpass表示进入区块链系统的一个简单的身份认证函数；

functionpay表示一条交易中的转账支付的函数；

functionrecord表示生成新区块前的所有交易记录的函数；

进一步，结构体struct Trade：区块链中的交易信息用结构体struct Trade表示，结构体包括四个成员：num用来表示交易编号；fromNode用来表示交易的发送者；toNode用来表示交易的接受者；payBalancekey用来表示交易金额；

结构体structNodes：区块链中的用户信息用结构体structNodes表示，结构体包括八个成员：address用来表示用户的地址，用于存储账户余额的地址；k1表示的是用户有无路由功能；k2表示的是用户有无钱包功能；k3表示的是用户有无挖矿功能；k4表示的是用户有无管理功能；sendBalance用来表示发行奖励的货币额度；Balance用来表示账户余额；baac表示共识机制中每个用户的活跃度与信用度所占比重，权重比例决定奖励；

结构体struct Edges：区块链中的用户间通信用结构体struct Edges表示结构体包括四个成员：fromAddress表示通信链路的消息发送者；toAddress表示通信链路的消息接受者；weight表示数据结构图结构的边上权值；State表示任意两个用户结点之间有无边存在，有为1，没有为0。

进一步，数据层需要的性质用PPTL公式描述并验证为：

数据层的安全性性质：如果没有路由或没有钱包或发送方余额不足，那么将不能交易；

发生了交易，且有钱包，且发送方余额够支付，具体描述：

define p：交易双方有路由；

define q：交易双方有钱包；

define r：交易发送方钱够；

define c：交易成功；

性质描述为PPTL公式为：[](<>c—>p∧q∧r)。

本发明的另一目的在于提供一种实施所述基于MSVL的区块链系统建模和安全性验证的方法的基于MSVL的区块链系统建模和安全性验证的系统，所述基于MSVL的区块链系统建模和安全性验证的系统包括：

模型建立模块，用于建立结构体数据类型描述区块链系统中区块的模型；

安全性质定义模块，用于确定所需要验证的安全性性质，并采用PPTL公式描述；

验证模块，用于检查区块链系统的安全性性质是否满足。

本发明的另一目的在于提供一种实现所述基于MSVL的区块链系统建模和安全性验证的方法的信息数据处理终端。

X可能是个软件，可能是个硬件，也可能是某个协议的系统，我们证明它是否达到我所期待的需求。X达到我需求的目标用测试就可以了，但现有的测试技术只能用于查找已有的bug，看我们的功能是否满足需求，同时输入很多测试案例，看这个结果是否满足我们的要求，比如现在我查出了常见漏洞，但不能证明你没有其他的漏洞。因此，我们用数学手段去推理证明它，把代码变成公式，去证明它有没有其他问题出现。综上所述，形式化验证方法是目前更完备的解决安全问题的方法，它的目标是为了提高代码的正确性和可靠性

综上所述，本发明的优点及积极效果为：将形式化方法应用于区块链系统安全性验证；形式化方法是基于数学逻辑推理的，用于计算机软件与硬件的安全性验证，具备精确无误的特征，常见的有模型检测、定理证明；模型检测方法的基本思想为：通过状态空间搜索确认区块链系统是否具有某些性质。即给定一个区块链建模程序M和规约q，生成对应的合约模型M，然后证明M＝>q，即规约公式q在合约模型M中成立，这样就证明了合约程序M满足规约q。MSVL语言是一种形式化系统建模语言，使用MSVL对系统的性质进行验证一般包括以下三个基本模块：1)系统建模语言MSVL，用于直观、明确地描述区块链系统的模型，而不考虑具体实现细节；2)功能强大而简明的描述系统应满足性质(属性要求)的逻辑表示法PPTL；3)提供一套验证系统建模逻辑一致性及系统是否满足所要验证性质的方法。

本发明的区块链用MSVL程序进行建模，区块链的安全性性质用PPTL描述，而PPTL为PTL的命题子集，MSVL为PTL的可执行子集，因而MSVL和PPTL可以统一在MC中执行，相比于其他方法，本发明不需要使用另外的形式语言，也不需要调用另外的工具及大量的手工证明，只需要提供待验证性质的PPTL公式，证明过程由MC自动完成。

附图说明

图1是本发明实施例提供的基于MSVL的区块链系统建模和安全性验证的方法流程图。

图2是本发明实施例提供的基于MSVL的区块链系统建模和安全性验证的系统结构示意图；

图中：1、模型建立模块；2、安全性质定义模块；3、验证模块。

图3是本发明实施例提供的区块链建模的用户类型及其功能的示意图。

图4是本发明实施例提供的区块链建模的每一笔具体交易的程序执行的流程示意图。

图5是本发明实施例提供的区块链建模的六个结点的p2p网络通信的示意图。

图6是本发明实施例提供的区块链建模的具体区块的数据结构的示意图。

图7是本发明实施例提供的区块链的结构分层的示意图。

图8是本发明实施例提供的验证性质满足时返回模型示意图。

具体实施方式

为了使本发明的目的、技术方案及优点更加清楚明白，以下结合实施例，对本发明进行进一步详细说明。应当理解，此处所描述的具体实施例仅仅用以解释本发明，并不用于限定本发明。

针对基于目前区块链系统中用户关心的安全问题；本发明将形式化方法应用于区块链系统安全性验证，用于计算机软件与硬件的安全性验证。本发明利用MSVL对区块链建模、用PPTL描述区块链的性质，最终在MC中进行验证，确定区块链的性质是否正确。

下面结合附图对本发明的应用原理作详细的描述。

如图1所示，本发明实施例提供的基于MSVL的区块链系统建模和安全性验证的方法包括以下步骤：

S101：用MSVL对需要验证的区块链系统进行建模，用结构体数据类型来描述区块链系统中的区块，用户，交易等；另外，在建模中，用函数表示区块链系统中的基本操作；

S102：分别从区块链系统的数据层、网络层、共识层、合约层着手来确定所需要验证的安全性性质，并采用PPTL公式描述这些性质；

S103：将建模的MSVL程序和描述区块链性质的PPTL公式统一在MC中，检查区块链系统的安全性性质是否满足。

如图2所示，本发明实施例提供的基于MSVL的区块链系统建模和安全性验证的系统包括：

模型建立模块1，用于建立结构体数据类型描述区块链系统中区块的模型；

安全性质定义模块2，用于确定所需要验证的安全性性质，并采用PPTL公式描述；

验证模块3，用于检查区块链系统的安全性性质是否满足。

下面结合附图对本发明的应用原理作进一步的描述。

本发明的实施例将建模的MSVL程序和描述性质的PPTL公式，在同一个MC中验证，如果验证成功，则该需要验证的区块链系统满足该性质，否则就违背性质。本发明用MSVL程序p来为待验证的区块链系统建模，并使用PPTL公式φ来描述所需要的性质，为了判断区块链系统是否满足这一性质，需要证明公式p→φ的有效性，如果p→φ有效，则区块链系统满足性质，否则区块链系统就违背该性质。

MSVL的基本数据结构有：

(1)整形：int

(2)浮点型：float

(3)字符型：char

(4)字符串型：string

(5)基本数据类型指针：int*/char*/float*/string*

(6)结构体：struct

(7)结构体指针:struct*。

MSVL程序涉及的主要语句：

(1)空语句：empty；

(2)基本赋值语句：

(3)next语句：Ox；

(4)always语句：□x；

(5)投影语句：(s₁,...,s_m)prj s；

(6)顺序语句：

(7)并行语句：

(8)条件语句：

(9)while语句：

(10)状态框架语句：

(11)区间框架语句：

(12)Await语句：其中，x₁,...,x_h是出现在b中的变量；

如图3所示，本发明实施例提供的基于MSVL的区块链系统建模和安全性验证的方法包括如下步骤：

第一步，用MSVL对需要进行验证的区块链系统进行建模，其中用结构体数据类型来描述区块链系统中的用户，交易，区块等；具体为：

区块链中的区块信息用结构体structBlock表示。

区块链中的交易信息用结构体structTrade表示。

区块链中的用户信息用结构体structNodes表示。

区块链中的用户间通信用结构体struct Edges表示。

而区块链中的一些功能，则用函数表示，具体为：

functionpass表示进入区块链系统的一个简单的身份认证函数，类似于登录操作；

function BAAC_max表示区块链系统的共识机制——活跃度与信用度的权衡比较算法(BAAC)，用来计算出获得奖励的矿工；

functionpay表示一条交易转账支付的函数；

functionrecord表示生成新区块前的所有交易记录的函数；

第二步，确定所述需要验证的区块链系统中的安全性性质，并采用PPTL公式描述这些性质。PPTL公式是根据具体要验证的性质来确定的，首先根据需要验证的性质，定义命题，然后根据命题的逻辑关系，得出相应合理的PPTL公式。

第三步，将建模的MSVL程序和描述性质的PPTL公式统一在MC中，检查区块链系统的性质是否满足。

用来描述区块链模型的MSVL程序和用来描述模型性质的PPTL公式都可以转换成PTL公式，所以可以在同一个MC中执行，并得出结果。MC是用来执行MSVL语言，其验证模块可以完成基于PPTL公式的性质验证。

建模的主要思想如下：

P2P网络的详细说明：

全分布式非结构化P2P网络，采用基于完全随机图的组织方式，各结点随机接入网络。如图6所示，采用洪泛的方式来广播消息，缺点是浪费资源。优点是容错率高，安全性高，隐私性强。

交易流程的详细说明：

主要分为三个阶段，申请交易，验证交易，记录交易，如图3所示。分别对三个阶段加以具体的说明：

第一阶段：申请交易，需要满足k1功能，也就是路由功能，然后等待对方的响应，对方同意交易的一个衡量的标准就是交易发起者的信用积分，只有满足交易接受者的理想信用积分，才会得到对方的响应。如果得到对方同意，进入下一阶段，否则交易结束。

第二阶段：响应过后，由交易发起者输入交易的金额，同时验证该用户是否具有钱包功能，也就是满足k2，之后验证钱包余额是否够用，如果验证通过进入下一阶段，不通过信用积分减少一分，并且交易结束。

第三阶段：交易记账，将交易打包到区块中，并在该用户的权值上加上交易额，作为区块生成后奖励额发行参考数据。

共识算法的详细说明：

奖励机制及其共识算法——活跃度与信用度的权衡比较算法(balancealgorithm ofactivity and credit，BAAC)。

下面结合具体实施例对本发明的应用原理作进一步的描述。

有六个用户结点A、B、C、D、E、F。在图的结构中对应的是结点，用户之间的通信交易对应图中的边，边上面的权值即是两个用户所有的交易额之和。

区块链建模系统的共识算法，主要可以分为五步：

第一步，将每一用户发送的交易额进行汇总，记为SA、SB、SC、SD、SE、SF。将每一个用户接受的交易额汇总，记为RA、RB、RC、RD、RE、RF。

第二步，将每一个结点与其相关联的边上的权值加和，这就是与该结点作为发送者和接受者的总交易额，以此代表用户在区块链系统中的活跃值(Activity)，记为A1、A2、A3、A4、A5、A6，A为A1、A2、A3、A4、A5、A6的加和，即A＝sum(A1，A2，A3，A4，A5，A6)。如下表所示:

A1＝RA+SA

A2＝RB+SB

A3＝RC+SC

A4＝RD+SD

A5＝RE+SE

A6＝RF+SF

第三步，查看用户的信用值，每个用户的信用比是当前信用值与总信用值得比例，记为C1、C2、C3、C4、C5、C6，这里设置总的信用值为100，用户信用最高为1。

第四步，BAAC共识算法即是用该用户的总的余额变动A所占百分比，乘以该用户的用户信用的信用比C/100，乘积记为M1、M2、M3、M4、M5、M6。如下表所示：

M1	(A1/A)*(C1/C)
		M2	(A2/A)*(C2/C)
M2	(A3/A)*(C3/C)
		M4	(A4/A)*(C4/C)
M5	(A5/A)*(C5/C)
		M6	(A6/A)*(C6/C)

第五步，在区块生成中，M最大的用户，便是获得奖励的矿工用户，可以得到奖励。求解max(M1，M2，M3，M4，M5，M6)。

代码实现：

用结构体数据类型来描述区块链系统中的用户，交易，区块等，具体为：

区块链中的区块信息用结构体structBlock表示。

区块链中的交易信息用结构体structTrade表示。

区块链中的用户信息用结构体structNodes表示。

区块链中的用户间通信用结构体struct Edges表示。

而区块链中的一些功能，则用函数表示，具体为：

functionpay表示一条交易转账支付的函数；

functionrecord表示生成新区块前的所有交易记录的函数；

建模实现的主要代码如下：

k1：用户有无路由功能，决定了该用户能否与其他用户通信。k1为0表示无路由功能，即该用户不能与其他任何用户进行通信。路由功能是用户的基本功能，如果无k1，那么肯定无后续的k2、k3与k4。相应地，k1为1表示有路由功能。

k2：用户有无钱包功能，决定了该用户能否与其他用户交易。k2为0表示无钱包功能，即该用户不能与其他任何用户进行交易，简单地说，因为该用户没有钱进行交易。钱包功能也是用户的基本功能之一，如果无k2，那么肯定无后续的k3与k4。相应地，k2为1表示有钱包功能。

k3：用户有无挖矿功能，决定了该用户是否具有获取奖励的资格及共识机制是否有效。k3为0表示无挖矿功能，即该用户不能参与挖矿，也得不到奖励。挖矿功能是用户的高级功能之一，少数用户才具有。相应地，k3为1表示有挖矿功能。

k4：用户有无管理功能，决定了该用户是否具有发行货币的权利。k4为0表示无管理功能，即该用户不能发行货币。管理功能是用户能具有的最高权力功能，一个系统只有唯一一个用户具有管理功能，负责整个区块链系统的货币发放，该用户所扮演的角色也就相当于区块链系统本身。相应地，k4为1表示有管理功能。

在本发明实施例中，由于是验证的安全性性质，所以选取的性质为：转账发生的条件验证，避免无必要的转账发生。

性质描述：如果没有路由或没有钱包或发送方余额不足，那么将不能交易。

上述性质等价于：如果发生了交易，那么交易双方一定具有路由，且有钱包，且发送方余额够支付。具体描述如下：

define p：交易双方有路由；

define q：交易双方有钱包；

define r：交易发送方钱够；

define c：交易成功

性质描述为PPTL公式为：[](<>c—>p∧q∧r)

需要验证[](<>c—>p∧q∧r)是否成立。该公式表示的性质是，当交易发生时，一定有p、q和r这三个原子命题同时成立。而p、q和r这三个原子命题表示的含义分别是：交易双方有路由；交易双方有钱包；交易发送方钱够。这也就是交易发生的必要条件。如果此公式满足，则证明区块链转账安全性性质可满足，否则不满足。

验证性质结果：

满足，所述MC返回结果如图8所示。

以上所述仅为本发明的较佳实施例而已，并不用以限制本发明，凡在本发明的精神和原则之内所作的任何修改、等同替换和改进等，均应包含在本发明的保护范围之内。

Claims

1.一种基于MSVL的区块链系统建模和安全性验证的方法，其特征在于，所述基于MSVL的区块链系统建模和安全性验证的方法在MC中用MSVL对区块链系统建模，用程序p表示；用PPTL描述区块链系统的性质，用公式φ表示；在MC中，加入MSVL的建模程序p和用PPTL描述的性质φ，验证区块链系统的安全性。

2.如权利要求1所述的基于MSVL的区块链系统建模和安全性验证的方法，其特征在于，所述基于MSVL的区块链系统建模和安全性验证的方法利用MSVL程序p对区块链系统进行建模；利用PPTL公式φ描述区块链系统的性质。

3.如权利要求1所述的基于MSVL的区块链系统建模和安全性验证的方法，其特征在于，所述基于MSVL的区块链系统建模和安全性验证的方法包括以下步骤：

4.如权利要求3所述的基于MSVL的区块链系统建模和安全性验证的方法，其特征在于，使用MSVL语言对区块链系统建模的区块链系统中的用户类型分为四种，分别用四个参数表示具体为：

区块链中的区块信息用结构体struct Block表示；

区块链中的交易信息用结构体struct Trade表示；

区块链中的用户信息用结构体struct Nodes表示；

区块链中的用户间通信用结构体struct Edges表示；

使用MSVL中的函数表示区块链系统中的功能，具体为：

function pass表示进入区块链系统的一个简单的身份认证函数；

function pay表示一条交易中的转账支付的函数；

function record表示生成新区块前的所有交易记录的函数；

function p2p表示p2p网络用户结点及其相互通信的遍历检测函数。

5.如权利要求3所述的基于MSVL的区块链系统建模和安全性验证的方法，其特征在于，PPTL公式根据具体要验证的安全性性质确定，首先根据需要验证的性质，定义命题；然后根据命题的逻辑关系，得出相应合理的PPTL公式。

6.如权利要求3所述的基于MSVL的区块链系统建模和安全性验证的方法，其特征在于，用MSVL对需要进行验证的区块链系统进行建模的方法具体包括：

(1)建模程序中的用户类型用四个参数表示：

(2)定义四个结构体来表示区块链系统中的用户、交易、区块；结构体struct Block：区块链中的区块信息用结构体struct Block表示，结构体包括五个成员：ID用来表示当前区块的摘要值；preID用来表示前一区块的摘要值；Ntrade用来表示所有交易的交易打包摘要值，即Merkle树根结点的hash值；x用来表示挖矿过程生成的随机数；t用来表示时间戳；

(3)区块链系统中的功能用函数表示，具体为：

function pass表示进入区块链系统的一个简单的身份认证函数；

function pay表示一条交易中的转账支付的函数；

function record表示生成新区块前的所有交易记录的函数；

7.如权利要求6所述的基于MSVL的区块链系统建模和安全性验证的方法，其特征在于，结构体struct Trade：区块链中的交易信息用结构体struct Trade表示，结构体包括四个成员：num用来表示交易编号；fromNode用来表示交易的发送者；toNode用来表示交易的接受者；payBalancekey用来表示交易金额；

结构体struct Nodes：区块链中的用户信息用结构体struct Nodes表示，结构体包括八个成员：address用来表示用户的地址，用于存储账户余额的地址；k1表示的是用户有无路由功能；k2表示的是用户有无钱包功能；k3表示的是用户有无挖矿功能；k4表示的是用户有无管理功能；sendBalance用来表示发行奖励的货币额度；Balance用来表示账户余额；baac表示共识机制中每个用户的活跃度与信用度所占比重，权重比例决定奖励；

8.如权利要求3所述的基于MSVL的区块链系统建模和安全性验证的方法，其特征在于，数据层需要的性质用PPTL公式描述并验证为：

发生了交易，且有钱包，且发送方余额够支付，具体描述：

define p：交易双方有路由；

define q：交易双方有钱包；

define r：交易发送方钱够；

define c：交易成功；

性质描述为PPTL公式为：[](<>c—>p∧q∧r)。

9.一种实施权利要求1所述基于MSVL的区块链系统建模和安全性验证的方法的基于MSVL的区块链系统建模和安全性验证的系统，其特征在于，所述基于MSVL的区块链系统建模和安全性验证的系统包括：

验证模块，用于检查区块链系统的安全性性质是否满足。

10.一种实现权利要求1～8任意一项所述基于MSVL的区块链系统建模和安全性验证的方法的信息数据处理终端。