区块链：研究与应用2（2021）100024支持完整性分析的多方区块链系统的建模方案罗辛光a，b，*，施泰博a，b，徐希伟a，baData61，CSIRO，悉尼，澳大利亚b新南威尔士大学计算机科学与工程学院，悉尼，新南威尔士州2052，澳大利亚A R T I C L E I N F O关键词：区块链数据完整性多方系统安全协议区块链异常A B S T R A C T多方系统对于业务流程很重要，但可能很复杂。区块链通过提供透明度、分散控制和不可变的交易历史来促进多方系统中的信任，以提高各方之间的安全性和问责制在区块链系统中使用加密散列和持续验证共享分类账，为各方提供了历史交易的数据完整性和智能合约执行的流程完整然而，在将区块链与链下组件相结合的更广泛系统的设计本文提出了两种建模方案，以更好地理解区块链对基于多方区块链的系统中的完整性的支持 该方案将架构中组件之间的交互建模为安全协议，以供标准技术和工具分析。我们首先说明如何将基于区块链的系统直接抽象建模为安全协议。然后，我们将展示如何对区块链特有的问题进行编码，例如基于共识的“分叉”（也称为“孤儿块”或“叔叔块”）。这允许事务重新排序行为在模型中表现出来，并允许检查该问题的设计缓解 我们通过分析三种设计方案来说明我们的方法，这些设计方案可能增强多方共享贸易证书的系统。1. 介绍多方系统是组织间业务流程的基础。它们从数据或流程的角度支持实体和组织之间的交互多方系统中的利益相关者为了共同的业务绩效而协作，但可能具有有限的信任。利益相关者持有碎片或冗余的数据副本，并按照各种流程进行通信。因此，数据完整性和过程完整性都是多方系统中的挑战对数据或流程完整性缺乏信心可能导致利益相关者及其业务运营出现成本或质量问题。例如，如果供应链中的利益相关者对另一方提供的文件的完整性没有信心，他们可能需要与第三方进行复杂的辅助过程，以独立验证这些文件。缺乏流程完整性可能会导致错过授权或支付等活动或以错误的顺序执行。区块链系统提供了透明度，分散控制和不可变的历史交易，这有助于改善多方系统中的问责制和数据完整性区块链系统使用不可变和仅附加的数据存储，并使用关于数据更新规则执行的分散共识。区块链系统不是完全依赖第三方来运行集中式系统，而是在利益相关者之间建立中立的基础，他们可以在分散的网络中共享数据。对共享数据的更改可以永久记录和跟踪。通常，基于区块链的系统包括区块链和链下组件。链下组件是不属于核心区块链网络的外部系统 在基于区块链的系统中，除了区块链之外的所有组件都被认为是链外的。还引入了链下组件来抵消区块链的不受欢迎的属性，例如低可扩展性和高延迟。链下数据的数据完整性可以通过将加密散列附加到共享分类账来支持，以允许独立访问据称原始数据的其他方进行交叉检查。 通过在区块链上记录流程状态并确保对该数据的更新符合流程，可以支持流程完整性* 通讯作者。澳大利亚悉尼新南威尔士大学计算机科学与工程学院电子邮件地址：SinKuang. data61.csiro.au（S.K. Lo），Mark. data61.csiro.au（M. Staples），Xiwei.Xu@ data61.csiro.au（X. Xu）.https://doi.org/10.1016/j.bcra.2021.100024接收日期：2021年3月21日;接收日期：2021年6月9日;接受日期：2021年7月17日2096-7209/©2021作者。出版社：Elsevier B.V.代表浙江大学出版社。这是一个在CC BY-NC-ND许可下的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）中找到。可在ScienceDirect上获得目录列表区块链：研究与应用杂志主页：www.journals.elsevier.com/blockchain-research-and-applicationsS.K. Lo等区块链：研究与应用2（2021）1000242完整性规则[1]。然而，在一个更广泛的基于区块链的系统[2]中，将区块链与链下组件和多个利益相关者相结合，可能会有复杂的流程交互和数据依赖。当链下交易依赖于链上交易时，某些区块链中潜在的交易重新排序行为也会产生不确定性。因此，在基于区块链的系统中如何支持完整性可能尚不清楚在本文中，我们提出了两种方案来建模基于多方区块链的系统的架构，以支持完整性分析。各方和架构组件之间的交互以特定的方式建模为安全协议，并使用标准的安全协议分析工具进行分析。第一种方案适用于具有概率终结性的区块链，其中基于共识的分叉（也称为“叔叔块”或“孤儿块”）使用非确定性包含交易的方案进行建模。 这允许出现交易重新排序问题（称为“区块链异常”[3]），并允许检查对该问题的控制。 第二种方案是一种适用于具有绝对有限性的区块链的抽象模型，其中系统可以直接建模为安全协议。 我们通过分析设计替代方案（有和没有区块链）来说明我们的方法，以实现称为ePhyto的真实世界跨司法管辖区贸易证书系统的可能扩展。1在我们的实验室研究中，我们使用过程分析工具包（PAT）2工具。我们的评估使用三个sce- narios来探索设计方案如何影响完整性属性。本文首先在第2节中简要介绍了区块链技术、基于区块链的系统和协议分析工具的背景。相关工作在第3节中讨论。第四节介绍了我们的方案。第4.2节描述了我们的评估方法，使用ePhyto系统和基于Ephyro的设计模型评估。第5节显示了使用我们的方案的结果，并讨论了发现。2. 背景2.1. 区块链区块链使用去中心化架构和加密技术提供不可变的共享账本。 区块链技术可以在不受信任的参与者的分散网络中处理交易。在功能上，区块链可以用作数据存储或计算基础设施。区块链存储网络中参与者执行的所有历史交易区块链分类账中的交易不能被删除或修改。区块链还可以运行称为智能合约的计算机程序作为交易。计算的结果存储在区块链分类账上。非功能性，区块链提供了对不变性，问责制和透明度的支持。历史的、不可变的、仅追加的交易提供了关于存储数据的数据完整性的保证，这对区块链网络中的所有参与者都是可用的。智能合约的安全执行环境确保了它们实现的业务逻辑的流程完整性。区块链平台可以提供公证、支付和可信身份注册等服务[4]。在一个分散的系统中，没有一方控制网络。相反，操作可以由分散网络中的任何参与节点执行和检查。所有参与者都可以保留区块链分类账的副本任何修改交易记录的企图都将对其他当事人显而易见[5]。然而，尽管比特币或以太坊等公共区块链中使用的Nakamoto共识机制可以在数千个匿名节点上运行，但它只提供了弱的交易语义。从一个节点的角度来看，一个最近似乎已经提交到区块链的区块可能后来被删除或重新排序。这是由于节点之间的竞争造成的1https://www.ippc.int/en/ephyto/。2https://pat.comp.nus.edu.sg/。创建新的区块（“矿工”）。 由此产生的替代历史在分类账中显示为称为“分叉”的分支，而不包括在共识分类账中的替代区块有时被称为“叔叔区块”或“孤儿区块”。这导致了区块链异常[3]。一方可能会观察到第一笔交易已被包括在分类账中，然后提交后续的相关交易。在这一点上，如果发生分叉影响第一笔交易的区块，那么第二笔交易（现在在交易池中）可能会在第一笔交易之前被包括在分类账中，从而造成完整性违规。如果第二笔交易是由第一笔交易在分类账上的初始存在触发的链下交易，则会出现类似的异常情况 这种交易重新排序可能会违反诸如创作或支付等流程的流程完整性，这些流程取决于交易的排序。 由于数据完整性会影响流程完整性，因此更好地理解区块链交易重新排序如何影响多方系统的完整性非常重要。还有其他区块链是用各种共识算法实现的。工作量证明（PoW）的一种常见共识算法是权益证明（PoS）。 具有PoS的区块链必须根据其在网络中拥有的硬币数量选择验证器来挖掘或验证区块交易。 PoW和PoS是具有概率确认的Nakamoto Consensus类型。相比之下，具有拜占庭容错（Byzantine Fault Tolerant，BFT）共识机制的区块链具有绝对的有限性。 交易重新排序在BFT区块链上不存在。 在具有BFT的区块链中，必须批准少量众所周知的许可验证器来确认网络中的块。 我们的第二个模型适用于具有绝对最终性的区块链建模。2.2. 过程分析工具众所周知，安全协议很难正确设计。许多形式化的验证技术已经被用来对安全协议进行建模和分析。我们的研究中使用了PAT过程分析工具[6]，但也存在替代工具，如SATMC [7]和ProVerif [8]。PAT可以模拟系统可能的过程流程，以允许对系统进行逻辑推理。PAT使用模型检查技术来检查诸如状态可达性和进程死锁之类的属性PAT允许使用堆栈和队列等数据结构的复杂模型PAT可以以状态转换图的形式对系统或过程流程进行建模。 为了模拟更复杂的系统，多个过程可以出现在一个PAT模型中。PAT自动分析状态之间可能的转换，并根据模型中的逻辑定义PAT允许通过命令行或使用PAT提供的灵活的GUI工具来创建状态转换图。PAT可以生成事件跟踪来探索各种声明，例如无死锁性，公平性和可达性。 白色方框中的数字表示事件或状态的顺序，红色方框中的数字表示过程的最终事件。箭头表示状态之间的转换3. 相关工作对基于区块链的系统进行形式化分析的工作很少以前对区块链进行形式化分析的大部分工作都是在底层区块链平台内的共识机制或智能合约上进行的。Dennis等人 [9]对拟议的时间滚动区块链进行了正式分析，旨在解决现有区块链当前规模呈指数增长的问题。他们将他们提出的区块链与通用区块链进行比较，以观察删除附加在区块链上的数据是否会影响他们提出的解决方案的安全性。他们的工作目标是验证他们提出的区块链机制。他们提出的模型只适用于分析具有他们提出的机制的区块链我们提出的S.K. Lo等区块链：研究与应用2（2021）1000243这些计划旨在允许使用标准Nakamoto Consensus对基于区块链的系统进行建模，以研究系统的完整性Amani等人使用Isabelle/HOL来验证以太坊智能合约字节码的行为[10]。他们展示了他们在用Solidity编写的托管协议合同上的方法。Abdellatif等人 提出了一种使用以太坊智能合约正式建模的方法[11]。他们使用静态模型检查方法分析了一个开源的真实世界智能合约Nehailletet al. 还使用Why3演绎程序验证平台对以太坊智能合约进行了建模。他们使用模型检查器来验证智能合约是否符合其规范[12]。所提出的模型涵盖了以太坊网络、合约和EVM（以太坊虚拟机）上的操作。这三个模型只专注于智能合约的建模，而我们的方案则专注于基于区块链的系统的行为。比特币和以太坊的服务可用性之前已经调查过。Weber等人的研究结果显示事务写可用性低于读可用性。他们还报告说，块的提交时间是高度可变的，并且受到网络重新排序的影响[13]。Duan等人模拟了区块链共识，并使用模型检查器验证了区块链的行为[14]。他们以协议的形式模拟区块链共识Bistarelli等人使用PRISM（一种概率模型检查器）来研究区块链的属性[15]。他们的目标是研究分叉或块开采等过程在块中发生的概率我们工作的目标是创建一个抽象模型，可以用来推理使用区块链设计的系统。 我们依赖于关于区块链行为的更抽象的假设，而Bistarelli的工作展示了区块链属性如何从共识协议的设计中产生。我们的分析是在不同的抽象层次，包括与应用及其领域。4. 拟议的建模方案本文的目的是讨论和评估我们提出的建模方案的可行性，以支持基于区块链的系统设计中的完整性分析，其中区块链只是更广泛的多方系统中的一个组件。 第一种方案适用于对区块链的概率终结性进行建模。它允许出现事务重新排序问题，并允许对该问题进行控制。查过了 第二个方案适用于作为安全协议的具有绝对有限性的系统的建模。当设计一个具有概率终结性的系统时，系统设计者必须考虑系统状态可能改变或恢复的可能性。相反，对于一个具有绝对终结性的系统，一旦达到一个状态，系统状态将是终结我们使用我们的方案来模拟一个基于区块链的设计候选人，以增强国际供应链的真实ePhyto贸易证书系统。该设计概念增强了ePhyto系统，为没有直接连接到可信的中央数据交换中心的非政府组织提供贸易证书真实性和流通性的证据一旦真正的ePhyto贸易证书的哈希值被记录在区块链上，所有非政府组织（见图中的红色箭头）都将被记录在区块链上。 1）可以通过将证书的哈希值与区块链上记录的哈希值进行比较来检查其收到的链下证书的完整性（见图2中的虚线箭头）。我们的每个建模方案都有一个链上模型和一个链下模型。链上模型侧重于共识协议和区块链主体，而链下模型侧重于与区块链交互的组件。我们定义完整性条件，以检查候选设计的要求和安全条件。使用协议分析工具检查这些条件。对链上元素建模的步骤在第4.1中描述，对链下元素建模的步骤在第4.2中列出。4.1. 链上元素我们在本节中描述了我们对区块链链上元素建模的方案识别区块链平台的系统行为：首先，识别基于多方区块链的系统中区块链平台的系统级行为由于区块链的分散性，系统流程和行为与传统的集中式系统相比可能有所不同。 不同的区块链使用不同的共识算法实现。将区块链平台的系统行为建模为协议：在收集平台的系统行为和组件信息后，我们可以为区块链平台中的每个组件生成协议模型，以模拟平台的Fig. 1. ePhyto在出口发货人、进口收货人之间开展活动，无论是否连接中央枢纽。●●S.K. Lo等区块链：研究与应用2（2021）1000244图二. 基于区块链的ePhyto发布和传输场景模型。该模型中的区块链元素包括区块加密模型、交易加密模型和确认区块模型（所有三个模型都在第4.1小节中定义，并在图4.1中显示）。分别为3- 5）。EA：出口当局。在这里，我们描述了具有概率finality的区块链的链上建模，包括使用Nakamoto共识的区块链，如比特币和以太坊。 我们使用区块模型、确认区块模型和交易模型对这些区块链的组件和流程进行建模。4.1.1. 块生命周期模型区块链记录区块的顺序列表，每个区块包含交易列表然而，从任何节点的角度来看，最初看起来被记录的区块可能是叔叔/孤儿区块，因此虽然“移除”的区块数量是不确定的，但概率有限性意味着这个过程不可能移除所有区块-为了简单起见，通常建议等待足够数量的“确认区块”，以确保区块不会被从区块链中移除的节点观察到 我们对块生命周期的这些方面进行建模，如图所示. 3. 状态Block_update表示添加新块。有两个过渡。 第一次转换每次都会将Block_Bit的块数增加1。我们用第二次转换来 模拟 节点 对块 移除的观察， 只 要 这 保 持 大 于 当 前 确 认的块 数量confirmed_bits，就可以减少块的数量。当我们删除一个区块i时，我们也删除了该区块的所有交易tX_n（i）但是，这些删除的事务仍然是事务池的一部分，如将其块号设置为零所示。正如我们将看到的，这允许这些交易重新包含在替代或稍后的区块中。4.1.2. 确认块模型随着区块链中区块数量的增加，最近确认的区块数量也应该增加对于关注点的分离，我们对图1中的confirmed块计数器confirmed_index的增加进行了建模。 四、所示的默认条件允许确认的块号增加到比最新的块号小一个，最新的块号模拟最小确认块的数量为一。更长的指定距离将模拟更多数量的最小确认块，例如通常推荐用于比特币的six。请注意，在这里，确认块非确定性地增加，因此悲观地说，不会总是在允许的最大值。4.1.3. 事务处理模型最后，我们对每个事务的生命周期进行建模（图5）。创建后，主要有两种状态：在Pool中等待添加到区块链，然后添加到区块链。当池中的交易被添加到区块链时，它会从区块生命周期模型中获取图三. 块移除模型，显示了添加块的过渡，以及删除叔叔/孤儿块的过渡。我们通过断言可达性声明来验证所有三种模型的正确性。最初的目标是确保分叉可以在我们的模型中发生我们检查t X_t（i）是否可以具有比tX_t（j）更高的block_t值。 基于图1中PAT生成的轨迹， 6（b），它表明块重新排序行为可以在我们的模型中表现出来，这验证了我们的模型按预期工作。在两个事务都从之前的块中删除之后，tX_i（j）被附加在tX _ i（i）4.2. 对链下元素在这里，我们描述了在基于多方区块链的系统中对链下元素进行建模的步骤。捕获链下系统设计：我们捕获多方系统中链下组件的活动图、序列图、数据流程图或业务流程模型我们感兴趣的是各种系统参与者之间的交互，以及系统中传输和交叉检查的数据识别链下系统中的参与者：一旦研究了架构图，我们就可以识别系统中的参与者在多党制中有两种类型的行为者：个人（人民/组织）和制度组成部分。 人可以是与系统打交道的任何人。基于系统的参与者是与其他参与者交互的自动化组件。●●S.K. Lo等区块链：研究与应用2（2021）1000245见图4。确认块模型，显示确认块的过渡。只有当当前块号严格大于确认的块号时才能触发。图五. 交易模型，模拟区块链网络中交易的转移。识别场景：我们捕获了许多系统使用场景，涵盖了数据完整性至关重要的关键交互。完整性条件被定义为对系统目标或要求进行建模。生成流程模型：我们从所有场景的设计中生成流程模型选择的架构图和场景被解释为安全协议，并转换为流程模型。目前，这一步是手动的。作为一个说明性的初始场景，我们创建了一个简单的流程模型，其中有三个参与者，两个后续事务一个接一个地执行，如图所示。第七章 然后我们创建一个更复杂的模型（图）。 2）考虑区块链上的分叉活动。各种目标被用来观察区块链异常如何影响三个参与者之间的交易 目标和结果在第5节中讨论。对于复杂模型，我们将区块链网络模型作为三种相互作用的状态转换模型。这三个过程的过渡相互影响，如果条件允许，它们将相互交错。以下各小节将对它们进行描述为了证明我们的方法中的链下建模，我们应用我们提出的方法来设计供应链环境中的范例系统的替代方案 供应链系统是多方系统的一个很好的例子，因为它们是复杂的，高度动态的，并且有不同的利益相关者。 我们使用它来评估我们的方法的整体可行性，并注意到架构分析结果的优势和局限性。我们的特定示范系统是对国际供应链真实ePhyto贸易认证系统的假设性增强。增强后的ePhyto系统可向未直接连接到可信的中央数据交换中心的非政府组织提供贸易证书真实性的证据4.2.1. 贸易证书系统：ePhytoePhyto证书（电子植物检疫证书）为贸易证书，用于控制进口植物贸易货品的生物安全风险。植物检疫证书证明货物符合进口要求，并由出口国的NPPO（国家植物保护组织）签发。ePhyto系统开发由国际植物保护办公室（IPPO）和联合国共同开发的一种新的认证系统，使用集中式集线器在NPPO之间安全交换XML ePhyto证书。然而，企业并不直接连接到中央枢纽，因此无法使用该系统来检查他们收到的证书的真实性。4.2.2. ePhyto架构图在ePhyto中，各国需要有系统与联合国运营的中央枢纽连接，或者使用枢纽提供的网络接口该中心是一个值得信赖的集中式系统，用于在国家之间转移证书然后，XML ePhyto证书可以呈现为打印文件，看起来类似于传统的纸质植物检疫证书。在图1所示的ePhyto架构中， 1、NPPO利益相关者依靠该中心安全交换权威的ePhyto证书。然而，其他利益相关者，如行业参与者（包括出口商、进口商和物流、贸易融资或贸易保险服务提供商）既不能连接到该中心，也不能访问通用国家系统，因此无法验证ePhyto证书。因此，行业持份者只能转让已批准证书的副本。 （图中虚线矩形区域所示。①的人。我们的研究探讨了这些利益攸关方面临的挑战因此，我们只对虚线矩形内的协议交互进行了建模基于从图中的虚线矩形提取的模型。1、ePhyto流程从出口商向当地政府申请出口许可证开始，提供产品类型、数量、运输期、产品成本、产品重量、进口公司和进口国家等详细信息。检查可由主管部门进行。还可能需要支持文件（如集装箱熏蒸证书），并可能“附加”到ePhyto证书上。出口当局将批准或拒绝申请。如果获得批准，将向出口商发出证书，允许他们将该批货物出口到该特定目的地。货物承运人将获得该证书以向目的地国家的海关出示（在我们的研究中，关于载体的细节被抽象化，以简化和集中我们的研究。证书及货物于最终交付前由进口国海关人员检查●●S.K. Lo等区块链：研究与应用2（2021）1000246图第六章 PAT（流程分析工具包）跟踪：（a）无块重排异常(b)红色虚线方块表示区块链异常。4.2.3. 演员在ePhyto本节介绍了这一过程中的参与者。EX porting consignor（EC）是发起流程以向出口授权。他们的目标是合法地将产品出口到进口国。出口管理局（EA）是批准或拒绝欧盟出口申请的授权实体，所有出口申请必须得到EA的批准，然后才能出口货物经批准后，由他们颁发证书收货人（IC）是从欧共体进口产品的实体他们希望证书存在，并且是真实的。Hub是由联合国管理的中央基础设施。该中心使各国能够通过该中心将真实的ePhyto证书转移到其他国家。4.2.4. ePhyto系统协议本节描述系统协议中的数据交换，如图1所示。有三个主要步骤。EC导出应用程序请求（EC-EA）在第一步中，EC以明文形式向EA发送导出应用程序请求 请求书包括货物的详细资料和进口国。 我们假设EC只发送正确的信息，因为EA会检查。由于我们主要关注证书发出后的安全性，因此本研究摘录了EA对请求的EA签发批准的出口文件（EA - EC）在批准EC的出口请求后，EA将通过中心向EC我们假设EA诚实行事，不会篡改证书。EC将批准文件转移到IC（EC-IC）一旦EC收到EA的证书，他们就可以完成货物的出口。我们在研究中对这些物流安排进行了抽象，因为任何欺诈活动（如货物替代）都被假定能够被进口海关代理识别如果EC或其他中介机构篡改证书，系统应允许EC和IC识别欺诈活动。伦理委员会将通过电子邮件将批准文件发送给IC。海关等官员可访问ePhyto中心以交叉检查文件的真实性，但供应链中的其他行业参与者则不能。现行制度有若干限制首先，行业参与者无法验证证书的真实性和完整性。第二，出口公司或货物承运人在从出口作者处收到批准的出口文件后，可能篡改这些文件。其次，如果出口当局撤销或重新颁发证书，行业参与者或纸质文件持有人无法检查。4.2.5. ePhyto系统我们探讨三种情况下，这是建模为系统中的参与者的互动场景1：签发植物检疫证书签发植物检疫证书的开始是因为欧盟委员会打算将货物出口到另一个国家。该过程始于欧盟委员会向出口当局申请证书一名官员将审查申请，并可能进行实际检查。 如有任何需要更改，将通知伦理委员会修改其申请以重新提交。 一旦不需要进一步更改，EA将批准并颁发植物检疫证书。证书将通过电子邮件发送给EC（另一个不在本模型范围内的交互是EC与ePhyto中心的交互情况2：更换植物检疫证书在某些情况下，如果计划装运有微小的更新，植物检疫证书可能会重新颁发。 EA将向申请人颁发具有新编号的证书的新替换版本，旧证书将不再有效。情况3：取消植物检疫证书有时必须由EA取消或撤回证书。 退出请求将被转发到EA。EA将根据以下要求提供信息：●●●S.K. Lo等区块链：研究与应用2（2021）1000247图第七章 一个简单的状态转换模型示例，以ePhyto为例。圆圈是状态，线条是转换。需求一旦不需要额外的信息可以向EC发出撤回5. 结果和讨论我们在PAT中模拟了参与者该流程模型是从原始ePhyto系统流程图中提取的。过程模型由两名独立的研究人员检查，以确保它反映了原始过程。由于我们的目标是验证使用区块链对多方系统安全性的影响，因此我们使用PAT中的可达性声明。可达性声明是一种断言，即在过程中可以达到（坏的）预定义状态;我们希望工具显示这些状态是不可达的。我们定义了模型要达到的多个目标，并允许PAT探索所有可能的状态。如果达到目标状态，将报告过程跟踪，逐步显示不良行为我们专注于在多方系统中传输的数据的完整性，并分析了不同的设计方案将如何影响每个设计中的攻击涵盖所有交互点的过程跟踪将由PAT生成结果将在下一节中讨论网络安全和物理威胁都可能导致生物安全风险。攻击者可以针对实体商品，运输，网络安全弱点，或结合多种方法进行攻击。在ePhyto上下文中，攻击者可能会尝试利用完整性弱点来实现无效的运输溢出、伪造（替代）或篡改威胁。5.1. 数据完整性5.1.1. 情景1：签发植物检疫证书基于图1所示的当前实践状态的过程。1，我们可以预测以下攻击：当EC收到EA通过电子邮件发出的植物检疫证书时，EC篡改证书，然后将其发送给IC或其他第三方。即使EA没有颁发有效证书，EC也可以发送假证书。在这两种情况下，进口当局可以使用中心独立检查和拒绝假证书，但IC和其他第三方不能。这可能有助欧洲共同体以欺诈手段取得贸易融资，或将假证书作为替代品附在另一批替代货物上。图图8显示了从PAT模型生成的轨迹。 数字表示发生过程的顺序。 每个箭头代表模型中的一个过程。最后一个红色方框X显示了进程达到一个定义的目标所生成的结果允许研究人员和实践者对系统进行推理，而无需实际实现整个系统。结果表明，EC可以篡改已批准的出口文件并将其发送给IC。在基线系统中，IC无法验证收到的文档的真实性或完整根据场景1的PAT分析结果，我们可以通过添加区块链作为组件来改进架构这使得EA见图8。PAT（流程分析工具包）生成的事件跟踪示例的一部分。将批准的植物检疫证书的哈希值记录到区块链上。区块链上的哈希值将允许多方系统中的其他参与者检查收到的证书的完整性。我们添加了一个名为BC的新参与者，并修改了之前的场景1协议。新协议如图2所示。收到的植物检疫证书的哈希值和存储在区块链上的哈希值作为参数。使用PAT分析该系统表明，用户仍然可以尝试篡改从授权EA收到的证书，但所有参与者（此处为IC）都可以交叉检查收到的文档的完整性因此，PAT显示Invalid，这意味着只要参与者可以将区块链上的哈希与据称原始文档的哈希进行交叉检查，5.1.2. 方案2：重新签发替代植物检疫证书在场景2中，只在区块链上添加哈希值是不够的。如果证书被重新颁发（更新和替换），那么EA将在区块链上记录两个不同的验证哈希值。原件可能被错误使用。相反，一旦处理了重新颁发阶段，系统必须指向新颁发的证书。因此，需要一个智能合约3在重新签发证书的过程中，应更新证书的版本号，以确保申请人不会重复使用先前批准的证书进行两次出口。EA将部署一个智能合约来绑定所有以前颁发的证书和最新的证书。在批准重新颁发过程后，EA将向申请人提供合同地址其中它将始终指向最新批准证书的哈希3或者是一种惯例，当存储哈希值时，也存储现在无效的先前证书的哈希值。我们在这里模拟使用智能合约作为说明性解决方案，以允许更新智能合约中记录的变量的最新状态●●S.K. Lo等区块链：研究与应用2（2021）1000248并且还将向申请人提供较新的文档 在这个过程中，参与者可以交叉检查智能合约，它将始终指向区块链上新记录的证书哈希，以确保收到的证书的完整性。在PAT模型中，当EA重新颁发证书时，EA将把最新的哈希值附加到前一个哈希值的集合中（使用PAT上的列表结构）。EC或IC接收到的较旧的哈希值将充当指向最新哈希值的指针当EC或IC在区块链上检查过时的哈希值时，它会指向最新的哈希值，因此他们可以判断他们的证书是否过时。5.1.3. 方案3：撤销植物检疫证书记录在区块链上的数据是不可修改的，因此被撤回证书的哈希值仍将在分类账上。 EA将销毁智能合约，并将智能合约的地址绑定到撤回通知并发送给EC。假设2和假设3的结果与假设1相似。由于篇幅的限制，本文不包括这方面的结果基于对所有三种场景的PAT分析，我们可以看到将区块链添加到这个多方系统中如何有助于提高系统的完整性。通过将外部数据的哈希值添加到区块链上，系统中的所有参与者都可以交叉检查和验证该数据的完整性。5.2. 过程完整性在我们的两个后续交易的模型中，如图所示。7、第一笔交易应该在第二笔交易之前附加在区块链上。从图2中PAT生成的过程跟踪中，在图6（b）中，我们可以观察到第一笔交易在第二笔交易之前被附加到一个区块上。在几个区块之后，包含第一个交易和第二个交易的区块被删除，两个交易都回到了交易池。 后来，第二笔交易被添加到第一笔交易之前的区块中。PAT跟踪表明，区块链异常[3]可能会发生，并且区块重新排序将改变附加到区块的交易序列。一种解决方案是使用智能合约在进行下一笔交易之前检查上一笔交易的存在通过添加先决条件检查，如果前一个事务不再在链上，则事务将停止执行。虽然第二个交易可能会在第一个交易被从区块中删除之前执行，但由于第一个交易不存在，因此进一步向下的交易将停止执行。 添加条件后，我们再次运行PAT来验证第二个事务是否可以在第一个事务之前发生。从图中的PAT结果。6（a），我们观察到第一笔交易总是在第二笔交易之前发生。另一种解决方案是应用X确认模式[2]，等待交易后足够数量的区块，这样它在共识分叉中的移除就不太可能了，以至于可以假设它是不可能的。之后，我们可以安全地添加第二个事务。这在流程模型中通过为每个利益相关者设置一个条件来表示，只有当当前区块号是在相关交易的区块号之后的安全区块数时，才能继续进行操作（例如，检查交易/散列）（例如，ePhyto证书）。5.3. 限制目前，我们假设区块链组件是安全和防篡改的（除了建模的短共识分叉）。实际上，在公共区块链网络中有几个硬分叉[16，17]，可以使以前有效的交易无效。虽然我们的方法是通用的，但我们基于区块链的应用模型目前针对每个场景中的交互尽管如此，我们希望我们的区块链模型对其他sce-narios的更改可以被模板化，以实现跨场景和系统架构的更系统的重用。在我们的模型中，我们假设出口管理局总是诚实地向出口发货人提供带有正确信息的证书。然而，原则上，他们可能会与进出口托运人合作，批准一份含有虚假信息的证书。整个供应链的系统性腐败可能意味着参与者相互合作接受进口商品，即使证书与区块链上记录的哈希值不匹配。我们将区块确认过程建模为简单模型，其中当当前区块数量大于确认的区块数量时，模型可以增加更现实的做法是将区块确认过程视为概率过程，以更好地反映真实区块链网络中的区块确认过程这可以帮助我们计算共识分叉的风险范围，以更好地配置确认区块的数量，以匹配交易的价值6. 今后工作协议模型可以扩展更多的参与者，以构建更完整的ePhyto系统模型例如，我们可以为贸易融资提供商等其他参与者建模，并包括进口收货人之间的进一步互动。PAT的分析假设所有可能的攻击都是同样可能的，但也可以为不同类型的攻击分配不同的概率或将需要不同的分析技术，例如基于可靠性模型或成本模型的技术这可以让我们检查使用公共区块链与私有区块链作为组件的架构替代方案之间的差异。其他潜在的未来工作包括自动化多方系统和区块链流程的模型生成7. 结论在本文中，我们提出了两种建模方案，以支持基于区块链的系统的架构设计方案的完整性分析。第一种适用于具有概率终结性的区块链，其中基于共识的分叉（也称为“叔叔块”或“孤儿块”）是使用不确定性交易包含方案建模的。第二种是适用于具有绝对有限性区块链的抽象模型，其中系统可以直接建模为安全协议。 我们通过建模和分析设计的完整性方面来展示我们方案的可行性，以可能扩展ePhyto，一个多方贸易证书系统。我们的评估考虑了三个相互作用的情况下，每个模型作为一个单独的过程。我们的分析表明，没有区块链的设计允许不受信任的出口商（或对出口商通信的中间人攻击）向其他行业利益相关者发送虚假证书 在区块链的设计中，使用区块链上的权威机构记录的证书哈希来检测假证书。通过区块链上的哈希，对链下证书文档的任何修改都将对连接到区块链网络的所有参与者显而易见PAT表明，只要颁发机构和区块链是值得信赖的，证书的完整性就可以得到保证。结果证明了使用我们的方法来建模和分析基于区块链的系统作为安全协议的可行性。竞合利益作者声明，他们没有已知的竞争性经济利益或个人关系，可能会影响本文报告的工作。S.K. Lo等区块链：研究与应用2（2021）1000249引用[1] I. Weber，X.许河，巴西-地Rivert等人，不可信的业务流程监控和执行使用区块链，在：M。La Rosa，P. Loos，O.牧师（编辑），BPM 2016：业务流程管理，Springer，Cham，France，2016，pp. 329- 347[2] X.徐岛韦伯，M。Staples，区块链应用架构，Springer，2019年。[3] C. Natoli，V. Gramoli，区块链异常，在：2016 IEEE第15届网络计算和应用国际研讨会（NCA）; 2016年10月31日至11月2日;剑桥，MA，美国，IEEE，Piscataway，NJ，美国，2016年，pp. 310- 317[4] A. Wright，P. De Filippi，Decentralized Blockchain Technology and the Rise oflex cryptographia，SSRN（2015）. https://doi.org/10.2139/ssrn.2580664网站。[5] I. O€nder，H. Treiblmaier，区块链和旅游业：三个研究命题，Ann。Tourism Res. 72（C）（2018）180[6] Y. 刘，J.Sun，J.S.Dong，Pat 3：An extensible architecture for building multi-domainmodel checkers，in：2011 IEEE 22nd International Symposium onSoftwareReliability Engineering; 29 Nov- 2 Dec 2011; Hiroshima，Japan，IEEE，Piscataway，NJ，USA，2011，pp. 190- 199.[7] A.阿曼多湖Compagna，Satmc：一个基于sat的安全协议模型检查器，在：J.J.Alferes，J.Leite（编辑），《人工智能中的逻辑学》，施普林格，柏林，海德堡，2004年，第100页。 七三零七三三[8] B. Blanchet，符号模型中安全协议的自动验证：验证者ProVerif。 《安全分析与设计基础VII》，施普林格，法国，2014年，pp. 54比87[9] R. Dennis，G.欧文斯湾Aziz，A temporal blockchain：a formal analysis，in：2016International Conference on Collaboration Technologies and Systems（CTS）;31Oct- 4 Nov 2016; Orlando，FL，USA，IEEE，Piscataway，NJ，USA，2016，pp.430- 437[10] S.Amani，M.B'egel ，M.Bortin等人 ，TowardsverifyingEthereumsmartcontractbytecode in Isabelle/HOL，in：Proceedings of the 7th ACMSIGPLAN InternationalConference on CertifiedPrograms and Proofs; 8- 9 Jan2018; Los Angeles，CA，USA，ACM，New York，NY，USA，2018，pp.66比77[11] T. Abdellatif，K.- L. Brousmiche，基于用户和区块链行为模型的智能合约的正式验证，在：2018年第9届IFIP新技术，移动性和安全国际会议（NTMS）; 2018年
我的内容管理
展开
