Formalization and Verification of Delegate Contract Signing Mechanism Based on Smart Contract Using CSP

Bangjie Zhu, Jiaqi Yin, Sini Chen, Huibiao Zhu

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Smart contracts are widely applied in financial delegation contracts to address contract fraud. The smart contract delegation contract signing mechanism (DCSM-SC) effectively tackles fraud risks arising from information and interest asymmetry. However, in dealing with financial contracts, a formalized analysis method is necessary.This paper models the delegation contract signing mechanism involving six key entities using CSP (Communicating Sequential Processes), and employs the PAT (Process Analysis Toolkit) model checker to verify six key properties: deadlock freedom, divergence freedom, data reachability, data correctness, anti-attack capability, and data leakage under the threat of intermediary attacks.

Original languageEnglish
Title of host publication39th Annual ACM Symposium on Applied Computing, SAC 2024
PublisherAssociation for Computing Machinery
Pages300-302
Number of pages3
ISBN (Electronic)9798400702433
DOIs
StatePublished - 8 Apr 2024
Event39th Annual ACM Symposium on Applied Computing, SAC 2024 - Avila, Spain
Duration: 8 Apr 202412 Apr 2024

Publication series

NameProceedings of the ACM Symposium on Applied Computing

Conference

Conference39th Annual ACM Symposium on Applied Computing, SAC 2024
Country/TerritorySpain
CityAvila
Period8/04/2412/04/24

Keywords

  • communicating sequential processes (CSP)
  • delegate contract signing mechanism (DCSM)
  • modeling
  • smart contract
  • verification

Fingerprint

Dive into the research topics of 'Formalization and Verification of Delegate Contract Signing Mechanism Based on Smart Contract Using CSP'. Together they form a unique fingerprint.

Cite this