- Title
- Formal verification of fraud-resilience in a crowdsourcing consensus protocol
- Creator
- Afzaal, Hamra; Imran, Muhammad; Janjua, Muhammad
- Date
- 2023
- Type
- Text; Journal article
- Identifier
- http://researchonline.federation.edu.au/vital/access/HandleResolver/1959.17/194260
- Identifier
- vital:18316
- Identifier
-
https://doi.org/10.1016/j.cose.2023.103290
- Identifier
- ISSN:0167-4048
- Abstract
- •A Trust and Transactions Chain consensus protocol is proposed for a blockchain-based crowdsourcing system.•Communicating Sequential Programs language is utilized for the formal modeling of the proposed consensus protocol.•The properties of no sybil attack, no eclipse attack, and fraud-resilience are defined through Linear Temporal Logic.•Model checking is employed to ensure the correctness of the proposed consensus protocol.•The formal verification is performed by giving the formal model and properties as input to the Process Analysis Toolkit. [Display omitted] Crowdsourcing has emerged as a promising computing paradigm that utilizes human intelligence to achieve complex tasks, but it encounters several security and trust issues. Blockchain is a potential technology that can resolve most of these issues, however, it is difficult to find an appropriate consensus protocol applicable to crowdsourcing systems. Therefore, this work presents a Trust and Transactions Chain (TTC) consensus protocol built upon blockchain technology. It selects a trusted leader and validators considering a trust model which depends on deposit ratio, block generation and validation rate, and waiting rate. The TTC protocol addresses the main challenge of ensuring correctness related to critical systems of crowdsourcing which has extreme significance as their failure can result in disastrous consequences. This work is primarily focused on fraud-resilience avoiding double-spending attack. It also deals with sybil and eclipse attacks. Model checking is exploited because it is effective and automatic to conduct formal verification. The TTC protocol is formally modeled utilizing Communicating Sequential Programs, and the fraud-resilience property is specified using Linear Temporal Logic. The verification of the model is done using Process Analysis Toolkit that takes the formal model and specified properties as input to inspect the properties’ satisfaction or violation. The results of the formal verification are analyzed with respect to the verification time and the number of visited states.
- Publisher
- Elsevier
- Relation
- Computers & security Vol. 131, no. (2023), p. 103290
- Rights
- All metadata describing materials held in, or linked to, the repository is freely available under a CC0 licence
- Rights
- Copyright Elsevier
- Subject
- Blockchain; Consensus protocol; Crowdsourcing; Model checking; Trust and transactions chain; 4604 Cybersecurity and privacy
- Reviewed
- Hits: 507
- Visitors: 453
- Downloads: 0