We develop a formal model of Algorand stateless smart contracts (stateless ASC1). We exploit our model to prove fundamental properties of the Algorand blockchain, and to establish the security of some archetypal smart contracts. While doing this, we highlight various design patterns supported by Algorand. We perform experiments to validate the coherence of our formal model w.r.t. the actual implementation.
A Formal Model of Algorand Smart Contracts / Bartoletti, Massimo; Bracciali, Andrea; Lepore, Cristian; Scalas, Alceste; Zunino, Roberto. - 12674:(2021), pp. 93-114. (Intervento presentato al convegno Financial Cryptography and Data Security. FC 2021 tenutosi a Online nel March 1–5, 2021) [10.1007/978-3-662-64322-8_5].
A Formal Model of Algorand Smart Contracts
Zunino, Roberto
2021-01-01
Abstract
We develop a formal model of Algorand stateless smart contracts (stateless ASC1). We exploit our model to prove fundamental properties of the Algorand blockchain, and to establish the security of some archetypal smart contracts. While doing this, we highlight various design patterns supported by Algorand. We perform experiments to validate the coherence of our formal model w.r.t. the actual implementation.| File | Dimensione | Formato | |
|---|---|---|---|
|
main.pdf
Solo gestori archivio
Tipologia:
Post-print referato (Refereed author’s manuscript)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
619.67 kB
Formato
Adobe PDF
|
619.67 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
