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

Abstract

Existing schemes in the realm of mobile healthcare (also, e-Healthcare) based on cloud and IoMT (Internet of Medical Things) do not ensure end-to-end security and are not compliant with HIPAA (Health Insurance Portability and Accountability Act). It is also very difficult often for these schemes to obtain evidence from the cloud in case of security breaches. In addition to these issues, mobile healthcare applications are prone to various types of attacks and formal proof is often unavailable. In this work, we propose our community cloud framework in an IoMT setting that ensures end-to-end security and circumvents many of the existing negative aspects using the Trusted Platform Module (TPM). We provide necessary proofs using BAN logic and Scyther tool. Also, we show that the energy consumption and the costs of communication and computation for our proposed protocol are far less than that of the existing protocols. We have implemented our protocol using Kotlin language in Android Studio ensuring all the required security properties.

KEYWORDS:

• BAN (Burrows–Abadi–Needham) Logic
• Community Cloud
• Health Insurance Portability and Accountability Act (HIPAA)
• Mobile
• Scyther tool
• Trust

1. Introduction

The exponential growth of IoT-enabled (Internet of Things-enabled) wearable devices such as smart medical sensors and healthcare management software has led to the revolution of collecting and storing healthcare data. Nowadays, we see a trend of increased use of IT (Information Technology) facilities and cyberspace. As one of the prominent technologies today, cloud computing also plays a vital role in some mobile healthcare systems. There is an expectation that this trend would grow fast in the coming days contributing to the field of IoMT in general. In fact, during recent outbreak of COVID-19 pandemic (Pathan, 2020), the necessity of IoMT for remote healthcare services has significantly been realised.

As part of IoMT (Parthasarathy & Vivekanandan, 2020), cloud computing is linked with the healthcare system; stored data could be sent to the hospitals and the doctors quickly from external storage. While using cloud can reduce the burden of a hospital to possess its own data storage facility and strong IT infrastructure, in such a setting, ensuring security and privacy of data would be quite difficult given the nature of cloud (as a third-party facility) and the overall communication and networking settings of IoMT. Security is basically considered a major challenge for wide-spread adoption of cloud technology or IoMT technology (Khan & Pathan, 2018) for mobile- or e-healthcare.

Medical data are often very sensitive and need to be protected maintaining some standard. For instance, to regulate healthcare industry, the US government introduced Health Insurance Portability and Accountability Act (HIPAA) (HIPAA, 2020). This was enacted to set some storage regulations and ensure sensitive medical data privacy to protect individuals covered by health insurance. While some legislated standards can ensure personal data privacy, often new technologies attract people, and when those are tried or tested (for practical implementation), there could be possibilities of violating standard terms. Many healthcare industries are not prepared for the new cyber age (Healthcare Cybersecurity, 2020). Fraud and identity theft in the healthcare sector have been on the exponential rise (Bay, 2015), just like in many other systems that take advantage of IT and cyber technologies today. ABI Research report (Bay, 2015) states that it is evident that the healthcare industry is adopting cloud technologies very swiftly and by the end of 2020, 80% of healthcare data might be stored at the cloud. Hence, in addition to its existing security challenges, healthcare industry has to cope with the security challenges of the cloud. At a minimum, the mobile healthcare industry should comply with HIPAA standards that regulate data privacy for personal healthcare information.

Motivation: There are various studies and predictions about healthcare data in the cloud as a part of IoMT. Global Market Insights Inc.’s report (Healthcare Cloud, 2020) states that the healthcare cloud computing market could surpass USD 55 billion by 2025, globally. However, in recent times, cyber-attacks have increased significantly, while many healthcare systems have not got sufficiently prepared to ensure patients’ data security and privacy. Hence, we consider a remote healthcare setting and tackle the key security issues in compliance with the HIPAA standard in this work.

Novelty and Contributions: The novelty and contribution of this work are as follows:

1. Our mobile healthcare framework ensures end-to-end security and overcomes the flaws in the existing literature.

2. The mobile healthcare framework complies with HIPAA regulations.

3. As far as we have investigated, we are the first to use White-Box Cryptography (WBC) in mobile applications.

4. Again, we are the first to propose a secure mobile healthcare framework using a community cloud and capable of collecting and preserving evidence (in case of security breaches) using the transaction log, counters, forensics method, and cryptographic audit log techniques.

5. We are the first to implement our protocol in real-time using Kotlin language in Android Studio.

6. Formal verification of our mobile healthcare protocol was successful using BAN logic (Burrows et al., 1990), (Abadi et al., 1993), and Scyther tool (Cremers, 2006).

7. Finally, our proposed protocol’s energy consumption, communication, and computation costs are far less than that of the existing protocols.

Structure of the Paper: After this introduction, Section 2 discusses the related works. Section 3 presents our proposed mechanism. Section 4 contains formal verification while Section 5 presents the security analysis. Section 6 presents the threat model. Performance analysis and comparisons are presented in Section 7 and Section 8 concludes the paper with future research direction.

2. Related work

Hu et al. (2010) propose a hybrid PKI (Public Key Infrastructure) based scheme for addressing HIPAA privacy and security regulations. Though this work links itself with HIPAA standard, it is proposed based on smart cards and not applicable for mobile healthcare applications and mobile clouds. Kumar et al. (2012) propose a novel authentication scheme for Wireless Medical Sensor Networks. We found that the scheme is still vulnerable to insider attack and off-line password guessing attack.

