Formalizing Blockchain-Based Communication for Tactical Data Link
摘要
Tactical Data Link (TDL) has been widely used to enhance communication and coordination among different parties in various scenarios. Recently, there has been growing interest in leveraging blockchain technology to address the challenges faced by traditional TDL systems, particularly in terms of trust, information sharing, and data consistency. In this paper, we employ process algebra Communicating Sequential Processes (CSP) to model and verify a blockchain-based TDL communication mechanism. Our approach captures the core features of the system, with a focus on the consensus achievement mechanism among TDL nodes and systemic issues arising when the system reaches its fault tolerance threshold. We analyze and verify key properties such as deadlock-freedom and liveness to ensure system reliability, as well as linearizability and data consistency to evaluate system security guarantees. Our results demonstrate that while the system maintains functional correctness within the fault tolerance threshold, its vulnerabilities beyond this limit require further investigation and enhancement.