Formal Modeling and Verification of a Blockchain-Based Crowdsourcing Consensus Protocol

Crowdsourcing is an effective technique that allows humans to solve complex problems that are hard to accomplish by automated tools. Some significant challenges in crowdsourcing systems include avoiding security attacks, effective trust management, and ensuring the system’s correctness. Blockchain is a promising technology that can be efficiently exploited to address security and trust issues. The consensus protocol is a core component of a blockchain network through which all the blockchain peers achieve an agreement about the state of the distributed ledger. Therefore, its security, trustworthiness, and correctness have vital importance. This work proposes a Secure and Trustworthy Blockchain-based Crowdsourcing (STBC) consensus protocol to address these challenges. Model checking is an effective and automatic technique based on formal methods that is utilized to ensure the correctness of STBC consensus protocol. The proposed consensus protocol’s formal specification is described using Communicating Sequential Programs (CSP#). Safety, fault tolerance, leader trust, and validators’ trust are important properties for a consensus protocol, which are formally specified through Linear Temporal Logic (LTL) to prevent several security attacks, such as blockchain fork, selfish mining, and invalid block insertion. Process Analysis Toolkit (PAT) is utilized for the formal verification of the proposed consensus protocol.

SECTION I. Introduction

Crowdsourcing is an effective way to solve complex problems by outsourcing to a crowd of people [1]. In recent years, it has gained considerable attention in academia and adoption in the industry. A large number of companies are using crowdsourcing as a method to solve critical problems. Human intelligence-based crowdsourcing consists of service consumers, service providers, and a crowdsourcing platform, as shown in Figure 1.

FIGURE 1.

Traditional crowdsourcing system.

Mechanical Turk [2], Upwork [3] and Uber [4] are some of the famous crowdsourcing platforms. In crowdsourcing, service consumers post tasks through a crowdsourcing platform that are hard to solve for computers but are comparatively easy for humans. In some platforms, such as Upwork, a service consumer needs to deposit the payment as an escrow amount to a crowdsourcing platform before a task begins. The interested service providers receive tasks through a crowdsourcing platform. They compete to solve and submit solutions of tasks to the crowdsourcing platform. The service consumers then select the appropriate solutions, and the corresponding service providers get the task payment.

Crowdsourcing has a wide range of applications in various security-critical systems, for example, disaster management systems [5], traffic monitoring systems [6], and healthcare systems [7]. With the rapid development of crowdsourcing applications, the limitations of traditional crowdsourcing systems are exposed. Firstly, the traditional crowdsourcing systems are based on centralized servers, which can suffer from a single point of failure [8]. Secondly, in case of a dispute between service providers and consumers, issues of free riding and false reporting can occur due to a lack of accountability and effective trust management [9]. In free riding, service providers try to get rewards without providing satisfactory solutions, and in false reporting, service consumers intentionally get useful solutions without losing the deposit. Thirdly, crowdsourcing systems are vulnerable to various security attacks, such as sybil, distributed denial of service (DDoS), and hijacking attacks [10]. Fourthly, sensitive information of users is at risk of privacy disclosure during the process of task assignment [11]. Lastly, there is minimal work on the formal verification of crowdsourcing systems to ensure the correctness, consistency, and completeness of the algorithms and protocols [12]. The advent of blockchain technology [13] brings high hopes to overcome most of the drawbacks in traditional crowdsourcing systems. A consensus protocol is the most critical component of blockchain which can establish mutual trust among crowdsourcing participants in a decentralized way. Therefore, crowdsourcing issues are solved using blockchain consensus algorithms.

A. Motivation for a New Consensus Protocol

Most of the existing generic blockchain consensus protocols have certain limitations. For example, Proof of Work (PoW) is highly resource-intensive and difficult to apply for large-scale online systems [13]. Employing Proof of Stake (PoS) in crowdsourcing systems may compromise the rights of nodes [14] as it suffers from security, fairness, and centralization issues. Delegated Proof of Stake (DPoS) handles the fairness issue by democratic voting, but still, it has some degree of centralization [15]. Moreover, employing DPoS cannot avoid collusion among stakeholders. Therefore, an application-specific blockchain consensus protocol is highly desirable, considering the peculiarities of crowdsourcing systems [16], [17]. To address the security and trust challenges, some recent studies [18]–​[20] have proposed blockchain-based consensus protocols for crowdsourcing applications that also strive to handle accountability, credible crowdsourcing, free riding, and false reporting, and compelling trust management issues. These studies were the prime motivation behind this work.

Several drawbacks are identified in the existing blockcha-in-based crowdsourcing consensus protocols. For example, Proof of Trust (PoT) elects a leader from ledger nodes using Reliable-Replicated-Redundant And Fault-Tolerant (RAFT) and validators from crowdsourcing service participants based on trust values [18]. However, PoT analyzes some of the security attacks, including sybil, DDoS, and collusion through simulations, and theoretically describes a few of the security properties. An improved PoT is a reputation-based protocol in which a high reputation worker is selected as a miner of the block, and verification nodes are also selected based on reputation [19]. However, the reputation calculation is based on the historical interaction of a miner and feedback of other nodes that may not be reliable. It is based on simulation techniques and analyzes collusion attacks. Mobile Crowdsourcing (MCS) chain is based on the total payment for block generation which informally analyzes security properties [20]. The consensus protocol of zkCrowd is based on DPoS and Practical Byzantine Fault Tolerance (PBFT) and is validated using simulation techniques, which favors voters having more tokens [21]. The RAFT and PBFT used in the existing blockchain-based crow-dsourcing consensus protocols are formally verified [22]–​[24], therefore, PoT and zkCrowd are partially verified. The existing blockchain-based crowdsourcing consensus protocols discussed-above employ simulation techniques that do not assure the models’ correctness as simulations are performed on limited data set.

B. Challenges

The weaknesses of the existing blockchain-based crowdsourcing consensus protocols present the following challenges.

1. How to design a secure and trustworthy consensus protocol that applies to crowdsourcing services?

   1. How to prevent security attacks, such as blockchain fork, invalid block insertion, and selfish mining?

   2. How to select trusted leader and validators to prevent their malicious behaviors?

2. How to ensure the correctness of the blockchain-based crowdsourcing consensus protocol?

C. Contributions

This research work aims to present a formally verified Secure and Trustworthy Blockchain-based Cr-owdsourcing (STBC) consensus protocol to deal with the above-discussed challenges. The consensus protocol is nam-ed as STBC because we have defined the security properties of the protocol and trustworthy selection process of a leader and validators based on trust factors. The peculiarities of the STBC consensus protocol are:

1. It records the activities of service providers and consumers, e.g., post, receive, and perform tasks as transactions, and the transactions that gain maximum votes are included in the proposed block.

2. The service consumers have to escrow deposit when they post a task, and the service providers get their share from the escrowed deposit after the successful completion of a task. When the service providers and consumers perform activities, their activity rate is incremented.

3. It selects a trusted leader from blockchain management nodes to propose a block and trusted validators from blockchain management nodes, crowdsourcing service providers, and consumers to validate and vote for the transactions and the block. The trusted leader and validators have to escrow deposit to prevent malicious behaviors.

4. Unlike the existing consensus protocols of blockchain-based crowdsourcing [18]–​[21], the selection criteria of a leader and the validators are different. While the leader is selected based on three trust factors (i.e., deposit ratio, activity rate, missed rate), the validators are chosen based on deposit ratio and activity rate.

The STBC consensus protocol prevents blockchain fork, selfish mining, and invalid block insertion attacks. In STBC consensus protocol, at most one block is proposed in every round, which avoids the possibility of a blockchain fork. If multiple nodes propose a block simultaneously, then blockchain can fork. A single leader is selected to propose a block in each round of consensus to prevent this situation. A successfully generated block that is accepted by a majority of the validators is only added in the blockchain. In this way, all the nodes record the same block, which ensures the absence of a fork. Moreover, only the block of a trusted leader is added to the blockchain which prevents selfish mining attack. If a leader acts maliciously to add an invalid block, the consensus protocol resists it by adding no block.

The guarantee of correctness of any system is essential, especially critical and real-time systems. As a crowdsourcing system involves several critical tasks, therefore its correctness has vital importance. Formal methods are rigorous mathematical techniques to model computer systems that help designers verify the system’s properties and assist in system testing to increase the confidence of correctness of a system. Model checking is an important formal methods-based technique used for the formal verification of critical systems. It is automatic, effective, and requires less human intervention. Therefore, it is utilized in this work.

The main contributions of this work are summarized below:

1. Security: The proposed consensus protocol provides security by defining security properties, i.e., safety and fault tolerance to prevent blockchain fork and selfish mining attacks. It is secure when at most $\left \lfloor{ \frac {n-1}{3}}\right \rfloor $ nodes are faulty. Here n denotes the total number of nodes. This ratio is assumed similar to most of the byzantine fault tolerance (BFT) consensus protocols.

2. Trustworthy: We presented an improved trust model based on several new factors such as deposit ratio, activity rate, and missed rate. The leader and validators’ trust properties are defined to prevent blockchain fork, selfish mining, and invalid block insertion attacks.

3. Fairness: The proposed consensus protocol provides a fair environment for the selection of leaders and validators. The activity rate is included to prevent rich nodes dominating the network. The introduction of missed rate of a node will increase its chances to be selected as a leader. The trust values update mechanism enforces nodes to obey protocol rules; because in the case of malicious activity, in addition to trust values, they also lose their deposit as a punishment.

4. Energy-saving: The protocol saves energy as a single leader is supposed to propose a block in every round.

5. Correctness: The correctness of the proposed consensus protocol is ensured utilizing a formal methods-based technique, i.e., model checking. The formal specification of the proposed STBC protocol is performed using CSP#. Furthermore, the PAT model checker is applied for the formal verification of safety, fault tolerance, leader trust, and validators’ trust properties. Linear Temporal Logic (LTL) is utilized to specify the security and trust properties.

This work is novel in formal modeling and verification of the consensus protocol for a blockchain-based crowdsourcing system ensuring safety, fault tolerance, leader trust, and validators’ trust. Albeit there are some formally verified blockc-hain consensus protocols [25]–​[28], some of the existing consensus protocols for a blockchain-based crowdsourcing system are partially verified [18], [21]. This work is different from [25]–​[28] as the proposed protocol is designed for a crowdsourcing application and in comparison to [18], [21] the proposed consensus protocol is formally verified.

The rest of the paper is organized as follows: Section II establishes the background knowledge; Section III discusses the related work; Section IV presents the system model; Section V defines the formal model of the proposed protocol; Section VI describes the results; and finally Section VII presents the conclusion and future work.

SECTION II. Background

This section provides background knowledge about blockchain and formal modeling and verification.

A. Blockchain Technology

Blockchain technology was introduced by an unknown person Satoshi Nakamoto, as a distributed, peer-to-peer, decentralized, and a linked structure to address the issue of double-spending [13]. Figure 2 represents an example of blockchain. The transactions are grouped and ordered in a structure called a block. In addition to transactions, a block contains its hash and the previous block hash. The variable Prev. Block Hash in the current block in Figure 2 is used to link the block to its previous block which prevents alteration of blocks and insertion of a block between existing blocks. The miners are responsible for adding the blocks in chronological order. In the blockchain, any node can initiate a transaction and broadcast it to the nodes of the network. The network nodes validate transactions and the miner of the block adds the validated transactions to the blockchain. The number of transactions in a block depends upon the size of a block.

FIGURE 2.

An example of blockchain.

Blockchain have applications in various fields, for example, healthcare [29], banking sector [30], insurance companies [31], and crowdsourcing [32]. In this work blockchain is exploited for crowdsourcing systems, as it helps to provide accountability, transparency, and immutability to avoid unfaithful and dishonest behaviors.

B. Formal Modeling and Verification

Formal modeling and verification of consensus protocols is important to ensure their correctness. Model checking is the formal methods-based technique that is effectively used for formal verification. Model checking involves verifying whether a formal model of the system satisfies the desired properties. Model checking technique is useful to reveal the errors that cannot be identified using testing and simulation techniques. In this work, we use the model checking technique because in comparison to other techniques, e.g., theorem proving, it is more effective, automatic, and needs less human involvement. Model checking technique is useful to check partial specifications. However, the state explosion problem is a big limitation of the model checking approach [33], as the state of the model grows infinitely large with the increase of variables, distinct values, and components.

CSP# is a formal specification language used for the formal modeling of concurrent aspects of critical systems. The high-level modeling constructs such as sequential/parallel composition, channels, and interleaving are combined with low-level C# constructs, e.g., variables, if-then-else, and arrays. The syntax of CSP# can be described as:\begin{align*} \begin{array}{lll}&~~ {Proc} ::= \mathrm {SKIP} & ~\,\!~\hspace {-0.4em} (\text {termination}) \\ & | \mathrm {STOP} & (\text {deadlock}) \\ & | ev \{program\} \rightarrow {Proc} & (\text {operation prefixing})\\ & | ev \rightarrow {Proc} & (\text {event prefixing})\\ & | [\,guard]\, {Proc} & (\text {state guard}) \\ & | {Proc_{1}} \;\vert \vert \; {Proc_{2}} & (\text {parallel composition}) \\ & | {Proc_{1}} \;\vert \vert \vert \; {Proc_{2}} & (\text {interleaving}) \\ & | {Proc_{1}}; {Proc_{2}} & (\text {sequential} \; \text {composition})\\ & | ch ? a \rightarrow {Proc(a)} & (\text {channel input})\\ & | ch ! a \rightarrow {Proc} & (\text {channel output})\\ & | {Proc_{1}} \;\Box \; {Proc_{2}} & (\text {external} \; \text {choice})\\ & | {Proc_{1}} \;\sqcap \; {Proc_{2}} & (\text {internal} \; \text {choice})\\ & | \mathrm {if} \; guard \; \mathrm {then} \; {Proc_{1}}\; \mathrm {else}\; Proc_{2} & (\text {boolean} \; \text {statement})\\ & | {Proc_{1}} \;\triangleright \; {Proc_{2}} & (\text {timeout})\\ & | {Proc_{1}} \;\triangle \; {Proc_{2}} & (\text {interrupt}) \end{array}\end{align*} where Proc, $Proc_{1}$ and $Proc_{2}$ are processes, guard represents a condition, ev is an event, program describes a piece of code that executes atomically and ch denotes a synchronized communication channel.

Assertions are used to query properties about the behavior of a system. Various types of assertions are supported in PAT, such as, deadlock-freeness, divergence-free, nonterminating, reachability and LTL. Deadlock-freeness and LTL assertions are used in this work.

C. Deadlock-Freeness

This assertion checks whether a process Proc is deadlock-free or not.

#assert Proc() deadlockfree;

D. Linear Temporal Logic (LTL)

LTL is used to specify properties to be checked on a formal model. LTL extends predicate or propositional logic by modalities and provide a way to mathematically represent linear time properties. PAT supports the full syntax of LTL. For a process Proc(), the below assertion checks whether Proc() satisfies the LTL formula $\phi $ .

#assert Proc() $\models \phi $ ;

The syntax of LTL is defined according to following rules:\begin{equation*} \phi = ev\, |\, prop\, |\, \phi _{1} \, \land \, \phi _{2} |\, \neg \, \phi | \, \Box \, \phi |\, \lozenge \, \phi |\, \bigcirc \, \phi |\, \phi _{1}\, \cup \, \phi _{2}\end{equation*} where ev is an event, $prop$ is an atomic proposition, $\Box $ is read as always, $\lozenge $ is read as eventually, $\bigcirc $ is read as next, and $\cup $ is read as until. An LTL formula $\Box \phi $ defines that $\phi $ must hold on the entire respective path while $\lozenge \phi $ represents that $\phi $ eventually holds on the respective path. An LTL formula $\bigcirc \phi $ describes that $\phi $ must hold at next state whereas $\phi _{1} \cup \phi _{2}$ shows that $\phi _{2}$ holds at the current position or at some future position and $\phi _{1}$ has to hold before that state. From that position $\phi _{2}$ does not necessarily has to hold any more.

SECTION III. Related Work

In this section, firstly blockchain consensus protocols are described, then blockchain-based crowdsourcing consensus protocols are discussed and crowdsourcing systems based on blockchain are described in the end.

A. Blockchain Consensus Protocols

Some important blockchain consensus protocols are briefly described here. PoW is the first consensus algorithm that is used in Bitcoin [13]. It is based on complicated computation where every node of the network continuously computes a hash value of every block header using different nonce values until the calculated hash value becomes less than or equal to a certain target value. When a node gets the desired value, other nodes of the network verifies its correctness, and the block is added to the blockchain. However, it is highly resource-intensive and has low throughput.

PoS is an alternative to PoW that requires much less energy to be consumed [14]. In this mechanism, a node is selected based on its stake to propose a block. However, it favors rich nodes in the network. In this way, centralization can occur in the network. Several solutions are proposed to address this issue. For example, Peercoin [34] uses coin age selection procedure, Blackcoin [35] is based on randomization and Bitshares [36] uses Delegated Proof of Stake (DPoS) [15] in which stakeholders select delegates based on voting for the generation and validation of a block, however, it has some degree of centralization.

PBFT is proposed for tolerating byzantine faults [37]. It can tolerate 1/3 byzantine faults. The consensus is divided into three phases, i.e., pre-prepare, prepared, and commit. A node can transit from one phase to another phase after getting 2/3 votes from other nodes. Tendermint is another BFT consensus protocol [38]. However, the BFT protocols are suitable for small networks and have poor scalability. The survey of several other blockchain consensus protocols is provided in [39].

B. Blockchain-Based Crowdsourcing Consensus Protocols

Recently, the integration of blockchain technology and crow-dsourcing has gained the attention of the research community. PoT is a consensus protocol built upon the idea of blockchain technology to handle the accountability issue in crowdsourcing services [18]. The protocol utilizes RAFT [22] to elect a leader from ledger nodes and selects service participants as validators of transactions based on trust values. The PoT protocol addresses the issue of scalability associated with BFT and Paxos-based algorithms. It considers the unfaithful behavior of nodes that is not addressed in BFT algorithms. The security attacks, including, sybil, collusion, and DDoS are analyzed in the work. As RAFT is formally verified through TLA proof system and Coq proof assistant [22], [23], therefore, PoT is defined as partially verified in Table 1. However, PoT cannot preserve privacy of users. An improved PoT consensus algorithm is presented for crowdsourcing using blockchain as an underlying technology [19]. In this protocol, a high reputation worker is selected as a miner of the block. The calculation of reputation is based on the historical interaction of a miner and feedback of other nodes which may not be reliable. It analyzes the collusion attacks and does not provide a mechanism to evaluate task solutions. Further, privacy and reliability are also not addressed in this work.

TABLE 1 Summary of Blockchain-Based Crowdsourcing Consensus Protocols

MCS-Chain is presented as a blockchain-based mobile crowdsourcing platform for decentralized and distributed tr-ust management [20]. The trust evaluation mechanism is defined which allows users to select reliable workers. A consensus protocol is presented in MCS-Chain for block generation to improve the efficiency of the blockchain. In the protocol, a new block is created when the total payment which needs to be recorded into the next block exceeds the defined threshold. The centralization and fork issues are addressed in the work which guarantee that even if several blocks are generated simultaneously, a unique block is added to the blockchain. The liveness, safety, fault tolerance, and decentralization are demonstrated theoretically but the system lacks in privacy and anonymity of users and workers.

The zkCrowd, a hybrid blockchain-based crowdsourcing platform is proposed to balance transaction transparency and privacy [21]. The zkCrowd consists of a public chain to manage public tasks and multiple subchains to handle private tasks. DPoS is implemented on the public blockchain to elect validators. The alternative validators which are not elected in the public chain are elected as subchain validators in a round-robin manner using PBFT on private subchains. The zkCrowd is resilient against a 51% attack, sybil attack, privacy leakage, free riding and false reporting, and byzantine failures. As continuous-time Markov chain models are defined for PBFT and are formally verified through PRISM model checker [24], therefore, zkCrowd is termed as partially verified in Table 1. However, zkCrowd lacks in defining cross-communication between public and private chains, privacy protection of answers, and a proper reward distribution mechanism. On the public chain, voters having more tokens have more influence on the network. Further, if there are a large number of private tasks then an issue of scalability can occur. The comparison of the above-discussed consensus protocols is provided in Table 1. Unlike [18]–​[21], the proposed protocol is formally verified.

C. Blockchain-Based Crowdsourcing Systems

1) Trust Management

