Abstract
Modal μcalculus is a wellknown formalism for describing properties of statebased transition systems. It can define properties such as "[in the current state] p holds, and there is a path where is holds again at some point in the future", where p comes from some fixed vocabulary of basic predicates.
A formula of the classical μcalculus refers only to finitely many basic predicates, which may sometimes seem restrictive. Real systems routinely operate on data coming from potentially infinite domains, such as numbers or character strings. Basic properties of such systems may reasonably include ones like "the number n was input", for every number n. It is then not clear how to say that "there exists a transition path where the currently input number is input again some time in the future" as a formula.
Various modal formalisms have been proposed to model temporal properties of systems that refer to data coming from infinite domains. Here I focus on the modal μcalculus with atoms, which is an extension of the classical calculus with features of nominal sets. There, basic predicates, formulas and models rely on atoms that come from some fixed infinite domain and can be tested for equality (or, in an extended variant, for some fixed order).
I present a few variants of the modal μcalculus with atoms, and describe their properties. As an example application, I show how to formulate the security property of the cryptographic NeedhamSchroeder protocol, which relies on generating atomic nonces and comparing them for equality, and which famously fails due to a maninthemiddle attack.
Much of the material presented in this talk is drawn from [C. Eberhart and B. Klin, 2019; B. Klin and M. Łełyk, 2019; B. Klin and M. Łełyk, 2017].
BibTeX  Entry
@InProceedings{klin:LIPIcs:2021:13435,
author = {Bartek Klin},
title = {{μCalculi with Atoms (Invited Talk)}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {1:11:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771757},
ISSN = {18688969},
year = {2021},
volume = {183},
editor = {Christel Baier and Jean GoubaultLarrecq},
publisher = {Schloss DagstuhlLeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13435},
URN = {urn:nbn:de:0030drops134358},
doi = {10.4230/LIPIcs.CSL.2021.1},
annote = {Keywords: modal μcalculus, sets with atoms}
}
Keywords: 

modal μcalculus, sets with atoms 
Collection: 

29th EACSL Annual Conference on Computer Science Logic (CSL 2021) 
Issue Date: 

2021 
Date of publication: 

13.01.2021 