Formal verification of fraud-resilience in a crowdsourcing consensus protocol

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 tech-nology that can resolve most of these issues, however, it is difficult to find an appropriate consensus pro-tocol 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 con-sidering 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.& COPY; 2023 Elsevier Ltd. All rights reserved.