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
Bracciali A.;
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 in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
fc2021-202.pdf
Accesso riservato
Descrizione: revised authors' paper
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
565.62 kB
Formato
Adobe PDF
|
565.62 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
|
PRINTED_algorandModelFC.pdf
Accesso riservato
Tipo di file:
PDF EDITORIALE
Dimensione
789.65 kB
Formato
Adobe PDF
|
789.65 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
