| Abstract |
The rapid proliferation of machine-to-machine (M2M) communications has transformed numerous sectors, ranging from industrial automation to smart cities. However, the increasing connectivity among autonomous devices raises significant security concerns, particularly regarding the integrity and confidentiality of the exchanged data. This paper explores the application of formal verification techniques to M2M nodes to ensure secure communications. By employing model checking and theorem proving methods, we systematically analyze the behavior of M2M nodes to detect and mitigate vulnerabilities that could be exploited by malicious entities. The formal models developed capture the critical security properties such as authentication, data integrity, and confidentiality. The results demonstrate that formal verification provides a rigorous framework for identifying and resolving security flaws, thereby enhancing the overall resilience of M2M networks against potential cyber threats. This research highlights the importance of integrating formal methods in the design and deployment of secure M2M communication systems, paving the way for more robust and trustworthy autonomous networks. © 2025 selection and editorial matter, Gaurav Aggarwal, Ashutosh Tripathi, Himani Goyal Sharma, Tripti Sharma and Rishabh Dev Shukla; individual chapters, the contributors. |
