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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Formalizing Blockchain-Based Communication for Tactical Data Link

  • Shangzhe Wu,
  • Yongxin Zhao,
  • Qiang Wang,
  • Qiang Chen,
  • Yongjian Li

摘要

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.