On the parameterized verification of abstract models of contact tracing protocols

We present an automata-based formal model of distributed systems specifically devised to formalise abstractions of Contact Tracing Protocols that combine Bluetooth and network communication. The model combines pure names, read/write operations on first-order and higher-order variables and synchronous communication primitives. The transition system models the interaction between devices in the same physical location and between a single device and a notification server. To automatically validate protocols in our formalism, we resort to an extension of the Cubicle SMT-based infinite-state model checker, in which the monotonic abstraction applied during the predecessor computation is strengthen by introducing abstract predicates obtained via Counting Abstraction.