A Formal Model of Algorand Smart Contracts

Massimo Bartoletti; Andrea Bracciali; Cristian Lepore; Alceste Scalas; Roberto Zunino

doi:10.1007/978-3-662-64322-8_5

A Formal Model of Algorand Smart Contracts

Massimo Bartoletti, Andrea Bracciali, Cristian Lepore, Alceste Scalas, Roberto Zunino

Department of Applied Mathematics and Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

614 Downloads (Pure)

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.

Original language	English
Title of host publication	Financial Cryptography and Data Security
Publisher	Springer
Publication date	2021
Pages	93-114
ISBN (Print)	978-3-662-64321-1
DOIs	https://doi.org/10.1007/978-3-662-64322-8_5
Publication status	Published - 2021
Event	International Conference on Financial Cryptography and Data Security 2021 - Virtual event Duration: 1 Mar 2021 → 5 Mar 2021 Conference number: 25 https://fc21.ifca.ai/

Conference

Conference	International Conference on Financial Cryptography and Data Security 2021
Number	25
Location	Virtual event
Period	01/03/2021 → 05/03/2021
Internet address	https://fc21.ifca.ai/

Series	Lecture Notes in Computer Science
Volume	12674
ISSN	0302-9743

Access to Document

10.1007/978-3-662-64322-8_5

FulltextAccepted author manuscript, 439 KB

OpenUrl availability

Full text

Cite this

@inproceedings{fb218c201c5b4d1d8952b574d25ea03c,

title = "A Formal Model of Algorand Smart Contracts",

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.",

author = "Massimo Bartoletti and Andrea Bracciali and Cristian Lepore and Alceste Scalas and Roberto Zunino",

year = "2021",

doi = "10.1007/978-3-662-64322-8_5",

language = "English",

isbn = "978-3-662-64321-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "93--114",

booktitle = "Financial Cryptography and Data Security",

note = "International Conference on Financial Cryptography and Data Security 2021, FC21 ; Conference date: 01-03-2021 Through 05-03-2021",

url = "https://fc21.ifca.ai/",

}

TY - GEN

T1 - A Formal Model of Algorand Smart Contracts

AU - Bartoletti, Massimo

AU - Bracciali, Andrea

AU - Lepore, Cristian

AU - Scalas, Alceste

AU - Zunino, Roberto

N1 - Conference code: 25

PY - 2021

Y1 - 2021

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-662-64322-8_5

DO - 10.1007/978-3-662-64322-8_5

M3 - Article in proceedings

SN - 978-3-662-64321-1

T3 - Lecture Notes in Computer Science

SP - 93

EP - 114

BT - Financial Cryptography and Data Security

PB - Springer

T2 - International Conference on Financial Cryptography and Data Security 2021

Y2 - 1 March 2021 through 5 March 2021

ER -

A Formal Model of Algorand Smart Contracts

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this