A Theoretical Perspective on the Formal Verification of IoT Protocols Using LTL and Rewriting Logic in Maude

Delia-Iustina Grigoriță

Paper 2025/1078

A Theoretical Perspective on the Formal Verification of IoT Protocols Using LTL and Rewriting Logic in Maude

Delia-Iustina Grigoriță

, Alexandru Ioan Cuza University, Iași

Abstract

As Internet of Things (IoT) systems become increasingly complex, verifying communication protocols is essential to guarantee their security and correctness. This paper introduces a brief introduction to the theoretical concepts of how to use formal techniques, LTL and rewriting logic within the Maude system to verify the security and proper behavior of the protocols. While rewriting logic explains how various events occur over time, LTL explains how a property can be formulated. This theoretical perspective is intended to inform future applications and research.

Metadata

Available format(s): PDF
Category: Foundations
Publication info: Preprint.
Keywords: Model Checking Maude Rewriting Logic IoT Protocols Temporal Logic Security
Contact author(s): deliaiustinagrigorita @ gmail com
History: 2025-06-10: approved; 2025-06-09: received; See all versions
Short URL: https://ia.cr/2025/1078
License: CC BY

BibTeX

@misc{cryptoeprint:2025/1078,
      author = {Delia-Iustina Grigoriță},
      title = {A Theoretical Perspective on the Formal Verification of {IoT} Protocols Using {LTL} and Rewriting Logic in Maude},
      howpublished = {Cryptology {ePrint} Archive, Paper 2025/1078},
      year = {2025},
      url = {https://eprint.iacr.org/2025/1078}
}