Logo image
Back
Formal Verification of the Burn-to-Claim Blockchain Interoperable Protocol
Conference proceeding   Peer reviewed

Formal Verification of the Burn-to-Claim Blockchain Interoperable Protocol

Babu Pillai, Zhe Hou, Kamanashis Biswas and Vallipuram Muthukkumarasamy
Formal Methods and Software Engineering, ICFEM 2023: Lecture Notes in Computer Science, Vol.14308, pp.249-254
Lecture Notes in Computer Science
International Conference on Formal Engineering Methods, ICFEM 2023, 24th (Brisbane, Australia, 21/11/2023–24/11/2023)
09/11/2023
DOI: https://doi.org/10.1007/978-981-99-7584-6_15

Metrics

1 Record Views

Abstract

This paper introduces an abstract blockchain model that employs the Burn-to-Claim cross-blockchain protocol [1]. This multi-level simulator models a virtual environment of nodes running on the Ethereum Virtual Machine (EVM). Developed using the CSP# language [2], it has undergone formal verification with the model checker PAT. Focusing on inter-network operations, our model (https://github.com/b-pillai/Burn-to-Claim-formal-verification) examines the properties of correctness, security, and atomicity using PAT. Surprisingly, atomicity, assumed to be inherent in the time-lock mechanism of the Burn-to-Claim protocol, does not always hold. We establish its validity under specific assumptions while confirming the protocol's correctness and security under the added assumptions.

Details

Logo image