A formally verified authentication protocol in secure framework for mobile healthcare during COVID-19-like pandemic

Figures & data

Figure 1. Security and Privacy-aware Mobile Healthcare Framework (SPMHF).

Figure 2. Steps in the Health Monitoring Mechanism.

Table 1. Major notations and their meanings.

Notation	Meaning	Notation	Meaning
CHA	Central Healthcare Authority	$\mathit{S}{\mathit{K}}_{\mathit{P}\mathit{H}}$	Symmetric Key shared between P & H
H	Hospital	$\mathit{S}{\mathit{K}}_{\mathit{H}\mathit{D}}$	Symmetric Key shared between H & D
S	Sensor/BSN	$\mathit{S}{\mathit{K}}_{\mathit{P}\mathit{S}}$	Symmetric Key Shared between P & S
D	Doctor	${\mathit{T}}_{\mathit{P}}$	Timestamp generated by P
$\mathit{I}{\mathit{D}}_{\mathit{P}}$	Identity of Patient	${\mathit{T}}_{\mathit{H}}$	Timestamp generated by H
PD	Patient Data	${\mathit{T}}_{\mathit{S}}$	Timestamp generated by S
P	Patient	${\mathit{N}}_{\mathit{P}}$	Nonce generated by P
$\mathit{I}{\mathit{D}}_{\mathit{H}}$	Identity of Hospital	${\mathit{N}}_{\mathit{S}}$	Nonce generated by S
ACK	Acknowledgment	${\mathit{N}}_{\mathit{H}}$	Nonce generated by H

Table 2. Threat modelling.

STRIDE	Threats	Countermeasures Provided by SPMHF
Spoofing	Insider attacks. Spoofing of source – patient medical devices may be spoofed by intruders, leading to incorrect data being delivered to patient communication devices. Spoofing of source - patient communication devices may be spoofed by intruders, leading to data being written to the intruder's target instead of the patient’s communication device. Spoofing of source – CCH servers may be spoofed by intruders, leading to incorrect data. Spoofing by tampering or reverse engineering to spoof.	An insider can try intentionally to hack the data from the Hospital TPM in CCH. However, he needs to access an authorised doctor’s credentials, including the password, biometric, and doctor's digital signature. The adversary cannot steal a patient’s information; hence, the proposed system withstands privileged insider attacks. Patients are authenticated at the MHA using a password and biometrics. Patient’s credentials are securely stored in the UICC of smartphones and are protected by password and biometrics (i.e. Robust Authentication). Messages are encrypted using the AES algorithm. White-Box Cryptography (WBC) is implemented in the MHA, ensuring encryption keys’ safety and security. TLS protocol ensures communication security. Intruders will be unsuccessful in tampering or reverse-engineering MHA as the code of MHA is attested and obfuscated; also, MHA is restricted to self-signing.
Tampering	Data tampering – patients and doctors intentionally or accidentally can modify, add, and delete data. Log Files tampering – patients, system admins, or formal or informal healthcare providers can delete or update log files in any way.	Role-Based Access Control (RBAC) is deployed in the SPMHF framework. Hence, this is not possible. All the messages exchanged are free from tampering as all the messages are encrypted using the AES algorithm. TLS cryptographic protocol ensures communication security in the SPMHF protocol. Hence, such log file tampering is not possible.
Repudiation	Potential data repudiation – patient and doctors denies or claims not receiving, writing, or editing data.	SPMHF has a Logging and Monitoring Control Manager (LMCM); it performs anomaly detection using statistical and machine learning (ML) algorithms and identifies traffic variances against pre-defined conditions. Any deviation of a system from standard access control policies could be monitored. Also, various authentication attempts (either passed or failed), management of users, rights management are recorded using logs. The items in a log are User IDs (identities), Exact timestamp (date-time) for logging in and logging off, device location using the LAN (Local Area Network), and an ID of the access point, or ID of the remote-access system.
Information disclosure	Unauthorised disclosure of data. Lost device – patients losing their communication devices would expose sensitive data such as login credentials and Patient Healthcare Records (PHR). Stolen device – theft of patient communication devices that would expose sensitive data such as login credentials and PHRs. Weak access control – improperly protected data stored in patients’ communication devices could allow attackers to read information not intended for disclosure.	RBAC is deployed in the SPMHF framework. It is safe against stolen verifier attack as the adversary cannot get any verifier or any relevant information from SE or MHA of either the sensor or smartphone as SE is tamper-resistant while MHA adopts WBC. If an adversary steals a sensor or smartphone, he will not be able to extract a patient’s credentials (keys) or health information as the sensor and smartphone do not store patient’s health records. The credentials (keys) stored in SE cannot be captured by adversary as SE is tamper-resistant. An adversary cannot obtain credentials (keys) from MHA either because it adopts WBC. All the messages exchanged are free from tampering as all the messages are encrypted using the AES algorithm. TLS protocol ensures communication security.
Elevation of privilege	Elevation using impersonation – informal healthcare professionals (e.g. friends or family members) may impersonate the patient’s context to gain additional privileges. Unauthorised access to administration interfaces – malicious users may gain access to configuration management through administration interfaces.	RBAC is deployed in the SPMHF framework. An intruder cannot generate a session key. Hence, it cannot decrypt the messages transmitted. Respective entities personalise MHA. If a symmetric shared key is compromised, CCH updates the keys OTA automatically; so, key freshness is ensured. Therefore, it could thwart an impersonation attack. A parallel session attack is not possible in our mechanism as SSL/TLS protocol is used for secure channel initiation, while application security is ensured by encryption using the AES algorithm.

