@inproceedings{b8c9cfb1924446dab4422596608fc3dc,
title = "The Formal Verification of Aptos Coin",
abstract = "The fungible contract tokens encounter numerous security challenges due to the vulnerabilities in contract languages; while Move, a novel and secure contract language, is designed to mitigate these vulnerabilities theoretically. To verify the security of the Move-based contract coin, this paper employs formal methods to model the Aptos coin, a leading Move-based token, and assess its high-level properties. Firstly, we examined Aptos Coin{\textquoteright}s contract code and integrated the Move{\textquoteright}s characteristics to construct a bottom-up model. Subsequently, we specified the necessary high-level properties that the model should possess. Finally, we utilize the Move Prover, a model-checking tool to verify the essential secure properties of Aptos coin. The results demonstrate that the Aptos coin can satisfy the properties with few prerequisite conditions.",
keywords = "Formal Verification, Fungible Token, Move Language, Smart Contract",
author = "Kundu Chen and Jie Luo and Yi Lu and Zhongyun Zhang and Wenbo Zhang and Xudong Wang and Pan Li and Jun Zhao",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.; 27th Information Security Conference, ISC 2024 ; Conference date: 23-10-2024 Through 25-10-2024",
year = "2025",
doi = "10.1007/978-3-031-75757-0\_1",
language = "英语",
isbn = "9783031757563",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "3--22",
editor = "Nicky Mouha and Nick Nikiforakis",
booktitle = "Information Security - 27th International Conference, ISC 2024, Proceedings",
address = "德国",
}