Paper 2021/798

Probabilistic Dynamic Input Output Automata (Extended Version)

Pierre Civit, Sorbonne University, French National Centre for Scientific Research, Laboratoire de Recherche en Informatique de Paris 6
Maria Potop-Butucaru, Sorbonne University, French National Centre for Scientific Research, Laboratoire de Recherche en Informatique de Paris 6
Abstract

We present probabilistic dynamic I/O automata, a framework to model dynamic probabilistic systems. Our work extends dynamic I/O Automata formalism of Attie & Lynch to probabilistic setting. The original dynamic I/O Automata formalism included operators for parallel composition, action hiding, action renaming, automaton creation, and behavioral sub-typing by means of trace inclusion. They can model mobility by using signature modification. They are also hierarchical: a dynamically changing system of interacting automata is itself modeled as a single automaton. Our work extends to probabilistic settings all these features. Furthermore, we prove necessary and sufficient conditions to obtain the implementation monotonicity with respect to automata creation and destruction. Our construction uses a novel proof technique based on homomorphism that can be of independent interest. Our work lays down the foundations for extending composable secure-emulation of Canetti et al. to dynamic settings, an important tool towards the formal verification of protocols combining probabilistic distributed systems and cryptography in dynamic settings (e.g. blockchains, secure distributed computation, cybersecure distributed protocols etc).

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. 36th International Symposium on Distributed Computing, DISC 2022
DOI
10.4230/LIPIcs.DISC.2022.20
Keywords
Automata Distributed Computing Formal Verification Dynamic systems
Contact author(s)
pierrecivit @ gmail com
maria potop-butucaru @ lip6 fr
History
2022-08-22: last of 2 revisions
2021-06-14: received
See all versions
Short URL
https://ia.cr/2021/798
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2021/798,
      author = {Pierre Civit and Maria Potop-Butucaru},
      title = {Probabilistic Dynamic Input Output Automata (Extended Version)},
      howpublished = {Cryptology {ePrint} Archive, Paper 2021/798},
      year = {2021},
      doi = {10.4230/LIPIcs.DISC.2022.20},
      url = {https://eprint.iacr.org/2021/798}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.