Table 3. Computational Costs for Login & Authentication Phases.

Protocol	Cost for P’s smartphone	Cost for S	Cost for Gateway	Overall computation cost	Overall execution time (sec)
(Kumar et al., 2012)	4TH + 2TS	TH + 2TS	TH + 3TS	6TH + 7TS	0.9145
(He et al., 2015)	4TH+2TS	TH + 2TS	2TH+5TS	7TH + 9TS	1.1755
(Li et al., 2016)	6TH + 2TS	5TH + 2TS	7TH + 6TS	18TH + 10TS	1.3102
(Wu et al., 2017)	10TH+2TS	4TH + TS	6TH+5TS	20TH+8TS	1.0504
Our Proposed	TS	TS	Not Applicable	2TS	0.2606

Figure 3. Bar chart for computational costs of login and authentication phases.

Table 4. Comparative chart of energy costs.

Protocol	Cost for P’s smartphone	Cost for S	Cost for Gateway	Overall energy cost	Overall Energy cost in µJoules
(Kumar et al., 2012)	4EH + 2ES	EH + 2ES	TH+ 3ES	6EH + 7ES	13.03 µJ
(He et al., 2015)	4EH+2ES	EH+2ES	2EH+5ES	7EH + 9ES	16.21 µJ
(Li et al., 2016)	6 EH + 2ES	5 EH +2 ES	7 EH + 6ES	18 EH+ 10ES	24.89 µJ
(Wu et al., 2017)	10 EH + 2ES	4 EH +ES	6 EH + 5ES	20 EH+ 8ES	88 µJ
Our Proposed	ES	ES	Not Applicable	2ES	2.42 µJ

Figure 4. Bar chart for energy costs of login and authentication phases.

Kumar, P., Lee, S.-G., & Lee, H.-J. (2012). E-SAP: efficient-strong authentication protocol for healthcare applications using wireless medical sensor networks. Sensors, 12(2), 1625–1647. doi:10.3390/s120201625

 PubMed Web of Science ®Google Scholar

He, D., Kumar, N., Chen, J., Lee, C.-C., Chilamkurti, N., & Yeo, S.-S. (2015). Robust anonymous authentication protocol for health-care applications using wireless medical sensor networks. Multimedia Systems, 21(1), 49–60. doi:10.1007/s00530-013-0346-9

 Web of Science ®Google Scholar

Li, X., Niu, J., Kumari, S., Liao, J., Liang, W., & Khan, M. K. (2016). A new authentication protocol for healthcare applications using wireless medical sensor networks with user anonymity. Security and Communication Networks, 9(15), 2643–2655. doi:10.1002/sec.1214

 Web of Science ®Google Scholar

Wu, F., Xu, L., Kumari, S., & Li, X. (2017). An improved and anonymous two-factor authentication protocol for health-care applications with wireless medical sensor networks. Multimedia Systems, 23(2), 195–205. doi:10.1007/s00530-015-0476-3

 Web of Science ®Google Scholar