Lee et al. (2013) propose an improved mobile-Healthcare emergency system based on extended chaotic maps. The authors claim that their system provides flawless user anonymity and mutual authentication alongside reducing the computation cost. However, their scheme cannot withstand multi-protocol attack or Denial of Service (DoS) attack. Also, it was not implemented for real-time operations as we understand. Li et al. (2013) propose an extended chaotic map and dynamic ID-based user authentication scheme against DoS attacks. But, this scheme also fails to protect itself against multi-protocol attack and is not for real-time operations. Though claim is made, clarity is missing in the work about how it overcomes the permanent DoS attack. Following this direction of work, 2015] propose a new three-party authenticated key agreement scheme based on chaotic maps that can work without passwords. Proposed scheme also offers thorough privacy protection to the users, so the user forgery attack can cause no damage. However, the same issues like lack of protection against multi-protocol attack, DoS attack, and absence of implementation aspect for real-time setting show its weaknesses. In addition to these issues, all these schemes in this line do not follow any specific standard.

He et al. (2015) present a lightweight authentication scheme for healthcare applications using symmetric algorithms and hash functions. The possibilities of off-line guessing attack, user impersonation attack, and sensor node capture attack still remain for this work due to its inherently weak mechanism. The work presented by Wu et al. (2017) has a fatal flaw that the user is able to communicate with the sensor directly at the end of the authentication process. This makes it more vulnerable to various attacks while the work by Li et al. (2016) cannot handle impersonation, off-line password guessing, and sensor node capture attacks.

Wazid et al. (2016) identify some challenges in the field of security protocols for mobile healthcare systems. The argument is that those challenges must be taken into consideration in order to ensure any secure, robust, and cost-effective solution. Alkeem et al. (2017) propose a healthcare system using cloud of things that combines various security concepts of both healthcare system and cloud computing. The authors claim that their approach ensures various security properties including non-repudiation. However, from the description of the mechanism, it is not clear how the non-repudiation and accountability are ensured. In fact, after a careful analysis, it can be noticed that there is no real end-to-end security ensured, anonymity of the patient is not ensured, there is no audit process, and there is no clarity about where the client’s credentials are stored.

A Multi-factor user authentication scheme for IoT-based healthcare services is proposed by Dhillon and Kalra (2018). They basically propose an Elliptic Curve Cryptography (ECC)-based authentication protocol that ensures real-time remote patient monitoring and tracking based on cloud-IoT setting. This protocol allows the medical professionals real-time access to patient’s data and to take actions accordingly. Again, Sharma and Kalra (2019) propose healthcare service that uses a lightweight user authentication scheme in a Cloud-IoT setting. Their work's main contribution is that legitimate users can get real-time access to remote patient’s sensor data that would be stored on some cloud server. However, examining the work, we find that it does not talk about cloud data security - they rely on some public cloud setting which is a real drawback. Also, there is no clear information how non-repudiation and accountability are ensured, the scheme does not ensure end-to-end security, there is no auditing process of cloud data, and like some other approaches, there is no clear information about the storage of client’s and cloud’s credentials (i.e. sensitive data). Tewari and Gupta (2020) propose a simple and lightweight mutual authentication protocol for healthcare systems ensuring location privacy with low computation and storage capabilities, but this recent work also does not ensure end-to-end security.

Motivated by these works, we find no proposal so far available that ensures the HIPAA standard for mobile healthcare in an IoMT setting, which could help COVID-19 or similar other pandemic situations when patients would need such care while maintaining security and privacy of data. We name our mechanism, Security and Privacy-aware Mobile Healthcare Framework (SPMHF). Following sections describe it alongside necessary analysis and results.

3. Our proposed mobile healthcare system – SPMHF

This section describes the entire ecosystem of our framework. Following are the major entities involved:

• Body Area Sensor Network (BSN). Here is the Sensor (S).

• Healthcare Application in BSN.

• Universal Integrated Circuit Card (UICC) in Smartphone.

• Healthcare Application in UICC.

• Central Healthcare Authority (CHA).

• Certifying Authority Cloud (CAC).

• Doctor (D).

• Patient (P) and Family (individuals).

• Community Cloud for Healthcare (CCH).

As reported in various reliable sources from the medical community, COVID-19 patients can show various types of symptoms like fever, cough, muscle pain, sore throat, shortness of breath, etc. (Symptoms, 2020). Due to the nature of the disease, it is classified as highly contagious. In such case or similar disease condition, when a patient needs emergency treatment or in the ICU (Intensive Care Unit), various types of bodily conditions need to be measured like low oxygen level in blood or hypoxia, high temperature, irregular pulse or heart rate, and so on (Wei-Hass, 2020), (Cardiac, 2020). A key requirement is as less physical contact with the patient as possible. Here, BSN could be very useful. Indeed, today there are various types of body sensors to automatically monitor body temperature, oxygen saturation, blood pressure, pulse rate, etc. (Khan & Pathan, 2018), (Zhang et al., 2020).