MCS-Chain+ is presented to address the issue of privacy in MCS-Chain [40]. The Intel Software Guard Extension (SGX) is utilized to anonymously authenticate trust through a trustworthy evaluation of trust. RC-chain is a reputation-based framework that is proposed as a crowdsourcing blockchain to support crowdsourcing trading and evaluation of user-reputation [41]. CrowdR-FBC is presented as a distribu-ted fog-blockchain mechanism for reputation management in crowdsourcing which prevents leakage of users’ privacy, involvement of malicious users, and tampering of users’ reputation [42]. It ensures the selection of trusted workers and the reliability of data. Blockchain technology is utilized to present a trusted and decentralized approach for a crowdsourcing system [43]. The proposed mechanism enables information of users and several behaviors to be transparent and cannot maintain the privacy of user’s information. A blockchain-based trust model using weighted consensus technique to share information in crowd environments is presented to achieve higher accuracy [44].

2) Task Management

CrowdBC is a blockchain-based decentralized framework for solving tasks of requesters by a crowd of workers without any trusted third party [32]. It protects the privacy of users as it utilizes pseudonymous addresses for the identities of requesters and workers, and stores encrypted solutions in distributed storage. However, defining an efficient evaluation function for tasks solution is crucial in CrowdBC. ZebraLancer is another platform that protects user privacy, but it depends on a trusted third party for registration of identities [47]. A novel hybrid blockchain-based crowdsourcing platform is proposed to ensure decentralization and privacy [45]. The platform consists of a hybrid structure of blockchain and dual consensus protocols to ensure secure communication among requesters and workers. Zero-knowl-edge proofs are used to protect the privacy of users whereas the access control model is not defined in detail. FedCrowd platform is proposed as a privacy-preserving and federated platform for blockchain-based crowdsourcing [48]. The sma-rt contracts are employed as a trusted platform to publish encrypted tasks and craft matching protocols are designed for task recommendation in an efficient way. But it depends on a trusted third party for the management of public and private keys. PFcrowd platform is presented to allow crowdsourcing systems to perform encrypted task-worker matching on the blockchain without any third party [49].

Blockchain-powered crowdsourcing model for the mobile environment is proposed to address several challenges such as, participants privacy, the integrity of services, and improving quality of experience [50]. A blockchain-based task matching (BPTM) model for crowdsourcing for reliable and secure matching is proposed using smart contracts [51]. Confidentiality and identity anonymity are achieved using searchable encryption. An auction-blockchain-based crowdsourcing technique, ABCrowd is presented to execute crowdsourcing on Ethereum blockchain including auctions [52]. It utilizes repeated bidders auction technique which allows truthful bidding. However, it lacks to protect user privacy. Task Select Worker Crowd (TSWCrowd) is presented to address the issues of reliable tasks allocation, ensuring workers’ payments and reliability of the platform [53]. The task-select-worker mechanism is defined to sort the tasks and the tasks having higher priority are assigned first. In contrast to ABCrowd, the average workers’ payment in TSW-Crowd is higher. ConGradetect is presented as a blockchain-based crowdsourcing detection system that addresses code and identity privacy but it analyzes simple codes [54].

Blockchain-based crowdsourcing is used for reliable data analysis in Mobile Ad-hoc Cloud (MAC) [55]. It addresses the challenges of attracting mobile devices to join the MAC network and able to collect reliable computation from mobile devices. A resilient-improved two-stage auction (ITA) is presented for fault tolerance in mobile crowdsourcing [56]. The proposed technique is beneficial for organizations as the workers are selected according to the time and budget of organizations. The designs for crowdsourced energy systems using blockchain technology are presented in [57], [58] to crowdsource small-scale production or trading of energy from distributed resources of energy. To handle the issues of crowdsourcing data access, analysis, and management, a framework based on blockchain technology is proposed [46]. The framework helps researchers in accessing operational data ensuring confidentiality, traceability, and accountability of data, and disseminating data in a controlled way to the public, but it lacks scalability.

3) Dispute Arbitration

A blockchain-based scheme for fine-grained authorization in data crowdsourcing (BC-FGA-DCrowd) is proposed in [59]. The scheme resists internal malicious actions and external sybil and DDoS attacks. The feasibility of the scheme is tested on the Ethereum network, however, it lacks in defining a proper function for evaluating the quality of data. A decentralized oracle-based game is proposed to decide the truth of queries and to resolve disputes [60]. In crowdsourcing, the quality of completed tasks and fairness in the evaluation of tasks are addressed using blockchain technology [61]. An arbitration mechanism is described for the realization of business services and to avoid security attacks, e.g., false reporting and free-riding but it lacks privacy analysis.

The comparison of the discussed research work in terms of security and trust is provided in Table 2. It is observed in the literature that there are very few blockchain-based crowdsourcing consensus protocols and some of these are partially verified [18], [21]. To the best of our knowledge, this is the first work which utilizes CSP# for the formal specification of a blockchain-based crowdsourcing consensus protocol and the PAT model checker for the verification of security and trust properties.

TABLE 2 Comparison of Blockchain-Based Crowdsourcing Systems

SECTION IV. System Model and Consensus Protocol

This section describes the architecture of the system, design of the consensus protocol, security properties, and associated attacks. In the end, a threat model with attacks and defenses is presented.

A. System Architecture

The architecture of the blockchain-based crowdsourcing system (BBCS) is represented in Figure 3. It consists of four actors: service consumer, service provider, blockchain management nodes, and validator nodes. The service consumers request for services by posting a task to the crowdsourcing platform. A service consumer can check the status of a task by sending a query to the blockchain. Service providers provide services by receiving a task through a crowdsourcing platform. A service provider can send a query to the blockchain to get information about the task payment. The blockchain management nodes are responsible for managing blockchain, e.g., proposing and validating blocks. In every round of consensus, a trusted leader is elected from the blockchain management nodes to propose and add a block to the blockchain. The validators validate and vote for transactions and blocks. The blockchain management nodes, service consumers, and providers can serve as validators.

FIGURE 3.

Architecture of the system.

B. Design of Consensus Protocol

1) Crowdsourcing Consensus Protocol

The overview of the proposed STBC consensus protocol is presented in Figure 4. The consensus process starts with the initialization of nodes that can perform the transactions. The blockchain management node having the highest trust value is selected as a leader for the current round. The trust is calculated based on deposit ratio, activity rate, and missed rate.The trusted validators are selected from blockchain management nodes, crowdsourcing service providers, and consumers to validate and vote for the transactions and the block to avoid malicious behaviors. The validator’s trust is calculated based on deposit ratio and activity rate. The process of selection of leader and validators runs in parallel to save time. After the process of selection, the trusted validators vote for transactions and broadcast votes. The leader prepares the block by including the transactions that gain the majority of the votes from validators. The leader then broadcasts the block to the validators and they vote for the block. If the majority of the validators accept the block then the leader adds the block in the blockchain and all the nodes update their ledger. The trust values and deposit of leader and validators are updated and the consensus process enters into the next round. If the block is rejected, then the leader and validators lose the trust and deposit, and the consensus protocol moves to the next round.

