Formal verification of fraud-resilience in a crowdsourcing consensus protocol
Hamra Afzaal, Muhammad Ali Imran, Muhammad Umar Janjua · Computers & Security · 2023
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.