A Formal Model of Algorand Smart Contracts

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

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

543 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 languageEnglish
Title of host publicationFinancial Cryptography and Data Security
PublisherSpringer
Publication date2021
Pages93-114
ISBN (Print)978-3-662-64321-1
DOIs
Publication statusPublished - 2021
EventInternational Conference on Financial Cryptography and Data Security 2021 - Virtual event
Duration: 1 Mar 20215 Mar 2021
Conference number: 25
https://fc21.ifca.ai/

Conference

ConferenceInternational Conference on Financial Cryptography and Data Security 2021
Number25
LocationVirtual event
Period01/03/202105/03/2021
Internet address
SeriesLecture Notes in Computer Science
Volume12674
ISSN0302-9743

Fingerprint

Dive into the research topics of 'A Formal Model of Algorand Smart Contracts'. Together they form a unique fingerprint.

Cite this