FIGURE 4.

Overview of STBC consensus protocol.

2) Calculation of Trust of a Leader

The trust factors of management nodes for the selection of a leader are defined as:

Deposit ratio of a management node: The deposit that a management node $i$ made is denoted as $md_{i}$ . The sum of deposits of all management nodes is defined as $MD = \sum md_{i}$ . The deposit ratio of a management node $i$ is calculated as $\alpha _{i} = \frac {md_{i}}{MD}\,\,\in $ [0, 1]. All the nodes should have the deposit greater than some specific amount for the block generation process.

Activity rate of a management node: Let $MB_{i}$ be the total number of times that a management node $i$ has been selected for block generation and $mb_{i}$ be the number of times that a management node $i$ has successfully generated the block. The activity rate of a management node is denoted as $\beta _{i} = \frac {mb_{i}}{MB_{i}}\,\,\in $ [0, 1]. Initially, it is assumed that $\beta _{i} =0$ .

Missed rate of a management node: Let $MS_{i}$ be the total number of times that a management node $i$ participates in leader selection and $ms_{i}$ be the number of times that a management node $i$ has not been selected as a leader. The missed rate of a management node is calculated as $\gamma _{i} = \frac {ms_{i}}{MS_{i}}\,\,\in $ [0, 1]. It is assumed that $\gamma _{i} =$ 0 initially.

A leader for block generation is selected from management nodes based on the above trust factors.

Trust of a leader: The trust of a leader $i$ can be calculated as: $\eta _{i} = \frac {\alpha _{i} + \beta _{i} + \gamma _{i}}{3}\,\,\in $ [0, 1]. The deposit ratio can affect the leader selection process. Therefore, to avoid the situation where a malicious attacker can dominate the network by submitting a tremendous amount of money, a maximum deposit that a node can submit is defined, which is agreed by all participants. In the first few rounds, the nodes having higher deposit and activity rate have a greater chance to be selected as a leader but in the long-term the nodes having a deposit and higher missed rate have an equal chance to be selected as the nodes having higher deposit and activity rate. Missed rate is introduced to provide fairness among nodes.

3) Calculation of Trust of Validators

The trust factors to define a criteria for the selection of validators are described below.

Deposit ratio of a validator node: The deposit that a validator node $j$ made is denoted as $vd_{j}$ . The sum of deposits of all validator nodes is defined as $VD = \sum vd_{j}$ . The deposit ratio of a validator node $j$ is calculated as $\Gamma _{j} = \frac {vd_{j}}{VD}\,\,\in $ [0, 1]. All the nodes should have a deposit greater than some specific amount for the block validation process.

Activity rate of a validator node: Let $VB_{j}$ be the total number of times that a validator node $j$ has been selected for block validation and $vb_{j}$ be the number of times that a validator node $j$ has successfully validated the block. The activity rate of a validator node is denoted as $\Lambda _{j} = \frac {vb_{j}}{VB_{j}}\,\,\in $ [0, 1]. Initially, it is assumed that $\Lambda _{j} =0$ .

Trust of a validator: The trust of a validator $j$ can be calculated as: $\sigma _{j} = \frac {\Gamma _{j} + \Lambda _{j}}{2}\,\,\in $ [0, 1]. The activity rate is introduced here to avoid rich nodes dominating the network.

4) Algorithm

The high-level pseudocode of STBC consensus protocol is described in Algorithm 1. It takes management $M$ , consumer $C$ , provider $P$ and validator $V$ nodes as input (line 1). Firstly, all these nodes are initialized (line 2). The consumer and provider nodes can perform transactions (line 3). These two steps are required for running the consensus protocol. Then the selection of a trusted leader $TLeader$ and $K$ trusted validators $TValidators$ runs in parallel (lines 4-5). After the selection process, the trusted validators vote for $T$ transactions for a block (lines 6-7). The leader proposes the block by including the leader information, previous block hash, and $T$ transactions that receive maximum votes (lines 8-9). The proposed block is then broadcast for a vote to validators (lines 10-11). If it is accepted by the majority of the validators then it is added in the blockchain and the leader and validators’ trust values and deposit are updated (lines 12-14). Otherwise, the proposed block is discarded and the selected leader and validators lose the trust and escrow deposit (lines 15-17). The number of activities $mb_{TLeader}$ , number of misses $ms_{TLeader}$ and deposit $md_{TLeader}$ of the leader are set to zero. The number of activities $vb_{TValidators}$ and deposit $vd_{TValidators}$ of trusted validators become zero. The whole process is repeated in the next round (line 18). In Algorithm 1, $\overline {Blockchain}$ represents the old state of blockchain and ^is the concatenation operator.

Algorithm 1: High level pseudocode of STBC consensus protocol

1

STBC(M, C, P, V)

2

Nodes_Initialization(M, C, P, V)

3

Perform_Transactions(C, P)

4

Selection() = Leader_Selection(M) $\parallel $

5

Validators_Selection(V, K)

6

VTransactions $\gets $ VoteBroadcast(Transactions, T, T,

7

Validators)

8

Propose(Block(index, TLeader, prevHash, hash,

9

Tmax(VTransactions)))

10

Broadcast(Block, TValidators)

11

Vote(Block, TValidators)

12

if (Accept(Block, Majority) == true)

13

Blockchain $\gets {Blockchain}$ ^Block

14

UpdateTrustAndDeposit()

15

else

16

Discard(Block)

17

LoseTrustAndDeposit()

18

Next_Round()

The high level pseudocode of $Nodes\_{}Initialization$ is presented in Algorithm 2. A management node $i$ is defined by its deposit $md_{i}$ , number of activities $mb_{i}$ , and number of misses $ms_{i}$ . Suppose a management node $i$ has a deposit that lies between the minimum and maximum deposit range. If the number of activities and misses are initially zero, then it can become part of the network (lines 2-5). It can serve as a validator, therefore, it is added in the validator nodes (line 6). Similarly, suppose a consumer node $c$ and a provider node $p$ have sufficient deposit and zero number of activities. In that case, they can be added to the network (lines 7-10, 12-15). A consumer and a provider can also serve as a validator, therefore, included in the validator nodes (lines 11, 16). Here, $s$ , $t$ , and $u$ represent a number of management, consumer, and provider nodes respectively that can be added to the network.

Algorithm 2: Pseudocode of nodes intialization

1

Nodes_Initialization(M, C, P, V)

2

for i $= 1, 2, \ldots, \text {s}$

3

if($md_{i} \geq $ minDeposit && $md_{i} \leq $ maxDeposit &&

4

$mb_{i} ==0$ && $ms_{i} ==0$ )

5

M = M $\cup $ {i}

6

V = V $\cup $ {i}

7

for c $= 1, 2, \ldots, \text {t}$

8

if($vd_{c} \geq $ minDeposit && $vd_{c} \leq $ maxDeposit

9

&& $vb_{c} ==0$ )

10

C = C $\cup $ {c}

11

V = V $\cup $ {c}

12

for $\text {p} = 1, 2, \ldots, \text {u}$

13

if($vd_{p} \geq $ minDeposit && $vd_{p} \leq $ maxDeposit

14

&& $vb_{p} ==0$ )

15

P = P $\cup $ {p}

16

V = V $\cup $ {p}

Algorithm 3 defines the types of transactions that can occur in a crowdsourcing system. A consumer $c$ can post a task and the deposit is stored in blockchain as an escrow amount (lines 2-4). A consumer deposit includes three shares, the first share is for task processing, the second share is the block reward and the third share is the verification fee. The number of activities of a consumer is updated (line 5). A provider $p$ can receive and perform a task (lines 6-8). The consumer then evaluates the task and if it is accepted then the provider gets the share of payment and the number of activities is incremented (lines 9-13). Otherwise, the consumer gets some proportion of the deposit (lines 14-17).

Algorithm 3: Pseudocode of performing transactions

1

Perform_Transactions(C, P)

2

$\exists c \in C$

3

PostTask(c)

4

Escrow(d_c)

5

c.UpdateNumActivities(1)

6

$\exists p \in P$

7

ReceiveTask(p)

8

PerformTask(p)

9

EvaluateTask(c)

10

if (AcceptTask(c) == true)

11

treward $\gets $ RemoveEscrow(d_c/total_shares)

12

TaskReward(p, treward)

13

p.UpdateNumActivities(1)

14

else

15

RejectTask(c)

16

pdeposit $\gets $ RemoveEscrow(d_c/total_shares)

17

DepositReturned(pdeposit)

Algorithm 4 describes the procedure of leader selection (line 1). Initially, the first management node $M_{0}$ is selected as a temporary trusted leader (line 2). The participation values $MS_{TLeader}$ and $MS_{x}$ of all the management nodes that take part in leader selection are incremented (lines 3, 6). From all the management nodes, a management node having the highest trust value $\eta $ is selected as a trusted leader (lines 4-5, 7-11). In case of a tie, an approach presented in [62] is utilized to avoid it. According to this, a management node having the smallest hash value of its identifier (or public key) and trust is selected (lines 12-18). The selection value of the trusted leader $MB_{TLeader}$ is incremented (line 19). The deposit of the selected leader is stored as an escrow amount to prevent malicious behavior (line 20).

Algorithm 4: Pseudocode of leader selection

1

Leader_Selection(M)

2

let TLeader $= M_{0}$

3

$MS_{TLeader} = \overline \,\,{MS_{TLeader}} +1$

4

x = 1

5

while (x < len $M$ )

6

$MS_{x} = \overline \,\,{MS_{x}} +1$

7

if ($\eta _{TLeader} > \eta _{M_{x}}$ )

8

$\text{x}++$

9

else if ($\eta _{TLeader} < \eta _{M_{x}}$ )

10

TLeader $= M_{x}$

11

$\text{x}++$

12

else if ($\eta _{TLeader} == \eta _{M_{x}}$ )

13

if (Hash(TLeader.GetMId(), $\eta _{TLeader}$ ) >

14

Hash($M_{x}$ .GetMId(), $\eta _{M_{x}}$ ))

15

TLeader $= M_{x}$

16

$\text{x}++$

17

else

18

$\text{x}++$

19

$MB_{TLeader} = \overline \,\,{MB_{TLeader}} +1$

20

Escrow($md_{TLeader}$ )

Algorithm 5 presents the process of selection of $K$ validators. The value for $K$ can be selected at the time of implementation. Initially, no trusted validators are selected (line 2). The validators are sorted in descending order according to the trust value $\sigma $ , and the first $K$ validators of highest trust values are selected (lines 3-12). It is ensured that a leader cannot serve as a trusted validator in the same round. The selection value $VB_{V_{a}}$ of every trusted validator is updated (line 13). The deposit $vd_{V_{a}}$ of each selected validator is stored in blockchain to prevent malicious behavior (line 14).

Algorithm 5: Pseudocode of validators selection

1

Validators_Selection(V, K)

2

len(TValidators) =0

3

$\text{a}\,\,=0$ , b = 1

4

while (a < len V −1 && $V_{a}$ != TLeader &&

5

len(TValidators) $\leq $ K)

6

while (b < len V && $V_{b}$ != TLeader)

7

if ($\sigma _{V_{a}} \geq \sigma _{V_{b}}$ )

8

$\text{b}++$

9

else

10

Swap($V_{a}$ , $V_{b}$ )

11

$\text{b}++$

12

TValidators $= \overline {TValidators}\,\,\cup \,\,V_{a}$

13

$VB_{V_{a}} = \overline \,\,{VB_{V_{a}}} +1$

14

Escrow($vd_{V_{a}}$ )

15

$\text{a}++$

The update trust process is described in Algorithm 6. When the leader’s block is accepted by the network, then its number of activities $mb_{TLeader}$ is incremented (line 2), it gets the block generation reward (lines 3-4) and gains its escrowed deposit (line 5). The number of misses $ms_{M \setminus TLeader}$ of management nodes other than the leader node is updated (line 6). The number of activities $vb_{TValidators}$ of trusted validators is incremented (line 7). The validators get the block validation reward (lines 8-9). The escrowed deposit of validators is returned (line 10).

Algorithm 6: Pseudocode of updating trust and deposit

1

UpdateTrustAndDeposit()

2

$mb_{TLeader} = \overline \,\,{mb_{TLeader}} +1$

3

greward $\gets $ RemoveEscrow(d_c/total_shares)

4

BlockGReward(greward)

5

DepositReturned(RemoveEscrow($md_{TLeader}$ ))

6

$ms_{M \setminus TLeader} = \overline \,\,{ms_{M \setminus TLeader}} +1$

7

$vb_{TValidators} = vb_{TValidators} +1$

8

vreward $\gets $ RemoveEscrow(d_c/total_shares)

9

BlockVReward(TValidators, vreward)

10

DepositReturned(RemoveEscrow($vd_{TValidators}$ ))

C. Properties and Attacks

In this work, we have defined security and trust properties, i.e., safety, fault tolerance, trusted leader, and trusted validators to prevent security attacks, such as blockchain fork, selfish mining, and invalid block insertion. The properties and attacks are defined below.

Definition 1 (Safety):

The consensus protocol is safe if all the nodes of network eventually reach the same decision.

Definition 2 (Fault Tolerance):

The consensus protocol is fault tolerant if all the honest nodes eventually accept the same block even in the presence of malicious nodes.

Definition 3 (Trusted Leader):

In every round of consensus protocol, a management node having the highest trust value is selected eventually.

Definition 4 (Trusted Validators):

In every round of consensus protocol, validator nodes that have the highest trust values are eventually selected.

Definition 5 (Blockchain Fork):

It represents a state of the blockchain in which nodes have different views about the blockchain state. The network nodes may receive more than one block at the same time.

