Tamarin-based verification of authentication protocols in smart city IoT

Abstract

The rapid growth of smart city applications relies heavily on Internet of Things (IoT) devices, where secure and reliable authentication protocols are essential for protecting sensitive data and services. However, these protocols often operate in dynamic and heterogeneous environments that expose them to replay, impersonation, and man-in-the-middle attacks. Traditional evaluation approaches frequently overlook subtle logical flaws in protocol design, leaving systems vulnerable de-spite appearing secure. This study employs the Tamarin Prover, a state-of-the-art symbolic verification tool, to systematically verify authentication protocols within smart city IoT infrastructures. Through rigorous modelling and lemma-based proofs, the protocols are examined against well-defined security properties, including secrecy, integrity, replay resistance, and impersonation prevention. The analysis uncovers both confirmed guarantees and hidden vulnerabilities, demonstrating how formal methods reveal weaknesses that informal reasoning may miss. By establishing a replicable Tamarin-based verification framework, this study not only validates the effectiveness of formal analysis for enhancing trust in IoT infrastructures but also provides practical insights to guide the secure design and deployment of future smart city authentication mechanisms.