μ-Calculi with Atoms (Invited Talk).

Modal μ-calculus is a well-known formalism for describing properties of state-based transition systems. It can define properties such as [in current state] p holds, and is a path where is holds again at some point in future, where p comes from some fixed vocabulary of basic predicates. A formula of 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 currently input number is input again some time in 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 modal μ-calculus with atoms, which is an extension of 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 modal μ-calculus with atoms, and describe their properties. As an example application, I show how to formulate security property of cryptographic Needham-Schroeder protocol, which relies on generating atomic nonces and comparing them for equality, and which famously fails due to a man-in-the-middle attack. Much of material presented in this talk is drawn from [C. Eberhart and B. Klin, 2019; B. Klin and M. Łelyk, 2019; B. Klin and M. Łelyk, 2017].