Definition 6 (Selfish Mining):

Miners secretly mine blocks to earn rewards. The selfish miners release the blocks to the public when they get a longer chain.

Definition 7 (Invalid Block Insertion):

The blocks that disobey network rules are known as invalid blocks. A malicious leader tries to add invalid blocks in the blockchain.

D. Threat Model

To introduce an effective attack against the STBC consensus protocol, an attacker needs to compromise more than 1/3 of network nodes. A malicious leader and a validator can pose several threats which can affect the working of the consensus process. If there are multiple nodes mining at the same time then blockchain can fork, therefore, in the proposed consensus protocol, a unique leader is selected in every round to propose a block to prevent blockchain fork. Malicious nodes may try to mine blocks secretly and broadcast to the network nodes. To avoid this situation, it is ensured that only the trusted leader can execute the block propose and broadcast process and all the nodes add the block of a trusted leader in their ledger in each round. A malicious leader may try to add an invalid block in the blockchain, but the consensus protocol prevents its addition by adding no block. The deposit of a leader is stored in the blockchain to avoid malicious behavior. If a leader remains honest then the escrowed deposit is returned, otherwise, the deposit is slashed away. Moreover, it also loses its trust and it becomes very difficult for the malicious leader to become the leader again. This incentivises the leader to behave honestly.

Malicious validators may refuse to vote for transactions or blocks to prevent the addition of the correct blocks. This situation can occur only if more than 1/3 of the validators are malicious. To avoid this situation, the selected validators must also submit a deposit to the blockchain. If the correct block cannot be added to blockchain due to malicious validators then the validators not only lose the trust but also the escrowed deposit which incentivises validators to behave honestly. Further, it becomes difficult for these nodes to become trusted validators again. Further, if the consensus process is localized among some fixed nodes then it can lead to centralization. Therefore, the trust model for the selection of a leader and validators is designed in such a way that it prevents centralization. For the selection of a trusted leader and validators, activity rate is utilized in addition to deposit ratio to restrict rich nodes from dominating the network. Missed rate is also introduced in the selection of a leader so that the nodes waiting to become leaders also get a chance. This ensures fairness and decentralization in the protocol.

SECTION V. Formal Specification of Consensus Protocol

This section presents the formal model of the STBC consensus protocol using CSP#. In the formal model, the structure of blocks and the blockchain is defined at an abstract level and our main focus is to model the communication among nodes to achieve the consensus.

A. Consensus Protocol

The consensus protocol is defined as a process (line 3) which involves four nodes represented as $PNodes$ (line 1) where node $i \in PNodes$ . The number of transactions to be included in a block is defined as $T$ (line 2). All the steps of the consensus protocol are described in detail. In a distributed environment, all the nodes execute a sequence of processes of consensus protocol in parallel.

1. $\#define\,\,PNodes\,\,4$ ;

2. $\#define\,\,T\,\,2;$

3. $\begin{aligned} Consensus\_{}\,\,Protocol()=\\ \hspace {-1.5em}\qquad \quad (\parallel \,\,i:\{0..PNodes-1\}\text{@}\\ \hspace {-1.5em}\qquad \quad (NodeInitialization();\,\,PerformTransactions();\\ \hspace {-1.5em}\qquad \quad \,\,Selection();\,\,VoteForTransactions(T,\,\,i);\\ \hspace {-1.5em}\qquad \quad \,\,ProposeAndBroadcast(i);\,\,VoteToBlock(i);\\ \hspace {-1.5em}\qquad \quad \,\,isValidBlockchain();\,\,AddBlock(i);\\ \hspace {-1.5em}\qquad \quad \,\,UpdateTrustAndDeposit()));\\ \hspace {-1.5em}\qquad \quad NextRound(); \end{aligned}$

B. Nodes Initialization

Firstly, the nodes are initialized having unique identifiers, with sufficient deposit, number of activities, and number of misses (line 4). There are three types of nodes, i.e., management nodes, provider nodes, and consumer nodes. All these nodes can serve as validator nodes.

4. $\begin{aligned} NodeInitialization()=(MngNode1(0,\,\,20,\,\,0,\,\,0);\\ \quad \,\,\,\,MngNode2(1,\,\,30,\,\,0,\,\,0);\,\,ProvNode1(2,\,\,15,\,\,0);\\ \quad \,\,\,\,ProvNode2(3,\,\,20,\,\,0);\,\,ConsNode1(4,\,\,10,\,\,0);\\ \quad \,\,\,\,ConsNode2(5,\,\,30,\,\,0);\,\,ConsNode3(6,\,\,20,\,\,0)); \end{aligned}$

$MngNode1$ is defined as a management node (line 5). The first parameter represents the identifier of the node. The deposit, number of activities, and number of misses are described in the second, third, and fourth parameters respectively. Firstly, a guard statement is specified in which it is checked that the node has a positive identifier, has sufficient deposit, and that the number of activities and misses lies between the minimum and maximum range (line 5.1). If the guard evaluates to true then the new management node is added (line 5.2). As a management node can serve as a validator, therefore, it is also included in the validator nodes. The behavior of $MngNode2$ is similar to $MngNode1$ , therefore it is marked as “$\ldots $ ” for simplicity (line 6).

5. $MngNode1(id,\,\,deposit,\,\,numActivities,\,\,numMisses)=$

1. $\begin{aligned} [id\,\,>=\,\,0\,\,\&\&\,\,deposit\,\,>=\,\,minDeposit\,\,\&\&\\ \hspace {-1.5em}\qquad \qquad \,\,\,\,deposit\,\, < =\,\,maxDeposit\,\,\&\&\\ \hspace {-1.5em}\qquad \qquad \,\,\,\,numActivities\,\,>=\,\,minNumActivities\,\,\,\,\&\&\\ \hspace {-1.5em}\qquad \qquad \,\,\,\,numActivities\,\, < =\,\,maxNumActivities\,\,\&\&\\ \hspace {-1.5em}\qquad \qquad \,\,\,\,numMisses\,\,>=\,\,minNumMisses\,\,\&\&\\ \hspace {-1.5em}\qquad \qquad \,\,\,\,numMisses\,\, < =\,\,maxNumMisses] \end{aligned}$

2. $\begin{aligned} add1\,\,\{var\,\,m1=new\,\,ManagementNode(id,\,\,deposit,\,\,\\ \hspace {-1.5em}\qquad \qquad \quad \,\,\,\,numActivities,\,\,numMisses);\\ \hspace {-1.5em}\qquad \qquad \quad \,\,\,\,managementNodes.Add(m1);\\ \hspace {-1.5em}\qquad \qquad \,\,\,\,validatorNodes.AddNode(new\,\,ValidatorNode(id,\,\,\\ \hspace {-1.5em}\qquad \qquad \,\,\,\,deposit,\,\,numActivities,\,\,numMisses,\,\,m1)); \}\,\, \rightarrow \,\,Skip; \end{aligned}$

6. $MngNode2(id,\,\,deposit,\,\,numActivities,\,\,numMisses)\,\,\!=\! \ldots $

$ProvNode1$ is described as a provider node (line 7). It is defined by an identifier, deposit, and number of activities. Provider nodes can also participate in validation. $ProvNode2$ (line 8) is similar to $ProvNode1$ .

7. $ProvNode1(id,\,\,deposit,\,\,numActivities)=$

1. $\begin{aligned} [id\,\,>=\,\,0\,\,\&\&\,\,deposit\,\,>=\,\,minDeposit\,\,\&\&\,\,\\ \,\,deposit\,\, < =\,\,maxDeposit\,\,\&\&\,\,\\ \,\,numActivities\,\,>=\,\,minNumActivities\,\,\\ \,\,\&\&\,\,numActivities\,\, < =\,\,maxNumActivities] \end{aligned}$

2. $\begin{aligned} add3\,\,\{\,\,var\,\,v1=new\,\,ProviderNode(id,\,\,deposit,\,\,\\ \,\,numActivities);\,\,providerNodes.Add(v1);\\ \,\,validatorNodes.AddNode(new\,\,ValidatorNode(id, \\ \,\,deposit,\,\,numActivities,\,\,v1));\,\,\}\,\,\rightarrow \,\,Skip; \end{aligned}$

8. $ProvNode2(id,\,\,deposit,\,\,numActivities)\,\,= \ldots $

$ConsNode1$ , $ConsNode2$ and $ConsNode3$ are defined as consumer nodes similar to provider nodes (lines 9-11).

9. $ConsNode1(id,\,\,deposit,\,\,numActivities)\,\,= \ldots $

10. $ConsNode2(id,\,\,deposit,\,\,numActivities)\,\,= \ldots $

11. $ConsNode3(id,\,\,deposit,\,\,numActivities)\,\,= \ldots $

C. Perform Transactions

When the nodes become part of the system they perform transactions for the execution of tasks (line 12). The transactions of a post, receive, perform, evaluate, accept, reject, and finish a task are described.

12. $\begin{aligned} PerformTransactions()=\\ \hspace {-1.0em}\qquad PostTask(consumerNode,\,\,30);\,\,ReceiveTask(\\ \hspace {-0.85em}\qquad providerNode);\,\,PerformTask(\,\,providerNode);\\ \hspace {-1.0em}\qquad EvaluateTask(consumerNode);\,\,(AcceptTask(\\ \hspace {-0.85em}\qquad consumerNode)\,\,\square \,\,RejectTask(\,\,consumerNode));\\ \hspace {-1.0em}\qquad FinishTask(providerNode); \end{aligned}$

The post task transaction is specified as a process that takes a node $vl$ and $deposit$ as input (line 15). The input node should be a consumer node and initially, its state should be $not\_{}post$ . The deposit should exist between the minimum and maximum range (line 15.1). If the guard condition is satisfied then the state of the task changes to $post$ . The consumer escrows the deposit in the blockchain. The number of consumer activities is updated (lines 15.2).

13. $\begin{aligned} var\,\,state\!=\![not\_{}\,\,post,\,\,post,\,\,receive,\,\,perform,\,\,evaluate,\\ \hspace {-1.5em}\,\,taccept,\,\,treject,\,\,finish]; \end{aligned}$

14. $var\,\,task\_{}\,\,state=state[{0}];\,\,\,\,$

15. $PostTask(vl,\,\,deposit)=$

1. $\begin{aligned} [vl==consumerNode\,\,\&\&\,\,task\_{}\,\,state==state[{0}]\,\,\\ \qquad \&\&\,\,deposit\,\,>=\,\,minDeposit\,\,\&\&\\ \qquad deposit\,\, < =\,\,maxDeposit] \end{aligned}$

2. $\begin{aligned} post\_{}\,\,task\,\,\{task\_{}\,\,state=state[{1}];\,\,\,\,\\ \qquad escrowC=consumerNode.SubmitDeposit(deposit);\\ \qquad blockchain.SetEscrowAmount(escrowC);\\ \qquad consumerNode.UpdateNumActivities(1);\}\,\, \rightarrow \,\,Skip; \end{aligned}$

When the task is posted it is received by the provider and the state changes from $post$ to $receive$ . This is described by the process $ReceiveTask$ (line 16).

16. $\begin{aligned} ReceiveTask(vl)=[vl==providerNode\,\,\&\& \\ \hspace {-1.0em}\qquad task\_{}\,\,state==state[{1}]] \end{aligned}$

1. $receive\_{}\,\,task\,\,\{task\_{}\,\,state=state[{2}];\}\,\, \rightarrow \,\,Skip;$

When the provider receives the task then he performs the task and the state of the task changes to $perform$ (line 17).

17. $\begin{aligned} PerformTask(vl)=[vl==providerNode\,\,\&\& \\ \hspace {-1.0em}\qquad task\_{}\,\,state==state[{2}]] \end{aligned}$

1. $perform\_{}\,\,task\,\,\{task\_{}\,\,state=state[{3}];\}\,\, \rightarrow \,\,Skip;$

After the task is performed by the provider, then the consumer evaluates it (line 18).

18. $\begin{aligned} EvaluateTask(vl)=[vl==consumerNode\,\,\&\& \\ \hspace {-1.0em}\qquad task\_{}\,\,state==state[{3}]] \end{aligned}$

1. $evaluate\_{}\,\,task\,\,\{task\_{}\,\,state=state[{4}];\,\,\}\,\, \rightarrow \,\,Skip;$

The consumer can accept or reject the task (lines 19-20). If it is accepted then its state changes to $accept$ (line 19.1).

19. $\begin{aligned} AcceptTask(vl)=[vl==consumerNode\,\,\&\&\\ \hspace {-1.0em}\qquad task\_{}\,\,state==state[{4}]] \end{aligned}$

1. $accept\_{}\,\,task\,\,\{task\_{}\,\,state=state[{5}];\,\,\}\,\, \rightarrow \,\,Skip;$

If the task is rejected then its state changes to $reject$ and the consumer gets a proportion of the escrow amount (line 20).

20. $\begin{aligned} RejectTask(vl)=[vl==consumerNode\,\,\&\& \\ \hspace {-1.0em}\qquad task\_{}\,\,state==state[{4}]] \end{aligned}$

1. $\begin{aligned} reject\_{}\,\,task\,\,\{task\_{}\,\,state=state[{6}];\\ \hspace {-1.0em}\qquad blockchain.RemoveEscrowAmount(escrowC/\\ \hspace {-1.0em}\qquad numShares);\,\,consumerNode.AddDeposit(escrowC/\\ \hspace {-1.0em}\qquad numShares);\,\,\} \rightarrow \,\,Skip; \end{aligned}$

When the task is accepted by the provider then its state is changed to $finished$ (line 21.1). The provider gets the task payment and the number of activities are updated.

