Formal Methods-based Security for the Internet of Medical Things (IoMT)
Imane Bouziane, Houda Belmokadem, Mohamed Moussaoui · River Publishers eBooks · 2025
Security is of utmost importance in wireless body area networks, also referred to as WBANs, within the domain of IoMT (Internet of Medical Things), considering the crucial significance of the data involved, which primarily consists of sensitive medical information of patients. WBANs play a crucial role in healthcare applications by enabling the collection and transmission of physiological data from wearable or implantable medical devices. For this reason, ensuring the security of this data is paramount to protect patient confidentiality, prevent unauthorized access, and maintain the trustworthiness of healthcare systems. In this context, formal verification emerges as a highly effective method for not only identifying potential vulnerabilities but also providing security guarantees for WBANs in the IoMT domain. In contrast to testing techniques that reveal problems but cannot prove their absence, formal verification involves mathematically analyzing the behavior and properties of a system, such as a WBAN protocol, using rigorous and systematic techniques. By subjecting WBANs to formal verification, researchers can detect design flaws, uncover potential security weaknesses, and validate the effectiveness of security measures. This chapter seeks to explore the intersection of formal methods and security in literature. It considers the analysis of WBANs within the IoMT domain to prove the absence of flaws and vulnerabilities formally.