In our setting (see Figure 1), the BSN contains a Secure Element (SE), SE contains a healthcare application which collects the health information (e.g. heart rate, temperature). This BSN healthcare application shares a symmetric key with the Mobile Healthcare Application (MHA) in UICC (Ahamad et al., 2014) of the patient’s smartphone. Again, this MHA and CCH share symmetric key between them. Both the Patient (P) and Doctor (D) possess mobile phones with UICCs as SEs and they communicate using 4G/5G through Mobile Network Operator (MNO). The MNO also enables Over-The-Air (OTA) connectivity. CCH provides healthcare services to the patients by bringing all hospitals or medical centres in the same cloud. The country's central government would manage CCH and it hosts a Trusted Platform Module (TPM) of all the hospitals (the respective hospitals personalise TPM).

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

CCH and patients are connected via 4G/5G ensuring communication security using Transport Layer Security (TLS) protocol. Application security is ensured using AES (Advanced Encryption Standard) and ECDSA (Elliptic Curve Digital Signature Algorithm). Certifying Authority (CA) serves as a Trusted Service Manager (TSM) (Ahamad & Pathan, 2019) in addition to its usual functions. Community Cloud here is controlled and shared by multiple organisations. Several owners can have some common interest and hence, it could be managed by a committee of owners or a third party – even can be located at a distant place. The legitimate members of the community would be given access to the data in the cloud. Wireless Public Key Infrastructure (WPKI) is implemented in this framework. Healthcare applications in BSN and UICC are personalised by the CCH using OTA. CCH updates the firmware in the SE of BSN and MNO updates the firmware in the UICC.

One of the most critical attacks against MHA is repackaging attack (Chen et al., 2018) where an attacker with malicious intent alters an application distributed in the market and then redistributes it. In order to overcome the repackaging attacks on MHA from the get-go, our framework implements the following countermeasures:

1. Self-Signing Restriction: This is a countermeasure against repackaging attacks. MHAs should be signed by both CA and CHA.

2. Code Obfuscation: By obstructing analysis, it can prevent disclosure of logic or code (i.e. less chance of reverse engineering). SPMHF adopts logic obfuscation such as control obfuscation.