21. $\begin{aligned} FinishTask(vl)=[vl==providerNode\,\,\&\& \\ \hspace {-1.0em}\qquad task\_{}\,\,state==state[{5}]]\,\, \end{aligned}$

1. $\begin{aligned} task\_{}\,\,finish\,\,\{task\_{}\,\,state=state[{7}];\\ \hspace {-1.7em}\qquad blockchain.RemoveEscrowAmount(escrowC/numShares);\\ \hspace {-1.7em}\qquad providerNode.AddDeposit(escrowC/numShares);\\ \hspace {-1.7em}\qquad providerNode.UpdateNumActivities(1)\,\,\}\,\, \rightarrow \,\,Skip; \end{aligned}$

D. Selection

The consensus protocol starts with the selection of leader and validators (line 22). There should exist some management and validator nodes in the network to execute the selection, and their selection executes in parallel to save time.

22. $\begin{aligned} Selection()=\,\,[managementNodes.GetLength()\,\,>\,\,0\,\,\\ \hspace {-1.0em}\qquad \&\&\,\,validatorNodes.GetLength()\,\,>\,\,0]\,\,\,\,\\ \qquad (LeaderSelection()\,\,\parallel \,\,SelectValidator(K)); \end{aligned}$

1) Leader Selection

The leader selection algorithm is executed by each node in parallel in a distributed environment. It is assumed that all the nodes should have exactly the same inputs to achieve synchronous agreement [63]. It is ensured using a flooding algorithm in [63]. Otherwise, disagreement may occur. Given the same input, each node chooses exactly the same leader. In case of a tie among the nodes of the same trust values, an approach similar to the work presented in [62] is used in this work to avoid this situation. Following this approach, if any two management nodes have the same trust values then a management node with the smaller hash value of identifier and trust is selected.

The process of selection of a trusted leader is specified as $LeaderSelection$ (line 23). Firstly, a temporary leader is selected and its participation value is incremented (lines 23.1-23.4). The participation value of all other management nodes involved in leader selection is incremented. The deposit ratio, activity rate, and missed rate of all management nodes are compared, and the node having the highest trust value is selected as a leader (lines 23.5-23.7). In case, if the management nodes have the same trust values, then the above-described approach is used to select one leader for the current round (lines 23.8-23.11). The selection value of the leader is incremented (line 23.12). The selected leader submits the deposit in the blockchain (lines 23.13-23.16).

23. $LeaderSelection()=leaderSelection\{\,\,$

1. $var\,\,index=0;$

2. $mn1=managementNodes.GetNode(index);$

3. $tempLeader=mn1;$

4. $tempLeader.UpdateNumParticipated(1);$

5. $\begin{aligned} while(index\,\, < \,\,managementNodes.GetLength()-1)\,\,\{\,\,\\ \qquad \,\,\,\,mn2=managementNodes.GetNode(index+1);\\ \qquad \,\,mn2.UpdateNumParticipated(1);\\ \qquad \,\,var\,\,depositRatio1=tempLeader.GetDeposit()/\\ \qquad \qquad \quad managementNodes.GetTotalDeposit();\\ \qquad var\,\,activityRate1=tempLeader.GetNumActivities()\\ \qquad \qquad \,\,\,\,/\,\,tempLeader.GetNumSelected();\\ \qquad \,\,var\,\,missedRate1=tempLeader.GetNumMisses()/\\ \qquad \qquad \quad tempLeader.GetNumParticipated();\\ \qquad \,\,var\,\,depositRatio2=mn2.GetDeposit()/\\ \qquad \qquad \,\,managementNodes.GetTotalDeposit();\\ \qquad \,\,var\,\,activityRate2=mn2.GetNumActivities()/\\ \qquad \qquad \,\,mn2.GetNumSelected();\\ \quad \,\,\,\,var\,\,missedRate2=mn2.GetNumMisses()/\\ \qquad \qquad \,\,mn2.GetNumParticipated(); \end{aligned}$

6. $\begin{aligned} if\,\,(((depositRatio1\,\,+\,\,activityRate1\,\,+\,\,\\ \qquad \qquad \,\,missedRate1)/3)\,\,>\,\,((depositRatio2\,\,+\\ \qquad \qquad \,\,activityRate2\,\,+\,\,missedRate2)/3))\{\,\,\\ \qquad \qquad \,\,index=index+1; \}\,\, \end{aligned}$

7. $\begin{aligned} else\,\,if\,\,(((depositRatio1\,\,+\,\,activityRate1\,\,+\,\,\\ \qquad \qquad \,\,missedRate1)/3)\,\, < \,\,((depositRatio2\,\,+\\ \qquad \qquad \,\,activityRate2\,\,+\,\,missedRate2)/3))\{\,\,\\ \qquad \qquad \,\,tempLeader=mn2;\\ \qquad \qquad \,\,index=index+1;\}\,\,\}\,\, \end{aligned}$

8. $\begin{aligned} else\,\,if\,\,(((depositRatio1\,\,+\,\,activityRate1\,\,+\,\,\\ \qquad \qquad \,\,missedRate1)/3)==((depositRatio2\,\,+ \\ \qquad \qquad \,\,activityRate2\,\,+\,\,missedRate2)/3))\{\,\,\\ \qquad \,\,\,\,if\,\,((tempLeader.computeHash(tempLeader.\\ \qquad \qquad \,\,\,\,GetMId(),\,\,(depositRatio1\,\,+\,\,activityRate1\,\,+\,\,\\ \qquad \qquad \,\,\,\,missedRate1)/3))\,\,>\,\,(mn2.computeHash(mn2.\\ \qquad \qquad \,\,\,\,GetMId(),\,\,(depositRatio2\,\,+\,\,activityRate2\,\,+\,\,\\ \qquad \qquad \,\,\,\,missedRate2)/3)))\,\,\{\,\,\,\,tempLeader=mn2;\\ \qquad \qquad \qquad \quad \,\,index=index+1;\}\,\,\\ \qquad \,\,\,\,else\,\,\{\,\,index=index+1;\,\,\}\,\,\}\,\,\}\,\, \end{aligned}$

9. $selectedLeader=tempLeader;$

10. $leaderSelected=1;$

11. $selectedLeader.SetRound(rd);$

12. $selectedLeader.UpdateNumSelected(1); $

13. $escrowL=selectedLeader.\,\,$

14. $SubmitDeposit(selectedLeader.GetDeposit());$

15. $blockchain.SetEscrowAmount(escrowL);$

16. $selectedLeader.SetDeposit(0); \,\,\}\,\, \rightarrow \,\,Skip;$

2) Validators Selection

The trusted validators selection process is specified as $SelectValidator$ (line 24). The deposit ratio and activity rate of all validator nodes are compared and the first $k$ nodes having the highest trust values are selected as trusted validators (lines 24.1-24.6). The selection value of the trusted validator is incremented (lines 24.7-24.8). The selected trusted validators submit the deposit to the blockchain in an escrow account (lines 24.9-24.11). The record of selected trusted validators is maintained (lines 24.12-24.13).

24. $SelectValidator(k)=selectkval\{\,\,$

1. $var\,\,index1=0;$

2. $var\,\,index2=1;$

3. $\begin{aligned} while(index1\,\, < \,\,validatorNodes.GetLength()-1\,\,\&\&\\ \qquad index1\,\, < \,\,k)\,\,\{\,\, \end{aligned}$

4. $\begin{aligned} while(index2\,\, < \,\,validatorNodes.GetLength())\,\,\{\,\,\\ \qquad \quad \,\,\,\,vn1=validatorNodes.GetNode(index1);\\ \qquad \quad \,\,\,\,vn2=validatorNodes.GetNode(index2);\\ \qquad \quad \,\,\,\,var\,\,depositRatio1=vn1.GetDeposit()/\\ \qquad \qquad validatorNodes.GetTotalDeposit();\\ \qquad \quad \,\,\,\,var\,\,activityRate1=vn1.GetNumActivities()/\\ \qquad \qquad vn1.GetNumSelected();\\ \qquad \quad \,\,\,\,var\,\,depositRatio2=vn2.GetDeposit()/\\ \qquad \qquad \,\,\,\,validatorNodes.GetTotalDeposit();\\ \qquad \quad \,\,\,\,var\,\,activityRate2=vn2.GetNumActivities()/\\ \qquad \qquad \,\,\,\,vn2.GetNumSelected(); \end{aligned}$

5. $\begin{aligned} if\,\,(((depositRatio1\,\,+\,\,activityRate1)/2)\,\,>=\,\,\,\,\\ \qquad \qquad \quad ((depositRatio2\,\,+\,\,activityRate2)/2))\{\,\,\\ \qquad \qquad \quad \,\,\,\,validatorNodes.SetNode(index1,\,\,vn1);\,\,\,\,\\ \qquad \qquad \quad \,\,\,\,validatorNodes.SetNode(index2,\,\,vn2);\,\,\,\,\\ \qquad \qquad \quad \,\,\,\,index2++;\}\,\, \end{aligned}$

6. $\begin{aligned} else\,\,\{\,\,validatorNodes.SetNode(index1,\,\,vn2);\,\,\,\,\\ \qquad \qquad \quad \,\,\,\,validatorNodes.SetNode(index2,\,\,vn1);\,\,\,\,\\ \qquad \qquad \quad \,\,\,\,index2++;\}\,\,\,\,\}\,\, \end{aligned}$

7. $var\,\,tn=validatorNodes.GetNode(index1);$

8. $tn.UpdateNumSelected(1);$

9. $escrowV=tn.SubmitDeposit(tn.GetDeposit());$

10. $blockchain.SetEscrowAmount(escrowV);$

11. $tn.SetDeposit(0);$

12. $trustedValidatorNodes.AddNode(tn);$

13. $index1++;\,\,\}\,\,valSelected=1;\,\,\}\,\, \rightarrow \,\,Skip;$

E. Vote and Broadcast Transactions

After the process of selection, the leader has to prepare the block and for this purpose, the transactions that receive maximum votes from validators are required. The procedure Vote ForTransactions is specified at line 25. This process takes a number of transactions, and a validator as input. The number of transactions to vote for should be greater than zero and less than or equal to the maximum number of transactions (line 25.1). Otherwise, no transaction is available to vote for (line 25.2). Before the voting process, a leader and validators must be selected, otherwise, no transaction can be selected for the voting process (line 25.1).

25. $VoteForTransactions(t,\,\,vl)=$

1. $\begin{aligned} [t\,\,>\,\,0\,\,\&\&\,\,t\,\, < =\,\,maxTransactions]\,\,\\ \qquad \quad ([leaderSelected == 1\,\,\&\&\,\,valSelected == 1]\\ \qquad \quad selection\_{}\,\,end\,\, \rightarrow \,\,voteTrans(t,\,\,vl)\,\, \square \\ \qquad \quad [leaderSelected == 0\,\,\parallel \,\,valSelected == 0]\\ \qquad \quad \,\,\,\,no\_{}\,\,transaction\_{}\,\,selected\,\, \rightarrow \,\,Skip)\,\, \square \end{aligned}$

2. $[t\,\, < \,\,0]\,\,no\_{}\,\,transaction\_{}\,\,to\_{}\,\,vote\,\, \rightarrow \,\,Skip;$

The voting process is described in procedure $voteTrans$ (line 26). It is a sequence of three processes. In the first process, every trusted validator selects $t$ transactions from pending transactions to vote for and the transactions proposal of every trusted validator is prepared (lines 26.2-26.3). In the second process, $VoteToTransaction\_{}a$ , the transactions proposals are validated and each trusted validator vote for it (lines 27-30). The third process describes the broadcasting and receiving of votes among validator nodes for transaction proposals (lines 26.4-26.7). A node will not broadcast or accept a block if the vote flag is zero. In this process, different communications channels are used, hence, the definition differs slightly for every node but the logical behavior remains the same.

26. $voteTrans(t,\,\,vl)=vote.t\,\,\{\,\,$

1. $var\,\,index1=0;$

2. $\begin{aligned} while(index1\,\, < \,\,trustedValidatorNodes.\\ \qquad GetLength()-1)\,\,\{\,\,\\ \qquad \quad tvn=trustedValidatorNodes.GetNode(index1);\\ \qquad \quad index1++;\,\,var\,\,index2=0; \end{aligned}$

3. $\begin{aligned} while(index2\,\, < \,\,pendingTransactions.GetLength()\\ \qquad \quad -1\,\,\&\&\,\,index2\,\, < \,\,t\,\,\&\&\,\,vl==tvn.GetVId())\,\,\{\,\,\\ \qquad \quad tran1=pendingTransactions.Get(index2);\\ \qquad \quad tTransactions.Set(index2,\,\,tran1);\,\,index2++;\}\,\,\\ \qquad \,\,\,\,transactionsProposals.Set(index1,\\ \qquad \quad new\,\,TransactionProposal(tTransactions,\\ \qquad \quad new\,\,TransactionSignature(index2)));\,\,\,\,\}\,\,\}\,\, \rightarrow \end{aligned}$

4. $\begin{aligned} ([vl==0]\,\,VoteToTransaction\_{}\,\,0();\,\,(\,\,\\ \qquad \quad ([voteflag0==1]\,\,(ch01!tempTVote0\,\, \rightarrow \,\,Skip\,\,\parallel \\ \qquad \qquad ch02!tempTVote0 \rightarrow \,\,Skip\parallel \,\,ch03!tempTVote0 \rightarrow \\ \qquad \qquad \,\,Skip)\,\, \square \,\,[voteflag0==0]\,\,Skip)\,\,\parallel \,\,\,\,\\ \qquad \quad ([voteflag1==1]\,\,ch10?y\,\,\{\,\,tvotes0.Add(y)\,\,\}\,\, \rightarrow \,\,\\ \qquad \quad \,\,\,\,Skip\,\, \square [voteflag1==0]\,\,Skip)\,\,\parallel \,\,\,\,\\ \qquad \quad ([voteflag2==1]\,\,ch20?y\,\,\{\,\,tvotes0.Add(y)\,\,\}\,\, \rightarrow \,\,\\ \qquad \quad \,\,\,\,Skip\,\, \square \,\,[voteflag2==0]\,\,Skip)\,\,\parallel \,\,\,\,\\ \qquad \quad ([voteflag3==1]\,\,ch30?y\,\,\{\,\,tvotes0.Add(y)\,\,\}\,\, \rightarrow \,\,\\ \qquad \quad \,\,\,\,Skip\,\, \square [voteflag3==0]\,\,Skip))\,\, \square \,\, \end{aligned}$

5. $[vl==1]\,\,VoteToTransaction\_{}\,\,1(); \ldots $

6. $[vl==2]\,\,VoteToTransaction\_{}\,\,2(); \ldots $

7. $[vl==3]\,\,VoteToTransaction\_{}\,\,3(); \ldots $

In every procedure of $VoteToTransaction\_{}a$ (lines 27-30), the transaction proposal is validated and voted accordingly. If the voting behavior of a node is honest then it votes for the transactions honestly, otherwise, the node having malicious intent does not vote for the transactions. It is mentioned that all transactions have similar behavior.

27. $\begin{aligned} VoteToTransaction\_{}\,\,0()=\,\,\\ \hspace {-0.5em}\qquad \,\,validateTProposal.0\,\,\{\,\,\\ \hspace {-0.5em}\qquad \,\,tempTProposal0=transactionsProposals.Get(0);\,\,\,\,\\ \hspace {-0.5em}\qquad \,\,tempProposedTransaction0\,\,=\,\,tempTProposal0.\\ \qquad GetTransactions();\\ \hspace {-0.5em}\qquad \,\,if(voteBehaviour[{0}]==Honest\_{}\,\,Vote)\,\,\{\\ \qquad \,\,\,\,tempTVote0=new\,\,TransactionVote(\\ \qquad \quad \,\,tempProposedTransaction0,\,\,tsignature0);\quad \,\,\,\,\\ \qquad \,\,\,\,tempTVote0.updateVotes(1);\} \\ \hspace {-0.5em}\qquad \,\,else\,\,if(voteBehaviour[{0}]==No\_{}\,\,Vote)\,\,\{\\ voteflag 0=0\} \,\,tvotes0.Add(tempTVote0);\} \rightarrow \,\,Skip; \end{aligned}$

28. $VoteToTransaction\_{}\,\,1()\,\,= \ldots $

29. $VoteToTransaction\_{}\,\,2()\,\,= \ldots $

30. $VoteToTransaction\_{}\,\,3()\,\,= \ldots $

In order to get the transactions with maximum votes, the process $TransWithMaxVotes$ is specified (line 31). It requires $t$ number of transactions as input. All the transactions that gain votes are checked and the first $t$ transactions that receive maximum votes are recorded.

31. $TransWithMaxVotes(t)=trans\,\,\{\quad \,\,\,\,$

1. $\begin{aligned} while(index1\,\, < \,\,votedTransactions.GetLength()-1\,\,\\ \qquad \&\&\,\,index1\,\, < \,\,t)\,\,\{\,\, \end{aligned}$

2. $\begin{aligned} while(index2\,\, < \,\,votedTransactions.GetLength())\,\,\{\,\,\\ \qquad \qquad \,\,\,\,tran1=votedTransactions.Get(index1);\\ \qquad \qquad \,\,\,\,tran2=votedTransactions.Get(index2); \end{aligned}$

3. $\begin{aligned} \qquad \,\,\,\,if\,\,(tran1.getVotes()\,\,>=\,\,tran2.getVotes())\{\,\,\\ \qquad \qquad \qquad \quad \,\,votedTransactions.Set(index1,\,\,tran1);\\ \qquad \qquad \qquad \quad \,\,votedTransactions.Set(index2,\,\,tran2);\\ \qquad \qquad \qquad \quad \,\,index2++;\}\,\, \end{aligned}$

4. $\begin{aligned} \qquad \,\,\,\,else\,\,\{\,\,votedTransactions.Set(index1,\,\,tran2);\\ \qquad \qquad \qquad \quad \,\,votedTransactions.Set(index2,\,\,tran1);\\ \qquad \qquad \qquad \quad \,\,index2++;\,\,\}\,\, \end{aligned}$

5. $ \qquad \,\,\,\,maxVotedTransactions.Set(index1,\,\,tran1);$

6. $ \qquad \,\,\,\,index1++; \quad \} \,\,\,\,\} \,\,\}\,\, \rightarrow \,\,Skip;$

F. Propose and Broadcast Block

After getting transactions that gain maximum votes, the block can be proposed. The block propose and broadcast procedure is described in line 32. If the leader is selected for the round, the block $b$ can be proposed (line 32.1). Firstly, an empty block is acquired from the locked blocks as the proposed block. The peek block of the blockchain is made the previous block of the current block to be proposed. The block is then proposed having information about the block index, leader of the block, previous block hash, and maximum voted transactions and is added in blocks proposals. If a node is the leader of the current round then it broadcasts the block to validators, otherwise, it receives the proposed block (lines 32.2-32.6). The same procedure is repeated for other blocks.

32. $ProposeAndBroadcast(b)=\,\,$

1. $\begin{aligned} [selectedLeader.GetRound()==b]\,\,proposeBlock.b\,\,\\ \quad \,\,\,\,\{\,\,proposedBlock=lockedBlocks.Get(b);\\ \qquad if\,\,(proposedBlock.GetBlockHash()==initialHash)\\ \qquad \quad \,\,\,\,\{\,\,prevBlock=blockchain.GetPeekBlock();\\ \qquad \qquad \,\,\,\,proposedBlock=new\,\,Block(b,\,\,selectedLeader,\\ \qquad \qquad \,\,\,\,prevBlock.GetBlockHash(),\\ \qquad \qquad \,\,\,\,maxVotedTransactions); \,\,\}\,\,\\ \qquad blocksProposals.SetProposal(b,\,\,new\,\,BlockProposal\\ \qquad \quad (proposedBlock,\,\,new\,\,BlockSignature(b)))\,\,\}\,\, \rightarrow \,\,\,\, \end{aligned}$

2. $\begin{aligned} ((\,\,[b==0]\,\,(ch01!blocksProposals.GetProposal(b)\,\,\\ \qquad \,\, \rightarrow Skip\,\,\parallel \,\,ch02!blocksProposals.GetProposal(b)\,\,\\ \qquad \,\, \rightarrow \,\,Skip\,\,\parallel \,\,ch03!blocksProposals.GetProposal(b)\,\,\\ \quad \,\, \rightarrow \,\,Skip)\,\, \square [b==1] \ldots [b==2] \ldots [b==3] \ldots \end{aligned}$

6. $\begin{aligned} [b==0]\,\,(ch10?y\,\, \rightarrow \,\,\{blocksProposals.\\ \qquad \quad SetProposal(b,\,\,y)\}\,\, \rightarrow \,\,Skip\,\, \square \,\,ch20?y\,\, \rightarrow \\ \qquad \quad \,\,\{blocksProposals.SetProposal(b,\,\,y)\}\,\, \rightarrow \,\,Skip\,\, \square \\ \qquad \quad \,\,ch30?y\,\, \rightarrow \,\,\{blocksProposals.SetProposal(b,\,\,y)\}\,\,\\ \quad \rightarrow \,\,Skip\,\,) \square [b==1] \ldots [b==2] \ldots [b==3] \ldots \end{aligned}$

After receiving the block, the validators vote for the block. The block voting process $VoteToBlock$ is specified at line 33. It takes the block index $b$ as input. It is a sequence of two processes and it is preceded by an event $propose\_{}end$ to ensure that the propose phase has ended (line 33.1). The first process $VoteToBlock\_{} a()$ validates the block proposal and accordingly votes for the block (lines 34-37). In the second process, the votes are broadcast and received among the validator nodes (line 33.1). If the vote flag is zero, a node will not broadcast or accept the vote for the block. The same process is followed for all the blocks (lines 33.2-33.4).

33. $VoteToBlock(b)=\,\,$

1. $\begin{aligned} [b==0]\,\,propose\_{}\,\,end\,\, \rightarrow \,\,VoteToBlock\_{}\,\,0();\,\,(\,\,\\ \qquad \quad ([voteflag0==1]\,\,(ch01!tempBVote0\,\, \rightarrow \,\,Skip\,\,\parallel \\ \qquad \quad ch02!tempBVote0 \rightarrow \,\,Skip\,\,\parallel \,\,ch03!tempBVote0\,\,\\ \qquad \quad \rightarrow \,\,Skip)\,\, \square \,\,[voteflag0==0]\,\,Skip)\,\,\parallel \,\,\,\,\\ \qquad \quad ([voteflag1==1]\,\,ch10?y\,\,\{\,\,bvotes0.Add(y)\,\,\}\,\, \rightarrow \\ \qquad \quad Skip\,\, \square \,\,[voteflag1==0]\,\,Skip)\parallel \,\,\,\,\\ \qquad \quad ([voteflag2==1]\,\,ch20?y\,\,\{\,\,bvotes0.Add(y)\,\,\}\,\, \rightarrow \,\,\\ \qquad \quad Skip\,\, \square \,\,[voteflag2==0]\,\,Skip)\parallel \,\,\,\,\\ \qquad \quad ([voteflag3==1]\,\,ch30?y\,\,\{\,\,bvotes0.Add(y)\,\,\}\,\, \rightarrow \,\,\\ \qquad \quad Skip\,\, \square \,\,[voteflag3==0]\,\,Skip))\,\, \square \,\, \end{aligned}$

2. $[b==1]\,\,propose\_{}\,\,end\,\, \rightarrow \,\,VoteToBlock\_{}\,\,1();\ldots $

3. $[b==2]\,\,propose\_{}\,\,end\,\, \rightarrow \,\,VoteToBlock\_{}\,\,2();\ldots $

4. $[b==3]\,\,propose\_{}\,\,end\,\, \rightarrow \,\,VoteToBlock\_{}\,\,3();\ldots $

In every process of $VoteToBlock\_{}a$ (lines 34-37), the malicious behavior is introduced. Firstly, the block proposal is validated and then voted on accordingly. If a node is honest then it votes for the block honestly, otherwise, does not vote.

34. $VoteToBlock\_{}\,\,0()=\,\,$

1. $\begin{aligned} validateProposal.0\,\,\{\,\,\\ \qquad tempProposal0=blocksProposals.GetProposal(0);\,\,\,\,\\ \qquad tempProposedBlock0=tempProposal0.GetBlock();\quad \,\,\,\,\\ \qquad var\,\,invalidBlock=blockchain0.\,\,\\ \qquad \quad ContainsBlock(tempProposedBlock0); \end{aligned}$

2. $if(invalidBlock)\,\,\{tempProposedBlock0=new\,\,Block();\}\,\,$

3. $\begin{aligned} if(voteBehaviour[{0}]==Honest\_{}\,\,Vote)\,\,\{\\ \qquad \quad \,\,tempBVote0=new\,\,BlockVote(tempProposedBlock0.\\ \qquad \quad \,\,GetBlockHash(), bsignature0); \\ \qquad \quad \,\,tempBVote0.updateVotes(1);\,\,\}\quad \,\,\,\, \end{aligned}$

4. $\begin{aligned} else\,\,if(voteBehaviour[{0}]==No\_{}\,\,Vote)\,\,\\ \qquad \quad \,\,\{voteflag0=0\}\,\,bvotes0.Add(tempBVote0);\}\,\,\\ \qquad \quad \,\, \rightarrow \,\,Skip; \end{aligned}$

35. $VoteToBlock\_{}\,\,1()\,\,= \ldots \,\,$

36. $VoteToBlock\_{}\,\,2()=\ldots $

37. $VoteToBlock\_{}\,\,3()=\ldots $

G. Blockchain Validity

After receiving enough votes, the block can be added to the blockchain. Before adding the block, the validity of the blockchain is checked, specified as $isValidBlockchain$ (line 38). The validity of the blockchain is checked by comparing the recorded and computed hash for every current and previous block (lines 38.1-38.5).

38. $isValidBlockchain()=validBlockchain\{\,\,$

1. $var\,\,index=blockchain.GetHeight();$

2. $\begin{aligned} while\,\,(index\,\, < =\,\,blockchain.GetHeight()\,\,\&\&\\ \qquad index\,\,>=\,\,2)\{\,\,\\ \qquad \,\,\,\,curBlock=blockchain.GetBlock(index);\\ \qquad \,\,\,\,prevBlock=blockchain.GetBlock(index-1); \end{aligned}$

3. $\begin{aligned} if\,\,(curBlock.GetBlockHash()\,\,!=\,\,\\ \qquad \qquad \,\,curBlock.computeHash())\{\,\,v=\,\,Not\_{}\,\,Valid;\}\,\, \end{aligned}$

4. $\begin{aligned} if\,\,(curBlock.GetPrevHash()\,\,!=\\ \qquad \qquad \,\,prevBlock.GetBlockHash())\{\,\,v=\,\,Not\_{}\,\,Valid;\}\,\, \end{aligned}$

5. $\begin{aligned} else\,\,if\,\,(curBlock.GetBlockHash()\,\,==\\ \qquad \qquad curBlock.computeHash()\,\,\&\&\\ \qquad \quad \,\,\,\,curBlock.GetPrevHash()\,\,==\\ \qquad \quad \,\,\,\,prevBlock.GetBlockHash())\{\quad \\ \qquad \quad \,\,\,\,v=valid;\,\,index--;\,\,\} \,\,\} \,\,\}\,\, \rightarrow \,\,Skip; \end{aligned}$

H. Adding Block in Blockchain

The process of block addition is specified as $AddBlock$ (line 39). For every block, firstly it is ensured that the blockchain is valid (line 39.1). If the block receives votes from a majority of the validators then it is added to the blockchain. Same process is repeated for every block (lines 39.2-39.4).

39. $AddBlock(b)=\,\,$

1. $\begin{aligned} [b==0\,\,\&\&\,\,v==valid]\,\,addtoBChain.b\,\,\{\,\,\\ \qquad \,\,\,\,tempProposedBlock0=bvotes0.\\ \qquad \quad \,\,GetBlockWithMajorityVotes(MajorityValidators);\\ \qquad \,\,\,\,if(tempProposedBlock0.GetBlockHash()\,\,!=\\ \qquad \qquad \,\,\,\,initialHash\,\,\&\&\,\,untrustedLeader==false)\,\,\{\,\,\\ \qquad \qquad \,\,\,\,blockchain0.AddBlock(tempProposedBlock0)\,\,\}\,\,\\ \qquad \,\,\,\,\}\,\, \rightarrow \,\,Skip\,\, \square \,\, \end{aligned}$

2. $[b==1\,\,\&\&\,\,v==valid] \ldots $

3. $[b==2\,\,\&\&\,\,v==valid]\,\,\ldots $

4. $[b==3\,\,\&\&\,\,v==valid]\,\,\ldots $

I. Update Trust Values and Deposit

At the end of the consensus protocol, trust values are updated (line 40). If the block is successfully added to blockchain then the leader’s number of activities is incremented, the leader gets the block generation reward and the escrow amount is returned (lines 40.1-40.2, 41-43). Similarly, the number of misses of participating management nodes are updated, the validators number of activities are incremented, they receive the block validation reward and their escrow deposit is returned (lines 40.2, 44-47). If the proposed block is not successfully added to the blockchain then the leader and validators lose trust (lines 40.3, 48-49). The leader deposit, the number of activities, and misses are set to zero. Similarly, the validators’ deposit and number of activities are set to zero.

40. $UpdateTrust()=$

1. $\begin{aligned} [blockchain0.ContainsBlock(tempProposedBlock0)\,\,\parallel \\ \qquad \quad blockchain1.ContainsBlock(tempProposedBlock1)\,\,\\ \quad \,\,\quad \parallel blockchain2.ContainsBlock(tempProposedBlock2)\,\,\\ \quad \,\,\quad \parallel blockchain3.ContainsBlock(tempProposedBlock3)]\,\, \end{aligned}$

2. $\begin{aligned} (UpdateLNumActivities(1);\\ \quad \,\,\quad GetBlockGReward(escrowC/numShares);\\ \quad \,\,\quad LDepositReturned(escrowL);\\ \quad \,\,\quad UpdatePMNumMisses(1);UpdateVNumActivities(1);\\ \quad \,\,\quad GetBlockVReward();TVDepositReturned();\,\,Skip) \square \,\, \end{aligned}$

3. $\begin{aligned} [!(blockchain0.ContainsBlock(tempProposedBlock0))\\ \hspace {-0.2em}\quad \,\,\quad \parallel !(blockchain1.ContainsBlock(tempProposedBlock1))\\ \hspace {-0.2em}\quad \,\,\quad \parallel !(blockchain2.ContainsBlock(tempProposedBlock2))\\ \hspace {-0.2em}\quad \,\,\quad \parallel !(blockchain3.ContainsBlock(tempProposedBlock3))\\ \quad \,\,\quad]\,\,maliciousLeader\,\, \rightarrow \,\,LLoseTrustAndDeposit()\,\, \square \\ \qquad \quad maliciousValidators\,\, \rightarrow \,\,VLoseTrustAndDeposit(); \end{aligned}$

The $UpdateLNumActivities$ process increases the number of activities of the leader by input $l$ (line 41).

41. $\begin{aligned} UpdateLNumActivities(l)=update\,\,\{selectedLeader.\\ \,\,\,\,\quad UpdateNumActivities(l)\}\,\, \rightarrow \,\,Skip; \end{aligned}$

In $GetBlockGReward$ , the block reward is removed from the blockchain and added in the account of leader (line 42).

42. $\begin{aligned} GetBlockGReward(deposit)=getdep\,\,\{blockchain.\\ \qquad RemoveEscrowAmount(deposit);\\ \qquad selectedLeader.AddDeposit(deposit)\}\,\, \rightarrow \,\,Skip; \end{aligned}$

The $LDepositReturned$ process specifies that the leader’s escrowed deposit is added in its account (line 43).

43. $\begin{aligned} LDepositReturned(deposit)=getdep\,\,\{blockchain.\\ \qquad RemoveEscrowAmount(deposit);\\ \,\,\qquad selectedLeader.AddDeposit(deposit)\}\,\, \rightarrow \,\,Skip; \end{aligned}$

In $UpdatePMNumMisses$ process, it is specified that if a management node is not a leader then its number of misses are updated (line 44).

44. $\begin{aligned} UpdatePMNumMisses(m)=update\,\,\{\,\,\\ \,\,\,\,while(index\,\, < \,\,managementNodes.GetLength()-1)\{\,\,\\ \quad \,\,\quad mn1=managementNodes.GetNode(index);\\ \quad \,\,\quad if\,\,(mn1\,\,!=\,\,selectedLeader\,\,\&\&\,\,\\ \qquad \quad \,\,\quad mn1.GetNumMisses()\,\, < \,\,maxNumMisses)\{\,\,\\ \qquad \quad \,\,\quad mn1.UpdateNumMisses(m);\}\,\,\\ \qquad \quad \,\,\quad index++;\,\,\}\,\,\,\,\}\,\, \rightarrow \,\,Skip; \end{aligned}$

The $UpdateVNumActivities$ process describes that the number of activities of all the trusted validators are incremented (line 45).

45. $\begin{aligned} UpdateVNumActivities(a)=update\,\,\{\,\,\\ \hspace {-0.7em}\,\,\,\,while(index < trustedValidatorNodes.GetLength()-1)\,\,\\ \qquad \{\,\,tvn=trustedValidatorNodes.GetNode(index);\\ \qquad tvn.UpdateNumActivities(a);\\ \qquad index++;\,\,\}\,\,\,\,\}\,\, \rightarrow \,\,Skip; \end{aligned}$

In $GetBlockVReward$ , it is described that the validators get the block validation reward from the deposit submitted by the consumer (line 46).

46. $\begin{aligned} GetBlockVReward()=vreward\,\,\{\,\,\\ \hspace {-0.7em} \,\,\,\,while(index < trustedValidatorNodes.GetLength()-1)\,\,\\ \qquad \quad \{\,\,tvn=trustedValidatorNodes.GetNode(index);\\ \qquad \quad blockchain.RemoveEscrowAmount((escrowC/\\ \qquad \quad numShares)/trustedValidatorNodes.GetLength());\,\,\,\,\\ \qquad \quad tvn.AddDeposit((escrowC/numShares)/\\ \qquad \quad trustedValidatorNodes.GetLength());\\ \qquad \quad index++;\,\,\} \,\,\}\,\, \rightarrow \,\,Skip; \end{aligned}$

The $TVDepositReturned$ process defines that the escrowed deposit of the validators is returned (line 47).

47. $\begin{aligned} TVDepositReturned()=tvdep\,\,\{\,\,\\ \quad \,\,while(index\,\, < \,\,trustedValidatorNodes.\\ \qquad \quad GetLength()-1)\,\,\{\,\,\\ \qquad \quad tvn=trustedValidatorNodes.GetNode(index);\\ \qquad \quad escrowV=tvn.GetEscrow();\\ \qquad \quad blockchain.RemoveEscrowAmount(escrowV);\,\,\,\,\\ \qquad \quad tvn.AddDeposit(escrowV);\,\,index++;\} \} \rightarrow Skip; \end{aligned}$

The $LLoseTrustAndDeposit$ defines that the leader’s number of activities, misses and deposit are set to zero (line 48).

48. $\begin{aligned} LLoseTrustAndDeposit()=ltrust\,\,\{\,\,\\ \,\,\,\,\quad selectedLeader.SetNumActivities(0);\\ \,\,\,\,\quad selectedLeader.SetNumMisses(0);\\ \,\,\,\,\quad selectedLeader.SetDeposit(0); \,\,\}\,\, \rightarrow \,\,Skip; \end{aligned}$

The validators’ number of activities and deposit are set to zero in $VLoseTrustAndDeposit$ process (line 49).

49. $\begin{aligned} VLoseTrustAndDeposit()=vltrust\,\,\{\,\,\\ \,\,\,\,\quad while(index\,\, < \,\,trustedValidatorNodes.\\ \qquad \quad GetLength()-1)\,\,\{\\ \qquad \quad tvn=trustedValidatorNodes.GetNode(index);\\ \qquad \quad tvn.SetNumActivities(0);\\ \qquad \quad tvn.SetDeposit(0);\,\,index++;\}\,\,\,\,\}\,\, \rightarrow \,\,Skip; \end{aligned}$

J. Next Round

In order to move the consensus protocol to the next round, the $nextRound$ process is specified (line 50). If the current round is less than the maximum number of rounds then the current round is incremented. All the necessary variables are cleared and the consensus protocol starts again.

50. $\begin{aligned} NextRound()=\,\,\\ \,\,\,\,\quad [rd\,\, < \,\,maxRounds]\,\,nextround\,\,\{\,\,rd++;\\ \,\,\,\,\quad lockedBlocks.Clear();\\ \,\,\,\,\quad bvotes0.Clear();\,\,bvotes1.Clear();\,\,bvotes2.Clear();\\ \quad \,\,\quad bvotes3.Clear();\,\,\,\,\\ \,\,\,\,\quad tvotes0.Clear();\,\,tvotes1.Clear();\,\,tvotes2.Clear();\\ \quad \,\,\quad tvotes3.Clear();\\ \,\,\,\,\quad managementNodes.Nullify(selectedLeader);\\ \,\,\,\,\quad validatorNodes.Nullify(trustedValidatorNodes);\\ \,\,\,\,\quad blockchain.Nullify(proposedBlock);\\ \,\,\quad \}\,\, \rightarrow \,\,Consensus\_{}\,\,Protocol()\,\, \square \,\,\\ \,\,\,\,\quad [rd\,\,>=\,\,maxRounds]\,\,Skip; \end{aligned}$

SECTION VI. Results and Analysis

We have verified our formal model of the proposed consensus protocol under normal and byzantine environments using the PAT model checker. We have defined five variations of our consensus protocol. The first two variations are defined with different numbers of malicious nodes with a threat factor of no vote (lines 51-52). The next two variations are specified with different numbers of malicious nodes but the voting behavior is defined as honest (lines 53-54). The fifth variation of consensus protocol simulates the behavior of an untrusted leader (lines 55-56). After the selection process, an untrusted leader is introduced which can try to add a block in the blockchain.

51. $\begin{aligned} Consensus\_{}\,\,Protocol\_{}\,\,With\_{}\,\,Minority\_{}\,\,Malicious\_{}\\ \hspace {-1.5em}\qquad \,\,\,\,No\_{}\,\,Vote()=IntroduceMaliciousNodes(Minority\_{}\\ \hspace {-1.5em}\qquad \,\,\,\,Nodes,\,\,No\_{}\,\,Vote);\,\,Consensus\_{}\,\,Protocol(); \end{aligned}$

52. $\begin{aligned} Consensus\_{}\,\,Protocol\_{}\,\,With\_{}\,\,Majority\_{}\,\,Malicious\_{}\\ \hspace {-1.5em}\qquad \,\,\,\,No\_{}\,\,Vote()=IntroduceMaliciousNodes(Majority\_{}\\ \hspace {-1.5em}\qquad \,\,\,\,Nodes,\,\,No\_{}\,\,Vote);\,\,Consensus\_{}\,\,Protocol(); \end{aligned}$

53. $\begin{aligned} Consensus\_{}\,\,Protocol\_{}\,\,With\_{}\,\,Minority\_{}\,\,Malicious\_{}\\ \hspace {-1.5em}\qquad \,\,\,\,Honest\_{}\,\,Vote()=IntroduceMaliciousNodes(Minority\\ \hspace {-1.5em}\qquad \quad \_{}Nodes,\,\,Honest\_{}\,\,Vote);Consensus\_{}\,\,Protocol(); \end{aligned}$

54. $\begin{aligned} Consensus\_{}\,\,Protocol\_{}\,\,With\_{}\,\,Majority\_{}\,\,Malicious\_{}\\ \hspace {-1.5em}\qquad \,\,\,\,Honest\_{}\,\,Vote()=IntroduceMaliciousNodes(Majority\\ \hspace {-1.5em}\qquad \,\,\,\,\_{}\,\,Nodes,\,\,Honest\_{}\,\,Vote);\,\,Consensus\_{}\,\,Protocol(); \end{aligned}$

55. $\begin{aligned} Consensus\_{}\,\,Protocol\_{}\,\,With\_{}\,\,Untrusted\_{}\,\,Leader()=\\ \hspace {-1.5em}\qquad \,\,\,\,(\parallel \,\,i:\{0..PNodes-1\} \text{@}(NodeInitialization();\\ \hspace {-1.5em}\qquad \,\,\,\,PerformTransactions();\,\,Selection();IntroduceUntr-\\ \hspace {-1.5em}\qquad \,\,\,\,ustedLeader();\,\,VoteForTransactions(T,\,\,i);\\ \hspace {-1.5em}\qquad \,\,\,\,ProposeAndBroadcast(i);\,\,VoteToBlock(i);\\ \hspace {-1.5em}\qquad \,\,\,\,isValidBlockchain();\,\,\,\,AddBlock(i);\\ \hspace {-1.5em}\qquad \,\,\,\,UpdateTrustAndDeposit()));\,\,NextRound(); \end{aligned}$

56. $\begin{aligned} IntroduceUntrustedLeader()=\{\,\,\\ \,\,\,\,\qquad selectedLeader=untrustedLeaderNode;\\ \,\,\,\,\qquad untrustedLeader=true; \,\,\}\,\, \rightarrow \,\,Skip; \end{aligned}$

LTL is used to specify the desired properties. The properties are represented as assertions in Table 3. We have verified general properties, as well as security properties, under normal and byzantine environments. The verification of properties under a byzantine environment shows that the proposed model is fault tolerant.

TABLE 3 Results for Verification of Security and Trust Properties Against the Formal Model

A. Deadlock-Free

A deadlock-free formal model is described as there does not occur a situation where a node has to wait for another node for an activity. The PAT model checker is used to query deadlock in the formal model. We have specified assertions and verified that the consensus protocol is deadlock-free in both normal and byzantine environments as shown in Table 3. The assertion $A1$ for the normal environment is specified below and for the byzantine environment, the assertions $A2$ -$A6$ are presented in Table 3.

1. $\#assert Consensus\_{} Protocol() deadlockfree;$

B. Consensus

Consensus is defined using $\#define$ as every node of the network must agree on the same block and add that block to its copy of the blockchain. It is specified as the peek block of each node’s chain should be the same.

• $\begin{aligned} \#define\,\,Consensus\,\,(!blockchain0.IsEmpty()\,\,\&\&\\ \hspace {-1.4em}\,\,blockchain0.GetPeekBlock()\,\,==\\ \hspace {-0.3em} \,\,\quad blockchain1.GetPeekBlock()\,\,\&\&\\ \hspace {-1.4em}\,\,blockchain1.GetPeekBlock()\,\,==\\ \hspace {-0.3em} \,\,\quad blockchain2.GetPeekBlock()\,\,\&\&\\ \hspace {-1.4em}\,\,blockchain2.GetPeekBlock()\,\,==\\ \hspace {-0.3em}\,\,\quad blockchain3.GetPeekBlock()); \end{aligned}$

LTL formulas are specified as assertions to verify that the formal model eventually reaches consensus or not in normal and byzantine environments. The assertion $A7$ for reaching consensus in the normal environment is specified below and for the byzantine environment, $A8$ -$A12$ are represented in Table 3. The symbol $\models $ is read as satisfies. It can be noted in Table 3 that the model does not reach consensus when the majority of nodes are malicious and they do not vote ($A9$ in Table 3). It is also observed that when an untrusted leader is added in the network then consensus cannot be reached ($A12$ in Table 3). This does not show that the consensus protocol is vulnerable but it is preferred that network nodes add no block in their ledger rather than adding a malicious block.

1. $\#assert Consensus\_{} Protocol() \models \lozenge Consensus;$

C. No Blockchain Fork

No blockchain fork can be assured when all nodes record the same proposed block in their blockchain. All nodes have a same view about the blockchain state.

• $\begin{aligned} \#define\,\,No\_{}\,\,Blockchain\_{}\,\,Fork\,\,(!blockchain0.IsEmpty()\,\,\&\&\\ \hspace {-1.4em}\,\,proposedBlock==blockchain0.GetPeekBlock()\,\,\&\&\\ \hspace {-1.4em}\,\,proposedBlock==blockchain1.GetPeekBlock()\,\,\&\&\\ \hspace {-1.4em}\,\,proposedBlock==blockchain2.GetPeekBlock()\,\,\&\&\\ \hspace {-1.4em}\,\,proposedBlock==blockchain3.GetPeekBlock()); \end{aligned}$

LTL formulas are specified below to verify that eventually no blockchain fork is ensured. Table 3 shows that the model ensures that a blockchain fork cannot occur in the normal environment as specified by an LTL formula $A13$ below and when the minority of nodes are malicious or byzantine nodes vote honestly as defined in Table 3 by LTL formulas $A14$ and $A16$ -$A17$ . The model does not satisfy this property when the majority of nodes are malicious and they do not vote ($A15$ in Table 3), and also when an untrusted leader is introduced into the network ($A18$ in Table 3). When the property is violated, then the proposed block cannot be added to the ledger of nodes but a fork does not occur.

1. $\begin{aligned} \#assert Consensus\_{} Protocol() \models \\ \qquad \lozenge No\_{} Blockchain\_{} Fork; \end{aligned}$

D. No Selfish Mining

No selfish mining is ensured when a leader of a peek block of every copy of the blockchain is the same. It shows that only the block of a single leader is added to the blockchain.

• $\begin{aligned} \#define\,\,No\_{}\,\,Selfish\_{}\,\,Mining\,\,(!blockchain0.IsEmpty()\,\,\&\&\\ \hspace {-1.8em}\,\,blockchain0.GetBlockLeader(blockchain0.GetPeekBlock())\\ \hspace {-1.8em}==blockchain1.GetBlockLeader(blockchain1.\\ \hspace {-1.8em}GetPeekBlock())\,\,\&\&\,\,blockchain1.GetBlockLeader(\\ \hspace {-1.8em}blockchain1.GetPeekBlock())==blockchain2.\\ \hspace {-1.8em}GetBlockLeader(blockchain2.GetPeekBlock())\,\,\&\&\,\,\,\,\\ \hspace {-1.8em}\,\,blockchain2.GetBlockLeader(blockchain2.GetPeekBlock())\\ \hspace {-1.8em}==blockchain3.GetBlockLeader(blockchain3.\\ \hspace {-1.8em}GetPeekBlock())); \end{aligned}$

LTL formulas are described to verify that there is no selfish mining in the protocol. The LTL formula $A19$ specified below is verified in the normal environment. In the byzantine environment, when the minority of nodes are malicious or byzantine nodes vote honestly, then the LTL formulas $A20$ , $A22$ -$A23$ shown in Table 3 are verified. However, when the majority of nodes become malicious and they do not vote for the block or an untrusted leader is added in the network then $A21$ and $A24$ exhibited in Table 3 are violated.

1. $\begin{aligned} \#assert Consensus\_{} Protocol() \models \\ \qquad \lozenge No\_{} Selfish\_{} Mining; \end{aligned}$

E. No Invalid Block Insertion

It is defined as in each round of consensus protocol there should not be any invalid (duplicate) block submitted by malicious leaders in the copy of blockchain of a node.

• $\begin{aligned} \#define\,\,No\_{}\,\,Invalid\_{}\,\,Block\_{}\,\,Insertion\,\,(rd>0\,\,\&\&\\ \hspace {-1.4em}\,\,!blockchain0.ContainsDuplicateBlocks()\,\,\&\&\\ \hspace {-1.4em}\,\,!blockchain1.ContainsDuplicateBlocks()\,\,\&\&\\ \hspace {-1.4em}\,\,!blockchain2.ContainsDuplicateBlocks()\,\,\&\& \\ \hspace {-1.4em}\,\,!blockchain3.ContainsDuplicateBlocks()); \end{aligned}$

The LTL formulas are specified to describe that the protocol and its variations satisfy eventually no invalid block insertion property. $A25$ is specified below for normal conditions while $A26$ -$A30$ are defined in Table 3 for byzantine conditions. Table 3 shows that all the variations of consensus protocol satisfy this property.

1. $\begin{aligned} \#assert\,\,Consensus\_{}\,\,Protocol()\,\,\models \\ \hspace {-0.3em}\,\,\qquad \lozenge \,\,No\_{}\,\,Invalid\_{}\,\,Block\_{}\,\,Insertion; \end{aligned}$

F. Safety

The safety property is defined as all the nodes reach the same decision. It means that all the nodes must agree on adding the same block. It can be ensured when there are no blockchain fork and no selfish mining attacks.

• $\begin{aligned} \#define\,\,Safety\,\,No\_{}\,\,Blockchain\_{}\,\,Fork\,\,\&\&\\ \hspace {-1.4em}\,\,No\_{}\,\,Selfish\_{}\,\,Mining; \end{aligned}$

The LTL formulas are described to verify that the protocol satisfies eventually safety property under normal and byzantine conditions. When the majority of the nodes become malicious and they adopt no voting behavior or an untrutsed leader is involved in the network then assertions $A33$ and $A36$ presented in Table 3 are not satisfied. The rest of the assertions $A31$ presented below and $A34$ -$A35$ represented in Table 3 are verified.

1. $\#assert Consensus\_{} Protocol() \models \lozenge Safety;$

G. Fault Tolerance

In each round, a common block will be accepted by all honest nodes even in the existence of some malicious nodes. This property is specified as reaching consensus. It is described below by an LTL formula $A37$ for normal conditions and LTL formulas $A38$ -$A42$ are defined in Table 3 for byzantine environment. Its behavior is similar to the consensus property as shown in Table 3.

• $\begin{aligned} \#define\,\,Fault\_{}\,\,Tolerance\,\,Consensus;\\ \hspace {-2.1em}\,\,A37.\,\,\#assert\,\,Consensus\_{}\,\,Protocol()\,\,\models \,\,\lozenge \,\,Fault\_{}\,\,Tolerance; \end{aligned}$

H. Trusted Leader

In every round of consensus, a trusted leader is selected. The LTL formulas are specified to verify that eventually a trusted leader is selected. $A43$ is described below for the normal environment and $A44$ -$A47$ for the byzantine environment are shown in Table 3. Table 3 represents that all the formulas are satisfied.

• $\begin{aligned} \#define\,\,trustedLeader\,\,(rd>=0\,\,\&\&\,\,leaderSelected==1);\\ \hspace {-2.1em}\,\,A43.\,\,\#assert\,\,Consensus\_{}\,\,Protocol()\,\,\models \,\,\lozenge \,\,trustedLeader; \end{aligned}$

I. Trusted Validators

The trusted validators are selected in every round of consensus protocol. LTL formulas are used to specify that eventually trusted validators are selected. $A48$ is defined below for the normal environment and $A49$ -$A52$ are described for the byzantine environment in Table 3. This property is verified for all the variations of consensus protocol as presented in Table 3.

• $\begin{aligned} \#define\,\,trustedValidators(rd>=0\,\,\&\&\,\,valSelected==1);\\ \hspace {-2.1em}\,\,A48.\,\,\#assert\,\,Consensus\_{}\,\,Protocol()\,\,\models \,\,\lozenge \,\,trustedValidators; \end{aligned}$

J. Analysis of the Protocol

We have performed the formal verification of the desired properties against the STBC protocol on an Intel i5-7200U 2.5 GHz CPU with 8 GB of memory, running Windows 10 and PAT version 3.5.1. The results of verification time (in seconds) of safety, fault tolerance, trusted leader, and trusted validators are presented in Figures 5, 6, 7, and 8 respectively. The number of nodes is represented on the horizontal axis and the verification time in seconds is shown on the vertical axis. The nodes involved are service consumers, service providers, blockchain management nodes, and validator nodes. When the properties are satisfied, it is analyzed that the verification time increases continuously with the increased count of nodes. In case of violation of a property, the verification time remains close to zero. For example, for the safety property, Figure 5 shows the assertions $A31$ , $A32$ , $A34$ , and $A35$ are satisfied, therefore, the verification time increases continuously with the increased count of nodes. However, the assertions $A33$ and $A36$ are not satisfied, therefore, the verification time remains close to zero. Similarly, the verification time of fault tolerance, trusted leader, and trusted validators properties increases with the increased count of nodes. Similar behavior is observed for the verification time of deadlock, consensus, no blockchain fork, no selfish mining, and no invalid block insertion properties.

FIGURE 5.

Verification time for safety.

FIGURE 6.

Verification time for fault tolerance.

FIGURE 7.

Verification time for trusted leader.

FIGURE 8.

Verification time for trusted validators.

We have performed formal verification for a limited number of nodes in the network. However, the proposed protocol itself is generic, and it can work for an arbitrary number of nodes. The noticeable point is that the verification time increases continuously with the increased count of nodes. With many nodes, an issue of state explosion may occur, which is one of the limitations of the model checking approach [33]. These limitations are outside the scope of this work. In the future, we plan to improve the efficiency of our model using different techniques, such as symbolic model checking with binary decision diagrams, partial order reduction, counterexample-guided abstraction refinement, and bounded model checking.

SECTION VII. Conclusion and Future Work

Secure and Trustworthy Blockchain-based Crowdsourcing consensus protocol is a formally verified consensus protocol, which ensures safety, fault tolerance, trusted leader, and trusted validator properties. It prevents security attacks, e.g., blockchain fork, selfish mining, and invalid block insertion. The proposed consensus protocol is energy-efficient as a single leader proposes a block in each round of the protocol. The trust model ensures fairness and decentralization because the waiting nodes also get a chance to become leaders. Ensuring the correctness of a consensus protocol has significant importance because the failure of a consensus protocol can lead to disastrous consequences. Therefore, to mitigate the associated risks, we have used a formal methods-based technique, i.e., model checking, which is automatic and effective to increase the formal model’s confidence of correctness. We have used CSP# for the formal specification of the consensus protocol. The security and trust properties are formally specified using LTL formulas. The PAT model checker is utilized to ensure the correctness of the formal specification against the specified properties.

At present, we have done model checking of our formal model for small number of nodes. For large number of nodes, state explosion can occur which will be addressed in future using different techniques such as symbolic model checking with binary decision diagrams, partial order reduction, counterexample-guided abstraction refinement and bounded model checking. The future work will consider failure or unavailability of nodes. Formal verification of further security properties, e.g., persistence and liveness, against the formal model will be done. We will do the performance analysis of the proposed consensus protocol using simulation techniques in addition to formal verification to get benefit of both approaches.