3. Code Attestation: TPM and UICC are hardware-based platform security solutions in SPMHF. TPM ensures secure booting process from boot loader to the kernel of OS (Operating System) and loading of library modules. Platform integrity is checked remotely by privileged isolation between applications along with remote attestation. Thus, any forgery of data (exchanged between CCH and patient's application) can be detected.

3.1. Certifying authority cloud (CAC)

CA has a cloud with usual functions like issuing certificates, providing directory services, Online Certificate Status Protocol (OCSP), and Certificate Revocation List (CRL).

Registration Authority (RA): CA infrastructure contains this authority for checking the credentials of patients.

Signing Services and Certificate Repository (SSCR): This entity is responsible for generating and signing the certificates. It also maintains the certificates in the Certificate Repository. Different types of certificates are issued which includes X.509, Short Lived Certificates and Lightweight Certificates. CA generates digital signatures in TPM of the CA. TPM is considered a Secure Signature Creation Device (SSCD); hence, CA's digital signatures are considered Qualified Electronic Signatures (QES).

OCSP: OCSP maintains X.509 certificates; this entity helps verify certificate validity.

TSA: Time Stamping Authority is for timestamping services.

CRL: It maintains the list of revoked certificates.

3.2. Central healthcare authority (CHA)

This entity monitors the functions of the hospitals. It also ensures the implementation of HIPAA in hospitals. CHA and CA employ Trusted Party Auditor (TPA) for monitoring the functions of CCH. CHA acts as an adjudicator and TSM. CCH is a subsidiary of CHA and CHA controls TPA.

3.3. Community cloud for healthcare (CCH)

The following entities are involved in CCH:

Communication Manager (CM): Information about CCH services, standards of communications, and interfaces used for different devices is kept in it. Three data interoperability methodologies are HL7 (Health Level Seven) (https://www.hl7.org/), DICOM (Digital Imaging and Communications in Medicine) (https://www.dicomstandard.org/), and IHE (Integrated the Healthcare Enterprise) (Bhatia & Ibrahim, 2020). HL7 and DICOM are the standards applied for data transmission among CCH, hospitals and CHA. For encrypted communication, IPSec VPN (Internet Protocol Security Virtual Private Network) is placed at the forefront of medical gateways. To engage in HTTPS (Hypertext Transfer Protocol Secure) communication, SSL (Secure Sockets Layer) protocol is applied for servers at the medical gateways (for web servers).

TPA: This entity is employed by TSM (i.e. CA) and CHA in our framework which monitors the functions of CCH.

WPKI Manager: This is responsible for the lifecycle of stakeholder’s certificates, and it takes care of the certificate status and directly contacts with the CA. This entity closely works with PM (Personalisation Manager) and CA.

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, and so on can be recorded using logs. The items in a log can be:

• User IDs (identities).

• Exact timestamp (date-time) for logging in and logging off.

• Device location that uses the LAN (Local Area Network), ID of access point, or ID of remote-access system.

The hospital TPM contains:

1. Identity and Access Management (IAM): This entity authenticates IoT devices, IoT Medical Applications (IMA) and Doctor (D) credentials which are issued by TSM, i.e. CA and issues a token which is used to carry out transactions.

2. Time Stamping Authority (TSA): It offers timestamping services for CCH generated messages.

3. Personalisation Manager (PM): PM is responsible for provisioning and personalising of the IoT device, IMA, and UICC of the doctor. UICC is the SE in doctor’s smartphone.

4. Evidence Manager (EM): It collects evidences using various audit log techniques. When any dispute arises among the stakeholders, this entity can provide proofs to the court of law. Once ECDSA is signed, it can prove that data is valid – by matching confirmation data with log data, timestamps, nonce, and old certificates. It also collects evidence from LMCM. TPA finds evidence in TPM of CCH. TPA audits the logs of TPM and detects tampering with the logs.

5. Patch Management and System Hardening: Applications and OSs are often targeted by various types of attacks on a daily basis. Effective “Patch Management” can successfully reduce the risk of compromising systems. System hardening process ensures relatively less attack surface of various types of networking devices and applications. As part of this task, system administrators can close specific network ports, enable or disable some services, use minimal software, etc. If a server runs a huge number of functions, it would be more prone to cyber-attacks and then, system hardening would be also more difficult. To facilitate system hardening, in our approach, we do whatever is required based on the requirements set for the system complying with the standard chosen before implementation of the system. After talking about various entities and aspects of our system, we describe here the health monitoring mechanism.

3.4. Doctor registration phase

Doctor submits his/her credentials to the hospital after being appointed as an employee of the hospital and hospital staff checks his/her credentials (such as National Identity). Hospital acts as an RA and starts the procedure of getting X.509 certificate from CA, hospital gets his/her credentials, takes his signature on the document, then allows to download key pair application on the UICC of the mobile phone. The doctor generates key pairs and then, CA maps the credentials. The public key will be in the repository of the CA. Hospital TPM customises the MHA in the UICC of doctor; it updates the software and firmware. A symmetric key $(S{K}_{HD})$ is agreed upon between the MHA of the doctor and hospital TPM in the CCH.

3.5. Customisation of sensor (BSN) phase

Hospital gets/buys sensors from the manufacturer containing an SE and MHA for recording different body parameters. The hospital records the sensor’s identity, date of manufacturing in its database and installs MHA in the SE of sensor. This MHA only supports symmetric encryption to consume fewer resources.

3.6. Healthcare data upload phase

A patient visits the hospital for some health issues (with symptoms of COVID-19 or any other disease), hospital staff checks his/her credentials, performs preliminary health checkups, and allocates a doctor. Doctor checks and prescribes treatment $(P{R}_D)$ and uploads the treatment data to the hospital database which is in the CCH. If the patient needs sensors to be embedded on/in the body (after getting admitted to ICU or so), doctor instructs the staff to allocate and embed sensors on/in the patient’s body. Doctor (D): $D\to H:\{I{D}_D,T_D,N_D,I{D}_P,P{R}_D,H(P{R}_D)\}S{K}_{HD}$.

3.7. Customisation of patient’s secure element phase

This is exactly similar to how the doctor generates key pairs and CA maps the credentials as described in subsection 3.4. Instead of doctor, this is for the patient’s credentials.

3.8. Customisation of MHA Phase

Here are the steps for this phase:

• Hospital Staff allocates sensors to the patient, maps sensor identity with patient identity and public key of the patient.

• Hospital TPM customises the MHA in the UICC. It updates the software and firmware. A symmetric key is agreed upon between the MHA and Hospital TPM in the CCH.

• A symmetric key is agreed upon between the MHA of sensors and MHA in the UICC.

3.9. Health monitoring mechanism

Figure 2 shows the steps involved in health monitoring mechanism while Table 1 elaborates the major notations used in the paper.

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

Step 1: The BSN (S) starts collecting the data from the patient and sends it to the UICC of the smartphone of the patient (P) every one minute via Bluetooth; the data transmitted to the UICC is encrypted with the symmetric encryption key shared between MHA of BSN (S) and MHA in UICC (P). $SP:\{I{D}_P,I{D}_S,T_S,N_S,LO{C}_P,PD\}S{K}_{PS}$

Step 2: MHA in UICC (P) decrypts the message and forwards the message to the TPM of the hospital (H) in CCH. $PH:\{I{D}_P,I{D}_H,T_P,N_P,LO{C}_P,PD\}S{K}_{PH}$ Step 3: If the readings are within the limits, Hospital (H) updates the database or if there is any deviation, it sends the message to the doctor (D) and patient’s family members. Hospital (H) sends an ambulance to the patient’s location. It also informs to the family members in case of emergency. $HD:\{I{D}_P,I{D}_H,T_H,N_H,LO{C}_P,PD\}S{K}_{HD}$ Symmetric keys are generated each time using hashing algorithms with one-bit cyclic shift of a master secret as described in (Kungpisdan et al., 2003). The key set $S{K}_{AB}$ (with {1, 2, 3, … n}) is generated from the secret key, $S{K}_{AB}$. The symmetric key shared between two parties, A and B generates session keys for each session and hence, session keys will be different for different sessions. In our case, symmetric secret key is shared between the MHA of SE in the smartphone and MHA of Hospital TPM. This system uses White Box Cryptography (WBC) (Beunardeau et al., 2016) which enables secure storage of secret keys and session keys in the MHA. The hospital TPM updates the keys in the MHA of SE in the smartphone. CCH stores patients’ data in the ciphertext, and hospital searches and retrieves patient data using the scheme proposed in (Xiao et al., 2020). CCH ensures patient data privacy using the scheme proposed by (Chang & Wu, 2019).

4. Formal verification using BAN logic and scyther tool

4.1. BAN logic based formal verification

Using BAN logic, we have formally verified our protocol.

1. Assumptions

   • (a) Secrets and Keys: “X” is a set of entities having {S, P, H and D}. CA issues certificates to all the entities involved and all the entities have their keys (AS1, AS2).

   • AS1. CA believes $(\mathrm{\forall }S\in \{\mathit{S},\mathit{P},\mathit{H}\mathit{a}\mathit{n}\mathit{d}\mathit{D}\}\underset{\mapsto }{K_X}X)$

   • CA believes all stakeholders own their public keys.

   • AS2. $X\in \{\mathbf{\text{ S}},\mathbf{\text{ P}},\mathbf{\text{ H}}\mathbf{\text{ and}}\mathbf{\text{ D}}\}$ X believes $\underset{\mapsto }{K_{CA}}CA)$. All system entities possess the public key and X.509 certificate of CA.

   • (b) Freshness:

     • AS3. G believes freshness $N_S$, if G sees quantity $N_S$ in a message, then G considers that as a replay message.

     • AS4. H believes freshness $N_P$, if H sees quantity $N_P$ in a message, then H considers that as a replay message.

     • AS5. D believes freshness $N_H$, if D sees quantity $N_H$ in a message, then D considers that as a replay message.

   • (c) Timeliness:

     • All entities involved believe that the nonce generated by them are unique and fresh.

     • AS6. $T_S$ is timestamp generated by S ensuring timeliness.

     • AS7. $T_P$ is timestamp generated by P ensuring timeliness.

     • AS8. $T_H$ is timestamp generated by H ensuring timeliness.

   • d) Assumptions about trust:

     • These assumptions are about the trust levels of all entities.

     • AS9. (∀X, Q ∈ {S, P, H and D}, X believes CA controls $\underset{\mapsto }{K_{CA}}Q$. CA is trusted by all entities.

     • AS10. ∀ belief Y, CA believes (TPM controls (H believes Y)). CA trusts CCH that Hospital TPM to relay CCH’s beliefs.

2. BAN Logic Based Verification

Step 1: P decrypts: $\{I{D}_P,I{D}_S,T_S,N_S,LO{C}_P,PD\}S{K}_{PS}$ from the assumptions AS1, AS2, AS5, AS6, & AS7. (1) $\begin{array}{r}\mathbf{\text{P believes}}:\{I{D}_P,I{D}_S,T_S,N_S,LO{C}_P,PD\}S{K}_{PS}\end{array}$(1)

P verifies public key of S (AS7) got from S that includes,

1. Verifying the public key of the certificate from the CA.

2. Validating the lifetime of “S” certificate.

3. Verifying the “S” Certificate from CRL.

4. If certificate verification is successful, then, (2) $\begin{array}{rl}& \mathbf{\text{P believes}}S\mathbf{\text{ said}}:\{I{D}_P,I{D}_S,T_S,N_S,LO{C}_P,PD\}S{K}_{PS}\end{array}$(2) (3) $\begin{array}{rl}& P\text{believes fresh}{T}_S\text{from}\mathbf{\text{ AS3}}\end{array}$(3) (4) $\begin{array}{rl}& P\text{believes fresh}{N}_S{\text{N}}_{\text{S}}\text{from}\mathbf{\text{ AS4}}\end{array}$(4)

So, from the statements (1) to (4),

P believes: $\{I{D}_P,I{D}_S,T_S,N_S,LO{C}_P,PD\}S{K}_{PS}$

Step 2: $PH:\{I{D}_P,I{D}_H,T_P,N_P,LO{C}_P,PD\}S{K}_{PH}$

H decrypts $PH:\{I{D}_P,I{D}_H,T_P,N_P,LO{C}_P,PD\}S{K}_{PH}$ $\{\mathbf{\text{I}}{\mathbf{\text{D}}}_{\mathbf{\text{P}}},\mathbf{\text{I}}{\mathbf{\text{D}}}_{\mathbf{\text{G}}},{\mathbf{\text{T}}}_{\mathbf{\text{G}}},{\mathbf{\text{N}}}_{\mathbf{\text{G}}},\mathbf{\text{Reading}},{\mathbf{\text{LOC}}}_{\mathbf{\text{ P}}}\}{\mathbf{\text{SK}}}_{\mathbf{\text{ GH}}}$ from the assumptions, AS1, AS2, AS5, AS6, & AS7.

H believes (5) $\{I{D}_P,I{D}_H,T_P,N_P,LO{C}_P,PD\}S{K}_{PH}\{\mathbf{\text{I}}{\mathbf{\text{D}}}_{\mathbf{\text{P}}},\mathbf{\text{I}}{\mathbf{\text{D}}}_{\mathbf{\text{G}}},{\mathbf{\text{T}}}_{\mathbf{\text{G}}},{\mathbf{\text{N}}}_{\mathbf{\text{G}}},\mathbf{\text{Reading}},\mathbf{\text{LO}}{\mathbf{\text{C}}}_{\mathbf{\text{P}}}\}\mathbf{\text{S}}{\mathbf{\text{K}}}_{\mathbf{\text{GH}}}$(5)

H verifies public key of S (AS7) got from S that includes,

1. Verifies the public key

2. Validating the lifetime of “P” certificate

3. Verifying the “P” Certificate from CRL

4. If certificate verification is successful, then

H believes P said: (6) $\begin{array}{rl}& \{I{D}_P,I{D}_H,T_P,N_P,LO{C}_P,PD\}S{K}_{PH}\end{array}$(6) (7) $\begin{array}{rl}& \text{H }\mathbf{\text{believes}}\mathbf{\text{fresh}}{T}_P{\text{T}}_{\text{G}}\text{from}\mathbf{\text{AS3}}\end{array}$(7) (8) $\begin{array}{rl}& \text{H}\mathbf{\text{believes fresh}}{N}_P{\text{N}}_{\text{G}}\text{from}\mathbf{\text{AS4}}\end{array}$(8)

So, from the statements (5) to (8),

H believes $\{I{D}_P,I{D}_H,T_P,N_P,LO{C}_P,PD\}S{K}_{PH}$

Step 3: $HD:\{I{D}_P,I{D}_H,T_H,N_H,LO{C}_P,PD\}S{K}_{HD}$

D decrypts the received $\{I{D}_P,I{D}_H,T_H,N_H,LO{C}_P,PD\}S{K}_{HD}$ $\{\mathbf{\text{I}}{\mathbf{\text{D}}}_{\mathbf{\text{P}}},\mathbf{\text{I}}{\mathbf{\text{D}}}_{\mathbf{\text{G}}},\mathbf{\text{I}}{\mathbf{\text{D}}}_{\mathbf{\text{H}}},{\mathbf{\text{T}}}_{\mathbf{\text{H}}},{\mathbf{\text{N}}}_{\mathbf{\text{H}}},\mathbf{\text{Reading}},\mathbf{\text{LO}}{\mathbf{\text{C}}}_{\mathbf{\text{P}}}\}\mathbf{\text{S}}{\mathbf{\text{K}}}_{\mathbf{\text{HD}}}$ from the assumptions AS1, AS2, AS5, AS6, & AS7. (9) $\begin{array}{r}D\mathbf{\text{believes}}\{I{D}_P,I{D}_H,T_H,N_H,LO{C}_P,PD\}S{K}_{HD}\end{array}$(9)

D verifies public key of H (AS7) got from S that includes,

1. Verifies the public key

2. Validating the lifetime of “H” certificate.

3. Verifying the “H” Certificate from CRL.

4. If certificate verification is successful, then,

D believes H said: (10) $\begin{array}{rl}& \{I{D}_P,I{D}_H,T_H,N_H,LO{C}_P,PD\}S{K}_{HD}\{\mathbf{\text{I}}{\mathbf{\text{D}}}_{\mathbf{\text{P}}},\mathbf{\text{I}}{\mathbf{\text{D}}}_{\mathbf{\text{G}}},\mathbf{\text{I}}{\mathbf{\text{D}}}_{\mathbf{\text{H}}},{\mathbf{\text{T}}}_{\mathbf{\text{H}}},{\mathbf{\text{N}}}_{\mathbf{\text{H}}},\mathbf{\text{Reading}},{\mathbf{\text{LOC}}}_{\mathbf{\text{P}}}\}\mathbf{\text{S}}{\mathbf{\text{K}}}_{\mathbf{\text{HD}}}\end{array}$(10) (11) $\begin{array}{rl}& D\mathbf{\text{believes}}\mathbf{\text{fresh}}{T}_H{\mathbf{\text{T}}}_{\mathbf{\text{H}}}\text{from}\mathbf{\text{AS3}}\end{array}$(11) (12) $\begin{array}{rl}& D\mathbf{\text{believes}}\mathbf{\text{fresh}}{N}_H{\text{N}}_{\text{H}}{\mathbf{\text{N}}}_{\mathbf{\text{H}}}\text{from}\mathbf{\text{AS4}}\end{array}$(12)

So, from the statements (9) to (12), $D\mathbf{\text{believes}}\{I{D}_P,I{D}_H,T_H,N_H,LO{C}_P,PD\}S{K}_{HD}$

4.2. Formal verification of our protocol using scyther tool

There are three types of attacks, first type is about the integrity of the messages exchanged among S, P, H and D, second type of attack is about the authentication of entities involved in the system and third is an attack on the confidentiality of data exchanged among the entities involved in the system. We used the default properties of the Scyther tool (Cremers, 2006). It is a simulation tool used to verify, falsify, and analyse the security properties and is the only tool that can verify multi-protocol attacks. Appendix A presents the code in SPDL (Security Protocol Description Language).

5. Security analysis

This section analyses our proposed protocol’s security, considering the known threats and attacks relevant to such a system. Threat model would consider the relevant cloud and application related issues.

5.1. Key security properties

To ensure authorisation, a patient needs to gain permission to store the data collected from his/her body in order to store it in the CCH. CCH needs to verify whether the patient is registered and authorised to place the messages in the CCH. CCH/Hospital TPM establishes a secure channel with MHA in the UICC using SSL/TLS protocol at the communication layer. Data exchanged between the entities are encrypted using shared symmetric key. Encrypted messages also contain timestamps and nonce which ensure timeliness and uniqueness properties. Hence, confidentiality is ensured. For mutual authentication, MHAs of the patient and doctor are personalised by the CCH i.e. a symmetric key is agreed between “Hospital TPM and patient” and “Hospital TPM and doctor”. This achieves the goal of mutual authentication, the privacy of credentials, and the session key’s security using symmetric key cryptography. The patient’s information is not accessible by any unauthorised entity; the intruder cannot send, capture or read the messages as the messages are encrypted at the application layer and transmitted using SSL/TLS protocol at the communication layer. This ensures integrity of exchanged messages.

To ensure availability, CCH makes sure that it is available to patients all the time. UICC in patent’s mobile phone and SE in BSN continuously send messages to CCH. These two (UICC and SE in BSN) will not keep any message in their memory. Moreover, a secure channel is established between MHA in UICC and CCH using SSL/TLS protocol. To ensure non-repudiation property, we use WPKI Manager which is responsible for the lifecycle of the stakeholder’s certificates. It takes care of the certificate status and directly contacts the CA. This entity closely works with PM and CA. Also, as noted before, digital signatures are generated in SSCD, which are considered QES. SSCD in this framework are SE and TPM.

5.2. Accountability, personalisation of MHA, and session key agreement

Each and every user in the ecosystem is accountable for his/her actions. The shared symmetric key (that is agreed upon between entities) encrypts all messages with Hospital TPM. Therefore, the patient and the doctor are responsible for their transmitted messages. As already noted before, Hospital TPM personalises the MHA in UICC. It updates the software and firmware.

5.3. Key freshness, repackaging attack, and security of keys

As discussed in Section 3, in order to thwart the repackaging attack on MHA, Self-Signing Restriction, Code Obfuscation, and Code Attestation are used. If the symmetric shared key is compromised, CCH would automatically update keys using OTA, thereby ensuring key freshness. In order to implement Signature-Creation Data, SSCD can configure hardware or software or both. The stakeholders in SPMHF generate digital signatures in UICC and hospital TPM so that they are considered as QES.

5.4. Secure key distribution

Patient’s private key is securely stored in UICC; symmetric keys are securely stored in MHA. Each MHA is independent of other applications (applications are protected by firewalls).

5.5. Denial of service attack (DoS)

The patient could withstand request or fake message-based DoS attack (Pathan, 2010) as CCH/Hospital TPM establishes a secure channel with MHA at the communication layer. Application security is also ensured by encrypting the messages using AES algorithm. Hence, fake messages are simply discarded to foil DoS attack.

5.6. Multi-protocol, man-in-the-middle (mitm), and replay attacks

Our protocol overcomes such attack (where multiple protocols are involved) as it has been successfully verified using Scyther tool. It also overcomes Man-In-The-Middle (MITM) attack as data exchanged between the entities are encrypted using shared symmetric key. As with that encryption, timestamps are recorded for all messages, replay attack is not possible to be launched as well.

5.7. Impersonation attack and parallel session attack

An intruder cannot generate a session key. Hence, it cannot decrypt the messages transmitted. Respective entities personalise MHA. If symmetric shared key is compromised, CCH updates the keys OTA automatically; so, key freshness is ensured. Therefore, it could thwart impersonation attack. Again, 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 AES algorithm.

5.8. Auditing

TPA is employed by CA and CHA (both act as TSM). TPA monitors and audits all hospital TPMs in CCH; thereby, ensuring transparency and accountability. In case of dispute among stakeholders, TPA collects evidence from networks, firewalls, and hospital TPM, etc. LMCM performs anomaly detection using statistical and ML algorithms, and identify traffic variances against pre-defined conditions.

5.9. HIPAA compliance

Our framework puts responsibility on the organisations to protect patient’s information. Secrecy of patient’s information is maintained during its rest and during the transit. Hospital TPM keeps patient’s data in encrypted form. The data can be decrypted with the shared symmetric key between hospital TPM and MHA in the patient’s UICC. Here, SSL/TLS protocol ensures the communication security.

5.10. Application security

WPKI Manager takes care of the certificate status and directly contacts with the CA. This entity closely works with PM and CA. In order to ensure non-repudiation property, digital signatures are generated in the SSCD.

5.11. Physically stolen medical sensor attack or node capture attack

If an adversary steals sensor or smartphone, he will not be able to extract patient’s credentials (keys) or health information as the sensor and smartphone do not store patient’s health records (i.e. the SEs and MHAs of both the sensor and smartphone do not contain any of patient’s health information). Moreover, the credentials (keys) stored in SE cannot be captured by the adversary as SE is tamper-resistant. Adversary cannot obtain credentials (keys) from MHA either because, it adopts WBC which resists white-box attacks.

5.12. Resistance against unauthorised key computation

An adversary will not be able to compute symmetric key shared between hospital TPM and sensor or between hospital TPM and gateway as the hospital TPM generates symmetric keys in CCH.

5.13. Resistance against privileged insider attack

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. Hence, the adversary cannot steal patient’s information; hence, the proposed system withstands privileged insider attacks.

5.14. Resistance against stolen verifier attack

Our system is safe against stolen verifier attack as the adversary cannot get any verifier or any relevant information from the SE or MHA of either the sensor or the smartphone as SE is tamper-resistant while MHA adopts WBC as mentioned in subsection 5.11.

5.15. Defense-in-depth

Our framework incorporates security in design at every phase of development and implementation. Trying to add security at the end of development phase can turn out to be very costly. As presented so far, with personalisation of MHA, encryption, secure channel and overall, step by step building process, we ensure defense-in-depth and end-to-end security.

Before presenting the performance analysis, let us talk about the threat modelling used for our approach in the next section.

6. Threat modelling

We have identified and analysed all the potential threats against the proposed system. In order to reduce the risks, the mitigation strategy for each threat has been identified. According to the security and privacy protection requirements in (Gerdes & Fensli, 2015) and countermeasure techniques corresponding to STRIDE (Shostack, 2014), Table 2 suggests a list of countermeasure techniques corresponding to STRIDE, to address the identified threats.

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.

7. Performance analysis, comparisons, and implementation

Comparative data about the costs of computation for login and authentication phases are presented in Table 3. Here, $TH$ denotes the time complexity of computing the one-way hash function while $TS$ stands for the same regarding symmetric encryption/decryption operation.

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

Our performance analysis confirms the efficacy of the proposed scheme. It employs one-way hash and symmetric encryption/decryption operations. These are the relatively low-cost operations in comparison with other cryptographic operations. As presented in (Xu & Wu, 2015), the time complexities (in seconds) are $TH=0.0004$ and $TS=0.1303$ where TH is time taken for hashing and TS is the time taken for encryption/decryption. Clearly, our proposed work shows better performance (see Figure 3).

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

Table 4 compares the energy consumption of our proposed protocol against the other works. To evaluate the energy consumption, cryptographic operations; hash and symmetric key operations are executed. As of (Javan & Bafghi, 2014), the energy consumed to generate encryption/decryption using AES algorithm is (ES): 1.21 Micro Joules/byte and to calculate SHA-1 hash (EH) is 0.76 Micro Joules. Clearly, as shown in the table, our scheme outperforms other alternative schemes based on the same platform (Figure 4).

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.

We have implemented a part of our Mobile Healthcare Application. Our implementation related information and Kotlin code could be found at: https://webmah.com/security/mobile-healthcare.zip

8. Conclusions and future work

SPMHF is designed in compliance with HIPAA standard. Given various practical circumstances of COVID-19 pandemic or any other similar situation that may appear in the future, it is a requirement to ensure appropriate level security and privacy for patient’s data as well as to develop a mechanism of minimum-contact based remote health monitoring of critical-stage patients. Our framework and protocol could be very effective in this case. In a nutshell, our framework ensures confidentiality of the messages exchanged, integrity of the message, audit control, effective patient authentication, access control, data availability, transparency, freshness of health data and the patient’s consent in the process. Overall, the HIPAA standard is strictly maintained and several known attacks could be thwarted with this practical-setting based work. We would like to work on mobile healthcare system’s accountability issues in compliance with HIPAA regulations in the future. Also, we plan to investigate possible adaptation of edge computing framework proposed in (Zhao et al., 2020) in order to overcome the end-to-end delays from cloud computing data centre for medical issue monitoring mobile applications.

Disclosure statement

The authors declare that there is no conflict of interest for this work.

Appendix

SAMPLE SPDL (Security Protocol Description Language) Code

/* SPMHF is based on Wireless PKI, SE, TPM */

const pk: Function;

secret sk: Function;

inverse keys (pk,sk);

usertype Timestamp;

usertype PID, SID,TP, NP, PD,LOCP,TS,NS,HID,TH,NH;

// Protocol description

Protocol SMHMS (S,P,H,D)

{

role S

{

const NS: Nonce;

const SKsp: SessionKey;

const SKph: SessionKey;

/* Authentication and Key Agreement Protocol */

send_1 (S,P, {PID,SID,TS,NS,PD,LOCP}SKsp);

claim_S1 (S, Secret, SKsp);

claim_S2 (S, Secret, NS);

claim_S3 (S, Niagree);

claim_S4 (S, Nisynch);

}

role P

{

const NP: Nonce;

var NS: Nonce;

const SKsp: SessionKey;

const SKph: SessionKey;

read_1 (S,P, {PID,SID,TS,NS,PD,LOCP}SKsp);

send_2 (P,H, {PID,HID,TP,NP,PD,LOCP}SKph);

claim_P1 (P, Secret, SKsp);

claim_P2 (P, Secret, SKph);

claim_P3 (P, Secret, NP);

claim_P4 (P, Niagree);

claim_P5 (P, Nisynch);

}

role H

{

const NH: Nonce;

var NP: Nonce;

var NS: Nonce;

const SKph: SessionKey;

const SKhd: SessionKey;

read_2 (P,H, {PID,HID,TP,NP,PD,LOCP}SKph);

send_3 (H,D, { PID,HID,TP,NP,PD,LOCP}SKhd);

claim_H1 (H, Secret, SKph);

claim_H2 (H, Secret, SKhd);

claim_H3 (H, Secret, NH);

claim_H4 (H, Niagree);

claim_H5 (H, Nisynch);

}

role D

{

var NH: Nonce;

const SKhd: SessionKey;

read_3 (H,D, { PID,HID,TP,NP,PD,LOCP}SKhd);

claim_D1 (D, Secret, SKhd);

claim_D2 (D, Niagree);

claim_D3 (D, Nisynch);

}

}

// With compromised key, an untrusted agent

const e: Agent;

untrusted e;

compromised sk(e);

Key generation technique

A set of shared keys are generated: Xi (shared between client and merchant) where i = 1, . . ., n. We present two possible efficient key generation techniques: one used for generating a set of Xi from the given secret X. The main concept is to apply one hash algorithm with one-bit shift (either left shift or right shift) of a master secret at each time of generating a session key. Both techniques could be shown as follows:

Generating Xi

$X1=h(1-\text{bit-shift}-of-X),X2=h(2-\text{bit-shift}-of-X),\dots ,Xn=h(n-\text{bit-shift}-\text{of}-X)$ To generate a set of Xi, client runs merchant registration protocol to register itself to merchant in order to share the secret X with merchant.