Open AccessArticle

APSec1.0: Innovative Security Protocol Design with Formal Security Analysis for the Artificial Pancreas System

Jiyoon Kim

Jongmin Oh

²,

Daehyeon Son

²,

Hoseok Kwon

²,

Philip Virgil Astillo

and

Ilsun You

^2,*

School of Computer Sciences, Gyeonsang National University, Jinju-si 52828, Republic of Korea

Department of Financial Information Security, Kookmin University, Seoul-si 02707, Republic of Korea

Department of Computer Engineering, University of San Carlos, Cebu City 6000, Philippines

Author to whom correspondence should be addressed.

Sensors 2023, 23(12), 5501; https://doi.org/10.3390/s23125501

Submission received: 30 April 2023 / Revised: 8 June 2023 / Accepted: 9 June 2023 / Published: 11 June 2023

(This article belongs to the Section Internet of Things)

Download

Browse Figures

Versions Notes

Abstract

The Medical Internet-of-Things (MIoT) has developed revolutionary ways of delivering medical care to patients. An example system, showing increasing demand, is the artificial pancreas system that offers convenience and reliable support care to patients with Type 1 Diabetes. Despite the apparent benefits, the system cannot escape potential cyber threats that may worsen a patient’s condition. The security risks need immediate attention to ensure the privacy of the patient and preserve safe functionality. Motivated by this, we proposed a security protocol for the APS environment wherein support to essential security requirements is guaranteed, the security context negotiation is resource-friendly, and the protocol is resilient to emergencies. Accordingly, the security requirements and correctness of the design protocol were formally verified using BAN logic and AVISPA, and proved its feasibility through the emulation of APS in a controlled environment using commercial off-the-shelf devices. Moreover, the results of our performance analysis indicate that the proposed protocol is more efficient than the other existing works and standards.

Keywords:

artificial pancreas system (APS); security protocol; formal verification

1. Introduction

Artificial pancreas system (APS) is a closed-loop insulin injection system, which can be classified as an Implantable Medical Device (IMD). It continuously monitors the glucose level of a patient with Type 1 Diabetes (T1D) and assists them with the insulin injection process. These systems will improve the glycemic control of the patient and reduce the risk of hypoglycemia and hyperglycemia, ultimately enhancing the quality of life of patients, especially those that suffer from T1D and other insulin-dependent conditions [1,2]. Traditional insulin injection requires two steps. First, the patient checks the glucose level through blood drop. After that, the medical attendant manually injects physician-prescribed insulin dosage if the level goes beyond the normal range. Meanwhile, state-of-the-art APS automates these procedures with two Internet-of-Things (IoT) devices and one controller device, also serving as the IoT gateway. One of the IoT devices continuously monitors, at a configured interval, the glucose level and forwards it to the controller. Subsequently, the controller, through its visualization feature, presents the observed level, as well as calculates the appropriate insulin dosage, which is sent as part of the command message to the insulin-injecting IoT device. An exemplary illustration of the APS is shown in Figure 1.

The demand for APS has lately been increasing due to the substantial growth of pancreatic ailment and failure cases. According to a report by IMARC Group, the global device market of APS has reached USD 1,949 million in 2021. The market is expected to reach USD 4,122 million by 2027. This represents a compound annual growth rate (CAGR) of 13.4% during the period from 2022 to 2020 [3]. Market Research Future also projected that in the period between 2022 and 2023, the market will generate sales of USD 341.08 million and an increase in CAGR of 18.0% [4].

With the increasing demand for not only APS but IMDs in general, new security risks also arise that need attention to ensure the privacy of patients and preserve safe functionality. In recent years, several studies have highlighted the vulnerability of IMDs, such as APS, to a variety of security threats [5,6]. The consequences of a successful attack on IMDs can range from device malfunction to life-threatening situations. Just as the previous research indicates, the usage of APS is increasing fast, along with its impact on society. Recently highlighted risks associated with APS include the unauthorized access to the devices from attacker, intercepting sensitive medical data, and even taking control of the devices themselves.

Although APS has apparently transformed classical medical care practices to be more convenient, living with elevated effectiveness for maintaining glucose to normal level, there are still several key issues in terms of cybersecurity that needs immediate resolution [7,8].

The basic structure of APS is composed of three resource-constrained devices, which communicate with each other wirelessly at certain intervals. Hence, considering the nature of such an environment, suitable secure communication protocol with low energy consumption is vital. Accordingly, these devices can authenticate, verify, and securely exchange message with each other. With such a motive, this paper has examined existing protocols for IMDs and IoT devices. For example, Bluetooth is the most widely adopted protocol in IoT ecosystem. However, its security level is not suitable for deployment in IMDs, especially in APS. Other existing protocols also had their own drawbacks if employed in the APS environment, and, more importantly, all of them are not resilient in case of emergency situations. Thus, this paper proposes a security protocol, dedicated to the APS, while considering the three vital criteria, being secure, lightweight, and resilient. In addition, the proposed protocol is also aligned with the security considerations from guidance documents for medical device of the US Food and Drug Administration (FDA) [9,10].

The main contributions of this paper are summarized as follows:

Designing an innovative security protocol to establish tripartite authentication and construct a secure channel between the involved devices of the APS.
Formally verifying satisfaction with vital security services as well as the correctness of the proposed protocol.
Comparing the protocol with existing IoT-intended protocol and well-known security standards in terms of security requirements, computation, and communication overheads.
Demonstrating the feasibility of the protocol through emulation in a controlled environment using commercial off-the-shelf devices.

The rest of the paper is organized as follows. Section 2 discusses an overview of an IMD system. Section 3 describes the proposed protocol. Section 4 presents the formal security analysis and results from BAN logic and AVISPA. Section 5 presents the experimental environment and implementation. Finally, Section 6 concludes the paper.

2. Related Works

Insulin is an important hormone that regulates blood glucose levels in the body. However, for individuals with insulin receptor deficiency, insulin resistance, or insulin secretion deficiency, insulin injections are necessary. It is one of the most common treatments for diabetes; however, insulin injections can be inconvenient in daily life. Patients must inject themselves at regular intervals and continuously monitor their blood sugar levels and insulin doses. This can be a significant source of stress for many diabetes patients.

Recently, the concept of an APS [11,12] has emerged as a solution to these problems. APS is a device that automatically performs continuous blood glucose monitoring and insulin administration. This replaces the role of the pancreas in secreting insulin to regulate blood glucose levels. APS enhances the convenience and safety of daily life of blood glucose control in diabetic patients by automating the process. In addition, it improves the accuracy of blood glucose regulation, reducing the incidence of complications associated with diabetes.

However, there are also several challenges associated with the development and implementation of an APS. One of the most critical issues is ensuring the security and privacy of patient information. Since APS uses sensitive personal information, such as medical records and blood glucose levels, it is essential to establish robust information security protocols to prevent unauthorized access, data breaches, and cyberattacks. Therefore, information security measures (e.g., security protocol) should be designed to ensure that patient data are protected and that patients can use APS with confidence.

Unfortunately, it is difficult to find significant existing research on security protocols specifically designed for APS. Instead, we expand our scope and review existing research on security protocols for IMD. The following existing studies on IMD-based security protocols were proposed in similar environments to APS. However, it is difficult to say that they fully support APS due to the various differences between APS and IMD, such as requirements, structure, device, and performance.

Wu et al.’s protocol [13] is a novel fine-grained IMD access control scheme based on a proxy device, such as the patient’s smartphone, which will delegate the heavy access control computations for the IMDs. The communications between the proxy and the IMD programmer are conducted through an audio cable to mitigate potential wireless attacks. The ciphertext-policy attribute-based encryption (CP-ABE) is employed to enforce fine-grained access control over the qualifications of the programmer operator. The IMD holds a unique identifier and master key, used only in the initial pairing process with the proxy. All operators with Public Key Infrastructure (PKI) parameters used in CP-ABE must first be registered with the Central Health Authority (CHA), which creates and manages secret keys used in communication. The operator obtains information by inputting or reading through the smart card and communicates with other devices using the programmer. The proxy connects with the programmer to control access to the IMD. In spite of this protocol’s novelty, its need for an audio cable connection between the proxy and the IMD programmer may be inconvenient or impractical in certain situations. Moreover, compared to traditional PKI algorithms, CP-ABE results in relatively excessive computation overhead while not widely being applied.

Chi et al.’s protocol [14] e-SAFE aims to provide secure, efficient, and forensics-enabled access to IMDs. The system uses a smartphone as a proxy to undertake most of the security-related tasks and establishes a trusted channel between the IMD and the smartphone by sharing a secret key derived from a master key that is physically inaccessible to attackers. The doctor responsible for all operations on the patient’s IMDs is authenticated, and access privileges are authorized through widely used SMS/email services. Furthermore, this protocol uses a compression-based encryption mechanism, PKI, and other cryptographic protocols. The IMD connects with the patient’s smartphone via Bluetooth and the programmer of the doctor via the wireless medium. The patient’s smartphone communicates with the IMD via Bluetooth and the programmer of the doctor via wireless. On the one hand, the protocol can provide secure access to IMDs, reducing the risk of malicious attacks. The authentication of doctors and authorization of access privileges ensure that only authorized personnel can access IMDs. The forensics-enabled feature allows for post-event analysis in case of any security breaches. On the other hand, using SMS/email services for authorization may not be secure enough for some users.

The HAT protocol [15] is a solution that provides fine-grained and dynamic access control for the next generation of IMDs while offering full control and transparency to the patient. This protocol can provide a secure key exchange that relies on a hash-based access token between personal devices and the IMD. The protocol involves three parties, the IMD, the patient’s personal device, and a security manager. The security manager is an external device under the patient’s control that issues access tokens to securely establish session keys between personal devices and the IMD. The security manager role can be assigned to a new external device at any time, revoking the former security manager. This protocol ensures that only authorized devices can communicate with an IMD, providing fine-grained and dynamic access control for patients while maintaining their privacy and security. The advantage of this protocol is that it allows for easy initialization or connection of new devices, and multiple personal devices can communicate with IMD simultaneously.

HAT exchanges session key between IMD and personal device through Elliptic Curve Diffie–Hellman Ephemeral (ECDHE) under the supervision of a security manager. Subsequently, the security manager is excluded from communication, and IMD and personal device communicate directly. However, in the APS environment, there are two medical devices (CGM, Insulin Pump) that need to be connected to the patient’s personal device (Controller). At the same time, an emergency phase is required to protect the patient from accidental incidents when the Controller becomes inoperable. HAT is not entirely suitable for the requirements of APS presented in Section 3.

The Bluetooth LE (BLE) protocol [16] is one of the low-power communication technologies designed for wireless devices. It enables low-power communication between devices, characterized by very low power consumption and short transmission distances. This allows for long operation times with small batteries. Additionally, it provides faster connection speeds and a larger range than the traditional Bluetooth protocol while reducing costs by using inexpensive wireless modules. However, considering to apply it for the APS, there are some disadvantages, such as two-party protocol, low data transfer rates and limited processing capabilities, complex implementation processes, and a lack of compatibility with the traditional Bluetooth protocol. More importantly, its key exchange protocol is not authenticated, thus being vulnerable to Man-in-The-Middle (MiTM) attacks.

The TLS 1.3 protocol [17,18] offers higher security than previous versions, reduces connection setup time, and enhances privacy protection. It addresses security flaws and vulnerabilities in earlier versions and improves resilience to new attack techniques. Additionally, the handshake process has been improved to speed up session establishment, and various features have been added to enhance privacy protection. However, despite its popularity and advanced architecture, it is relatively complex, a two-party protocol, and requires heavy computation overhead, which is thus clearly not proper for the APS.

3. Proposed Protocol

APS can relieve the inconvenience for patients who have to manage their health conditions due to various diseases continuously. For example, insulin pumps are used for patients who require multiple insulin injections, such as Type 1 Diabetes and gestational diabetes. Conventional insulin injection therapy is a method that can control a patient’s blood sugar effectively. Still, it is accompanied by the inconvenience (pain, fear, etc.) of an injection needle for each administration. Insulin pumps can relieve not only the inconvenience of insulin injection therapy but also prevent missed or misuse of medications.

Meanwhile, APS collects the patient’s condition to provide various functions to the patient and repeats the process of injecting medicine based on this. In other words, APS can collect and judge sensitive information, such as the patient’s health status. Such sensitive information and the operation of devices based on it can become a target for malicious attackers to damage users’ financial and physical values. Therefore, the communication of the APS device must be sufficiently protected from malicious attackers. In this chapter, we design a security protocol that supports authentication and key negotiation to protect patient-sensitive information from malicious attackers in communication between APS devices. The terms used in this paper and their meanings are shown in Table 1.

Before delving into designing security protocols, it is necessary to analyze the target environment and define security requirements and assumptions. A description of the target environment is provided in the Introduction, and in this chapter we define security requirements and assumptions and design security protocols.

3.1. Security Requirement

Security requirements refer to the demands that an organization or system must fulfill to operate securely and to protect the information, assets, and users’ personal data. While there can be various forms of security requirements, defining appropriate security requirements is desirable. Therefore, the process of deriving security requirements through the analysis of the target environment is crucial in designing security protocols.

APS is a medical device that delivers insulin automatically to diabetes patients. Therefore, to protect the patient’s health and privacy, it is important to design the system with security as the top priority. The following are some of the security requirements for APS:

Mutual Authentication. Mutual authentication plays a crucial role in establishing a trusted relationship by verifying and confirming the trustworthiness of each other. Through mutual authentication, it is possible to verify the trustworthiness of communication counterparts and set up access controls for security and privacy protection. Since the APS environment deals with sensitive data such as patient health information, it is necessary to provide access control through mutual authentication to protect it. Mutual authentication can be implemented using various methods, such as encryption, digital signatures, certificates, tokens, and other mechanisms.

Confidentiality and Integrity. Confidentiality and integrity are two key principles of information security. Confidentiality refers to the protection of sensitive information so that it is only accessible to authorized users or systems. In other words, sensitive information should be disclosed only to users with appropriate permissions. Integrity means that information remains unchanged and in its original state, as authorized by users or systems. APS that transmits sensitive information, such as users’ health information, should protect the information from unauthorized alteration or damage through confidentiality and integrity. Confidentiality and integrity are complementary principles in information security. Therefore, a comprehensive information security strategy should consider both confidentiality and integrity and implement them rigorously to ensure the security of information.

Secure Key Exchange. Secure key exchange is an important concept in computer security and cryptography, used to establish shared secret keys for secure encrypted communication. A key exchange is the process of exchanging confidential information between two entities to generate shared secret keys for use in communication. There are various methods for key exchange, and the choice of method should be based on the requirements of the communication system and security policies. Secure key exchange is a critical step in ensuring the confidentiality, integrity, authentication, and other security properties of communication and should be carefully selected and implemented.

Perfect Forward Secrecy Perfect Forward Secrecy (PFS) is a property of cryptographic protocols that ensures that if an attacker manages to obtain the secret key of a particular session, they will not be able to use it to decrypt past or future sessions. In other words, PFS ensures that the secrecy of past and future communications remains intact even if the secret key of a particular session is compromised. PFS is typically achieved through the use of temporary session keys that are generated for each session and are not derived from a long-term secret key. These session keys are used to encrypt and decrypt data for the duration of the session, and they are discarded once the session is completed. As a result, even if an attacker manages to obtain the session key for a particular session, they will not be able to use it to decrypt any past or future sessions.

Privacy. Privacy protection refers to the safeguarding of an individual’s personal information and activities. It involves various means and methods to ensure that personal information is not collected, used, or disclosed without authorization. Privacy protection respects the rights and freedoms of individuals and includes principles and technologies for appropriately handling and securing personal information. This can be achieved through techniques and procedures, such as secure processing of personal information, encryption, access controls, user consent, and data integrity. Privacy protection aims to enhance trust and security in handling personal information while respecting and safeguarding an individual’s privacy. In an APS environment, security protocols that ensure privacy can safeguard against attacks involving the recognition, identification, or tracking of the user’s APS device by potential attackers.

Emergency Phase. APS is a critical system that directly impacts the health of patients, and it should be prepared for various disruptions caused by different factors. The proposed protocol is designed to exchange emergency session keys to overcome certain disruptions caused by control device failures in emergency situations.

3.2. Assumptions

Assumptions refer to the essential elements that should be considered for a security protocol to meet the security requirements in the target environment. The assumptions for the proposed protocol are as follows:

The security protocol proposed in this paper is designed based on the APS.
The security protocol proposed in this paper is the communication of three participants, CGM, Controller (CONT), and Insulin Pump (IP).
The protocol proposed in this paper communicates through an open wireless channel.
CGM and IP share their passcode safely with CONT.
Emergency situation means a situation where the CONT cannot communicate normally with CGM or IP for any reason.

3.3. Proposed Protocol

The proposed protocol consists of three phases, (1) the registration phase, (2) the communication phase, and (3) the emergency phase. The design of the proposed protocol is shown in Figure 2 and detailed descriptions are below.

3.3.1. Registration Phase

In the first step, CGM and IP must authenticate to establish a secure channel with the controller before transmitting patient information. The Registration phase in Figure 2 shows the certification process between IP and CONT, as well as CGM and CONT. The detailed descriptions of the Registration phase are as follows. Before starting the procedure, CGM and IP share their passcode (

P W D_{C G M}

and

P W D_{I P}

) with CONT through a secure channel. Furthermore, all the communication participants generate ECDH key pairs. In this paper, we assume the ECDHE (ECDH Ephemeral) option that can use ephemeral keys and support perfect forward secrecy. The key generation and exchange process of the ECDHE option is shown in Table 2.

(R1): After sharing passcodes and generating ECDHE key pairs, CGM generates and transmits a random nonce ( $n_{1}$ ) to trigger a connection with CONT.
(R2): Upon receiving the message sent by CGM, CONT sends a response message that includes a session identifier ( $S i d$ ) indicating the current session, the ECDHE public key ( $g^{X}$ ) generated in (R1), a fresh nonce ( $n_{1}$ ) received from CGM, and a newly generated random number ( $n_{2}$ ) is included in the message. The message in this step can be protected by the message authentication code ( $H M_{1}$ ) generated using CGM’s passcode ( $P W D_{C G M}$ ) by computing $H M_{1} = H M A C (P W D_{C G M}, S i d | | g^{X} | | n_{1} | | n_{2})$ .
(R3): CGM first checks HM1 in the message the CONT sends and, if valid, creates a new random number ( $n 3$ ). After that, CGM calculates the ECDHE secret key ( $g^{X} Y$ ) using the CONT’s ECDHE public key ( $g^{X}$ ) and its own ECDHE private key (Y). Furthermore, the session key ( $S K_{C G M}$ ) will be calculated with the ECDHE secret key ( $g^{X Y}$ ) and random numbers ( $n_{2}$ and $n_{3}$ ) of CGM and CONT. To protect the messages in this step, CGM includes message authentication codes ( $H M_{2}$ and $H M_{3}$ ) in the outgoing message, which are protected by $S K_{C G M}$ and $P W D_{C G M}$ , respectively. Upon receiving this, CONT checks $H M_{3}$ first, and if it is valid, it calculates the ECDHE session key ( $g^{X Y}$ ) by combining the CGM’s ECDHE public key ( $g^{Y}$ ) and random numbers. Finally, $H M_{2}$ is checked with the ECDHE session key to verify that the same key was exchanged securely with the CGM. $H M_{2}$ and $H M_{3}$ is calculated as $H M_{2} = H M A C (S K_{C G M}, S i d | | g^{Y} | | n_{2} | | n_{3})$ , $H M_{3} = H M A C (P W D_{C G M}, S i d | | g^{Y} | | n_{2} | | n_{3} | | H M_{2})$ , separately.
(R4)–(R6): In steps (R4) to (R6), steps (R1) to (R3) described above are equally performed between the IP and the CONT. Through steps (R4) to (R6), IP and CONT satisfy mutual authentication and securely exchange the ECDHE session key ( $g^{Y Z}$ ). The message authentication codes $H M_{4}$ , $H M 5$ , and $H M_{6}$ are calculated as $H M_{4} = H M A C (P W D_{I P}, S i d | | g^{X} | | n_{4} | | n_{5})$ , $H M_{5} = H M A C (S K_{I P}, S i d | | g^{Z} | | n_{5} | | n_{6})$ , $H M_{6} = H M A C (P W D_{I P}, S i d | | g^{Z} | | n_{5} | | n_{6} | | H M_{5})$ , separately.
(R7): When the CONT completes authentication with CGM and IP, it sends the IP’s ECDHE public key to CGM. The transmission message is protected by the included message authentication code ( $H M_{7}$ ) and the ECDHE Session Key ( $g^{X Y}$ ) between CGM and CONT. $H M_{7}$ is calculated as $H M_{7} = H M A C (S K_{C G M}, S i d | | g^{Z} | | n_{3} | | n_{6})$ .
(R8): Contrary to the above, CONT sends the CGM’s ECDHE public key to IP. The message in this step also is protected by the message authentication code ( $H M_{8}$ ) and the ECDHE Session Key ( $g^{Y Z}$ ) between IP and CONT. $H M_{7}$ is calculated as $H M_{8} = H M A C (S K_{I P}, S i d | | g^{Y} | | n_{3} | | n_{6})$ .

3.3.2. Communication Phase

If CGM and IP successfully authenticate with CONT, they can transmit the patient’s medical information through a secure channel. The Communication phase in Figure 2 represents the process of measuring patient information with a medical device and transferring it to a suitable device. In this case, CGM measures the patient’s blood glucose level (BGL), and CONT converts it into appropriate command and dose messages. The converted message directs IP to inject the appropriate insulin into the patient and return the Insulin on Board (IoB) information to CONT.

IoB refers to the amount of active rapid-acting insulin currently present in the user’s body. This is important as rapid-acting insulin can remain active in the body for up to 3–5 h, and maintaining an appropriate level of IoB is crucial for proper blood sugar control. Checking IoB is included in the Communication phase of this paper, along with blood glucose analysis and insulin administration. The detailed procedure of the Communication phase is outlined below.

(C1): If CGM and IP have successfully generated session keys ( $S K_{C G M}$ , $S K_{I P}$ ) with the CONT during the Registration phase, the Communication phase can be initiated. CGM is a device that monitors the user’s blood glucose, and the blood glucose information should be treated as sensitive personal information. Therefore, CGM encrypts the Blood Glucose Level (BGL) using the session key ( $S K_{C G M}$ ) agreed upon with CONT and sends it to CONT.
(C2): Once CONT receives the BGL from CGM, it calculates the appropriate insulin dosage for the user’s blood glucose and generates a command for it. Then, it encrypts the generated command and insulin dosage (CMD, dose) using the session key ( $S K_{I P}$ ) agreed upon with IP and sends it to IP.
(C3): IP administers insulin to the user based on the received command (CMD) and insulin dosage (dose) from the Controller. After administering the insulin, IP generates a message that includes information such as the Insulin on Board (IoB) and the remaining insulin in the device. The message is then encrypted using the session key ( $S K_{I P}$ ) and sent to CONT for reporting.

3.3.3. Emergency Phase

APS is an important device that improves the convenience of patients with diabetes, but it can experience mechanical or communication problems due to various reasons. A malfunction in APS implies not only a device failure but also an immediate health problem for the user. Therefore, an Emergency phase is proposed in which CGM and IP exchange messages to administer insulin by themselves, assuming CONT cannot function properly. Of course, it would be safe for the user to prepare an emergency insulin and blood glucose meter in preparation for such a situation.

(E1)–(E3): IP periodically encrypts and sends Heartbeat messages to CONT to check if it is functioning properly. If CONT is usually working, it can send a response message to IP when it receives the Heartbeat message. On the other hand, when the communication between CONT and IP is disconnected due to mechanical or communication failure, CONT cannot deliver the response message for the Heartbeat message. At this point, IP detects Emergency Trigger and starts the Emergency phase.
(E4): To notify CGM that the Emergency phase has begun, IP sends the session identifier ( $S i d$ ) used in Registration and the warning message (Alert) to CGM. At this stage, IP and CGM calculate the emergency session key $(S K_{E M G}$ ). The emergency session key $(S K_{E M G}$ ) is generated using the mutual ECDHE public keys transmitted by the CONT in steps (R7) and (R8) of the Registration phase, their own ECDHE private key, and nonce values.
(E5): CGM generates an Emergency Request message that includes the session identifier ( $S i d$ ) and the user’s blood glucose level (BGL), which is encrypted with the emergency session key ( $S K_{E M G}$ ), and sends it to IP. IP administers the required insulin dose based on the received BGL and a predetermined critical value, and then encrypts the Emergency Response message with the emergency session key ( $S K_{E M G}$ ) that includes the session identifier ( $S i d$ ) and sends it to CGM.

4. Formal Verification

In this section, we analyze the proposed security protocol through well-known formal security analysis tools, BAN logic [19] and AVISPA [20]. Both have been used by many researchers to prove the security of their approaches. Security protocols can exhibit unintended behavior due to design flaws, the ambiguity of messages, or complex interactions. Therefore, verification is required to ensure the security of the proposed protocol. BAN logic was proposed by M. Burrows, M. Abadi, and R.M. Needham in 1989, and AVISPA was proposed by A. Armando’s research team in 2005. To prove security through analysis tools, it is necessary to convert the proposed security protocol into an appropriate model for each tool. The proposed security protocol consists of the Registration phase, the Communication phase, and the Emergency phase, and the converted models and verification process for each tool are shown in the subsection below.

4.1. BAN Logic

BAN logic [19] sequentially goes through the process of idealization, assumptions, goals, and derivation to verify the security of a protocol. The notations and rules of BAN logic used in the above process are shown in Table 3 and Table 4. First, in the idealization stage, unnecessary elements are removed from BAN logic to model the security of the proposed protocol. In the assumption stage, the minimum essential information known through environmental factors or pre-exchange processes before executing the proposed protocol is defined. In the goal stage, the security goals are defined to require in the target environment of the proposed protocol. Finally, in the derivation stage, a series of processes are represented to derive the security properties defined in the goal stage through BAN logic’s rules presented in Table 4 from the results of the idealization and assumption stages. The results of verifying the security of the proposed security protocol through BAN logic in this paper are as follows.

4.1.1. Idealization

As a first step, the proposed security protocol in this paper is modeled in an idealization form that removes unnecessary elements other than the message protected by encryption and message authentication codes. The idealization form of the proposed security protocol is presented below:

\begin{matrix} CONT \to CGM : & {〈 S i d, g^{x}, n_{1}, n_{2}, CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM 〉}_{P W D_{C G M}} \end{matrix}

(1)

\begin{matrix} CGM \to CONT : & {〈 S i d, g^{y}, n_{2}, n_{3}, CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM | CONT \overset{S K_{C G M}}{\leftrightarrow} CGM 〉}_{P W D_{C G M}} \end{matrix}

(2)

\begin{matrix} CONT \to IP : & {〈 S i d, g^{x}, n_{4}, n_{5}, CONT \overset{P W D_{I P}}{\leftrightarrow} IP 〉}_{P W D_{I P}} \end{matrix}

(3)

\begin{matrix} IP \to CONT : & {〈 S i d, g^{z}, n_{5}, n_{6}, CONT \overset{P W D_{I P}}{\leftrightarrow} IP, CONT \overset{S K_{I P}}{\leftrightarrow} IP 〉}_{S K_{I P}} \end{matrix}

(4)

\begin{matrix} CONT \to CGM : & {〈 S i d, g^{z}, n_{3}, n_{6}, CONT \overset{S K_{C G M}}{\leftrightarrow} CGM 〉}_{S K_{C G M}} \end{matrix}

(5)

\begin{matrix} CONT \to IP : & {〈 S i d, g^{y}, n_{3}, n_{6}, CONT \overset{S K_{I P}}{\leftrightarrow} IP 〉}_{S K_{I P}} \end{matrix}

(6)

\begin{matrix} IP \to CGM : & {〈 S i d, A l e r t, CGM \overset{S K_{E M G}}{\leftrightarrow} IP 〉}_{S K_{E M G}} \end{matrix}

(7)

\begin{matrix} CGM \to IP : & {〈 S i d, B G L, CGM \overset{S K_{E M G}}{\leftrightarrow} IP 〉}_{S K_{E M G}} \end{matrix}

(8)

4.1.2. Assumptions

In the Assumption step, assumptions necessary for the operation of the proposed protocol are formulated. Assumptions should contain only the minimum necessary and realistic information. The assumptions used in this section define security keys and freshness for CGM, CONT, and IP as follows:

\begin{matrix} CGM ∣ \equiv CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM \end{matrix}

(9)

\begin{matrix} CGM ∣ \equiv # (n_{1}) \end{matrix}

(10)

\begin{matrix} CGM ∣ \equiv \overset{g^{y}}{⟼} CGM \end{matrix}

(11)

\begin{matrix} CONT ∣ \equiv CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM \end{matrix}

(12)

\begin{matrix} CONT ∣ \equiv # (n_{2}) \end{matrix}

(13)

\begin{matrix} CONT ∣ \equiv \overset{g^{x}}{⟼} CONT \end{matrix}

(14)

\begin{matrix} IP ∣ \equiv CONT \overset{P W D_{I P}}{\leftrightarrow} IP \end{matrix}

(15)

\begin{matrix} IP ∣ \equiv # (n_{4}) \end{matrix}

(16)

\begin{matrix} IP ∣ \equiv \overset{g^{z}}{⟼} IP \end{matrix}

(17)

\begin{matrix} CONT ∣ \equiv CONT \overset{P W D_{I P}}{\leftrightarrow} IP \end{matrix}

(18)

\begin{matrix} CONT ∣ \equiv # (n_{5}) \end{matrix}

(19)

\begin{matrix} CGM ∣ \equiv # (n_{3}) \end{matrix}

(20)

\begin{matrix} IP ∣ \equiv # (n_{6}) \end{matrix}

(21)

4.1.3. Goals

Security protocols must meet security requirements to ensure safe communication for users in the environment in which they are applied. The security protocol proposed in this paper aims to protect the user’s sensitive medical information from malicious users in the APS environment. Therefore, we verify the security of the user authentication and session key exchange process presented in the proposed security protocol. The following defines the security requirements necessary to provide secure communication in the APS environment, such as user authentication and key reliability.

\begin{matrix} CGM ∣ \equiv CONT ∣ \equiv CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM \end{matrix}

(22)

\begin{matrix} CGM ∣ \equiv CONT \overset{g^{x y}}{\leftrightarrow} CGM \end{matrix}

(23)

\begin{matrix} CGM ∣ \equiv CONT \overset{S K_{C G M}}{\leftrightarrow} CGM \end{matrix}

(24)

\begin{matrix} CONT ∣ \equiv CGM ∣ \equiv CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM \end{matrix}

(25)

\begin{matrix} CONT ∣ \equiv CGM ∣ \equiv CONT \overset{S K_{C G M}}{\leftrightarrow} CGM \end{matrix}

(26)

\begin{matrix} CONT ∣ \equiv CONT \overset{g^{x y}}{\leftrightarrow} CGM \end{matrix}

(27)

\begin{matrix} CONT ∣ \equiv CONT \overset{S K_{C G M}}{\leftrightarrow} CGM \end{matrix}

(28)

\begin{matrix} IP ∣ \equiv CONT ∣ \equiv CONT \overset{P W D_{I P}}{\leftrightarrow} IP \end{matrix}

(29)

\begin{matrix} IP ∣ \equiv CONT \overset{g^{x z}}{\leftrightarrow} IP \end{matrix}

(30)

\begin{matrix} IP ∣ \equiv CONT \overset{S K_{I P}}{\leftrightarrow} IP \end{matrix}

(31)

\begin{matrix} CONT ∣ \equiv IP ∣ \equiv CONT \overset{P W D_{I P}}{\leftrightarrow} IP \end{matrix}

(32)

\begin{matrix} CONT ∣ \equiv IP ∣ \equiv CONT \overset{S K_{I P}}{\leftrightarrow} IP \end{matrix}

(33)

\begin{matrix} CONT ∣ \equiv CONT \overset{g^{x z}}{\leftrightarrow} IP \end{matrix}

(34)

\begin{matrix} CONT ∣ \equiv CONT \overset{S K_{I P}}{\leftrightarrow} IP \end{matrix}

(35)

\begin{matrix} CGM ∣ \equiv CONT ∣ \equiv CONT \overset{S K_{C G M}}{\leftrightarrow} CGM \end{matrix}

(36)

\begin{matrix} CGM ∣ \equiv CGM \overset{g^{y z}}{\leftrightarrow} IP \end{matrix}

(37)

\begin{matrix} CGM ∣ \equiv CGM \overset{S K_{E M G}}{\leftrightarrow} IP \end{matrix}

(38)

\begin{matrix} IP ∣ \equiv CONT ∣ \equiv CONT \overset{S K_{I P}}{\leftrightarrow} IP \end{matrix}

(39)

\begin{matrix} IP ∣ \equiv CGM \overset{g^{y z}}{\leftrightarrow} IP \end{matrix}

(40)

\begin{matrix} IP ∣ \equiv CGM \overset{S K_{E M G}}{\leftrightarrow} IP \end{matrix}

(41)

\begin{matrix} IP ∣ \equiv CGM ∣ \equiv CGM \overset{S K_{E M G}}{\leftrightarrow} IP \end{matrix}

(42)

\begin{matrix} CGM ∣ \equiv IP ∣ \equiv CGM \overset{S K_{E M G}}{\leftrightarrow} IP \end{matrix}

(43)

4.1.4. Derivation

Finally, the proposed security protocol is analyzed by applying the idealization form (1–8) and assumptions (9–22) to the rules of BAN logic (Table 4). The results derived from each idealization form must be appropriately matched with the Goals (i.e., security requirements) required by the target environment. The detailed derivation process for verifying the security of the protocol is as follows.

From Idealization (1):

\begin{matrix} CGM ◃ {〈 S i d, \overset{g^{x}}{⟼} CONT, n_{1}, n_{2}, CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM 〉}_{P W D_{C G M}} by (1) \end{matrix}

(44)

\begin{matrix} CGM ∣ \equiv CONT ∣ \sim (S i d, \overset{g^{x}}{⟼} CONT, n_{1}, n_{2}, CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM) \\ by (44), (9), MM \end{matrix}

(45)

\begin{matrix} CGM ∣ \equiv CONT ∣ \equiv (S i d, \overset{g^{x}}{⟼} CONT, n_{1}, n_{2}, CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM) \\ by (45), (10), FR, NV \end{matrix}

(46)

\begin{matrix} CGM ∣ \equiv CONT ∣ \equiv CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM by (46), BC \end{matrix}

(47)

\begin{matrix} CGM ∣ \equiv CONT ∣ \sim \overset{g^{x}}{⟼} CONT by (45), BC \end{matrix}

(48)

\begin{matrix} CGM ∣ \equiv CONT \overset{g^{x y}}{\leftrightarrow} CGM by (48), (11), DH \end{matrix}

(49)

\begin{matrix} CGM ∣ \equiv CONT \overset{S K_{C G M}}{\leftrightarrow} CGM by (49), (46), BC \end{matrix}

(50)

From Idealization (2):

\begin{matrix} CONT ◃ {〈 S i d, \overset{g^{y}}{⟼} CGM, n_{2}, n_{3}, CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM, CONT \overset{S K_{C G M}}{\leftrightarrow} CGM 〉}_{P W D_{C G M}} \\ by (2) \end{matrix}

(51)

\begin{matrix} CONT ∣ \equiv CGM ∣ \sim (S i d m \overset{g^{y}}{⟼} CGM, n_{2}, n_{3}, CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM | CONT \overset{S K_{C G M}}{\leftrightarrow} CGM) \\ by (51), (12), MM \end{matrix}

(52)

\begin{matrix} CONT ∣ \equiv CGM ∣ \equiv (S i d, \overset{g^{y}}{⟼} CGM, n_{2}, n_{3}, CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM, CONT \overset{S K_{C G M}}{\leftrightarrow} CGM) \\ by (52), (13), FR, NV \end{matrix}

(53)

\begin{matrix} CONT ∣ \equiv CGM ∣ \equiv CONT \overset{P W D_{C G M}}{\leftrightarrow} CGM by (53), BC \end{matrix}

(54)

\begin{matrix} CONT ∣ \equiv CGM ∣ \equiv CONT \overset{S K_{C G M}}{\leftrightarrow} CGM by (53), BC \end{matrix}

(55)

\begin{matrix} CONT ∣ \equiv CGM ∣ \sim \overset{g^{y}}{⟼} CGM by (52), BC \end{matrix}

(56)

\begin{matrix} CONT ∣ \equiv CONT \overset{g^{x y}}{\leftrightarrow} CGM by (56), (14), DH \end{matrix}

(57)

\begin{matrix} CONT ∣ \equiv CONT \overset{S K_{C G M}}{\leftrightarrow} CGM by (57), (18), BC \end{matrix}

(58)

From Idealization (3):

\begin{matrix} IP ◃ {〈 S i d, g^{x}, n_{4}, n_{5}, P W D_{I P} 〉}_{P W D_{I P}} by (3) \end{matrix}

(59)

\begin{matrix} IP ∣ \equiv CONT ∣ \sim (S i d, g^{x}, n_{4}, n_{5}, P W D_{I P}) by (59), (15), MM \end{matrix}

(60)

\begin{matrix} IP ∣ \equiv CONT ∣ \equiv (S i d, g^{x}, n_{4}, n_{5}, P W D_{I P}) by (60), (16), FR, NV \end{matrix}

(61)

\begin{matrix} IP ∣ \equiv CONT ∣ \equiv CONT \overset{P W D_{I P}}{\leftrightarrow} IP by (61), BC \end{matrix}

(62)

\begin{matrix} IP ∣ \equiv CONT ∣ \sim \overset{g^{x}}{⟼} CONT by (60), BC \end{matrix}

(63)

\begin{matrix} IP ∣ \equiv CONT \overset{g^{x z}}{\leftrightarrow} IP by (63), (A 9), DH \end{matrix}

(64)

\begin{matrix} IP ∣ \equiv CONT \overset{S K_{I P}}{\leftrightarrow} IP by (64), (61), BC \end{matrix}

(65)

From Idealization (4):

\begin{matrix} CONT ◃ {〈 S i d, \overset{g^{z}}{⟼} IP, n_{5}, n_{6}, CONT \overset{P W D_{I P}}{\leftrightarrow} IP, CONT \overset{S K_{I P}}{\leftrightarrow} IP 〉}_{P W D_{I P}} by (4) \end{matrix}

(66)

\begin{matrix} CONT ∣ \equiv IP ∣ \sim (S i d, \overset{g^{z}}{⟼} IP, n_{5}, n_{6}, CONT \overset{P W D_{I P}}{\leftrightarrow} IP, CONT \overset{S K_{I P}}{\leftrightarrow} IP) \\ by (66), (18), MM \end{matrix}

(67)

\begin{matrix} CONT ∣ \equiv IP ∣ \equiv (S i d, \overset{g^{z}}{⟼} IP, n_{5}, n_{6}, CONT \overset{P W D_{I P}}{\leftrightarrow} IP, CONT \overset{S K_{I P}}{\leftrightarrow} IP) \\ by (67), (19), FR, NV \end{matrix}

(68)

\begin{matrix} CONT ∣ \equiv IP ∣ \equiv CONT \overset{P W D_{I P}}{\leftrightarrow} IP by (68), BC \end{matrix}

(69)

\begin{matrix} CONT ∣ \equiv IP ∣ \equiv CONT \overset{S K_{I P}}{\leftrightarrow} IP by (68), BC \end{matrix}

(70)

\begin{matrix} CONT ∣ \equiv IP ∣ \sim \overset{g^{z}}{⟼} IP by (67), BC \end{matrix}

(71)

\begin{matrix} CONT ∣ \equiv CONT \overset{g^{x z}}{\leftrightarrow} IP by (71), (14), DH \end{matrix}

(72)

\begin{matrix} CONT ∣ \equiv CONT \overset{S K_{I P}}{\leftrightarrow} IP by (72), (68), BC \end{matrix}

(73)

From Idealization (5):

\begin{matrix} CGM ◃ {〈 S i d, \overset{g^{z}}{⟼} IP, n_{3}, n_{6}, CONT \overset{S K_{C G M}}{\leftrightarrow} CGM 〉}_{S K_{C G M}} by (5) \end{matrix}

(74)

\begin{matrix} CGM ∣ \equiv CONT ∣ \sim (S i d, \overset{g^{z}}{⟼} IP, n_{3}, n_{6}, CONT \overset{S K_{C G M}}{\leftrightarrow} CGM) by (74), (50), MM \end{matrix}

(75)

\begin{matrix} CGM ∣ \equiv CONT ∣ \equiv (S i d, \overset{g^{z}}{⟼} IP, n_{3}, n_{6}, CONT \overset{S K_{C G M}}{\leftrightarrow} CGM) by (75), (20), FR, NV \end{matrix}

(76)

\begin{matrix} CGM ∣ \equiv CONT ∣ \equiv CONT \overset{S K_{C G M}}{\leftrightarrow} CGM by (76), BC \end{matrix}

(77)

\begin{matrix} CGM ∣ \equiv CONT ∣ \sim \overset{g^{z}}{⟼} IP by (75), BC \end{matrix}

(78)

\begin{matrix} CGM ∣ \equiv CGM \overset{g^{y z}}{\leftrightarrow} IP by (78), (11), DH \end{matrix}

(79)

\begin{matrix} CGM ∣ \equiv CGM \overset{S K_{E M G}}{\leftrightarrow} IP by (79), (76), BC \end{matrix}

(80)

\begin{matrix} CGM ∣ \equiv # (CGM \overset{S K_{E M G}}{\leftrightarrow} IP) by (79), (76), BC \end{matrix}

(81)

From Idealization (6):

\begin{matrix} IP ◃ {〈 S i d, \overset{g^{y}}{⟼} CGM, n_{3}, n_{6}, CONT \overset{S K_{I P}}{\leftrightarrow} IP 〉}_{S K_{I P}} by (6) \end{matrix}

(82)

\begin{matrix} IP ∣ \equiv CONT ∣ \sim (S i d, \overset{g^{y}}{⟼} CGM, n_{3}, n_{6}, CONT \overset{S K_{I P}}{\leftrightarrow} IP) by (82), (65), MM \end{matrix}

(83)

\begin{matrix} IP ∣ \equiv CONT ∣ \equiv (S i d, \overset{g^{y}}{⟼} CGM, n_{3}, n_{6}, CONT \overset{S K_{I P}}{\leftrightarrow} IP) by (83), (21), FR, NV \end{matrix}

(84)

\begin{matrix} IP ∣ \equiv CONT ∣ \equiv CONT \overset{S K_{I P}}{\leftrightarrow} IP by (84), BC \end{matrix}

(85)

\begin{matrix} IP ∣ \equiv CONT ∣ \sim \overset{g^{y}}{⟼} CGM by (83), BC \end{matrix}

(86)

\begin{matrix} IP ∣ \equiv CGM \overset{g^{y z}}{\leftrightarrow} IP by (86), (17), DH \end{matrix}

(87)

\begin{matrix} IP ∣ \equiv CGM \overset{S K_{E M G}}{\leftrightarrow} IP by (87), (83), BC \end{matrix}

(88)

\begin{matrix} IP ∣ \equiv # (CGM \overset{S K_{E M G}}{\leftrightarrow} IP) by (87), (83), BC \end{matrix}

(89)

From Idealization (7):

\begin{matrix} CGM ◃ {〈 S i d, A l e r t, CGM \overset{S K_{E M G}}{\leftrightarrow} IP 〉}_{S K_{E M G}} by (7) \end{matrix}

(90)

\begin{matrix} CGM ∣ \equiv IP ∣ \sim (S i d, A l e r t, CGM \overset{S K_{E M G}}{\leftrightarrow} IP) by (90), (80), MM \end{matrix}

(91)

\begin{matrix} CGM ∣ \equiv IP ∣ \equiv (S i d, A l e r t, CGM \overset{S K_{E M G}}{\leftrightarrow} IP) by (91), (81), FR, NV \end{matrix}

(92)

\begin{matrix} CGM ∣ \equiv IP ∣ \equiv CGM \overset{S K_{E M G}}{\leftrightarrow} IP by (92), BC \end{matrix}

(93)

From Idealization (8):

\begin{matrix} IP ◃ {〈 S i d, B G L, CGM \overset{S K_{E M G}}{\leftrightarrow} IP 〉}_{S K_{E M G}} by (8) \end{matrix}

(94)

\begin{matrix} IP ∣ \equiv CGM ∣ \sim (S i d, B G L, CGM \overset{S K_{E M G}}{\leftrightarrow} IP) by (94), (88), MM \end{matrix}

(95)

\begin{matrix} IP ∣ \equiv CGM ∣ \equiv (S i d, B G L, CGM \overset{S K_{E M G}}{\leftrightarrow} IP) by (95), (89), FR, NV \end{matrix}

(96)

\begin{matrix} IP ∣ \equiv CGM ∣ \equiv CGM \overset{S K_{E M G}}{\leftrightarrow} IP by (96), BC \end{matrix}

(97)

According to the derivation above, the proposed security protocol can achieve all the security goals stated in the goals. This means that the proposed protocol can securely protect users’ medical information from malicious attackers. Table 5 compares the security requirements, the security goals presented in the goals, and the stages of derivation at which the security goals are achieved. Furthermore, we show that the security requirements and goals are satisfied by using Theorem 1 and following Lemmas.

Theorem 1.

The proposed security protocol is secure against malicious attacks.

Proof of Theorem 1.

Through Lemma 1 to Lemma 6, the defined goals are satisfied that the proposed security protocol is secure against malicious attacks. □

Lemma 1.

The proposed security protocol can provide mutual authentication in three communication segments, CONT and CGM, CONT and IP, and IP and CGM.

Proof of Lemma 1.

On the one hand, it can be demonstrated that the security protocol supports mutual authentication by verifying the trust between each other through a pre-shared key. In our proposed protocol, CGM and IP each use a pre-shared key with CONT. Mutual authentication between CGM and CONT can be verified through derivations (47) and (54). Similarly, mutual authentication between IP and CONT can be verified through derivations (62) and (69). On the other hand, there is no pre-shared key between CGM and IP. However, mutual authentication can be demonstrated based on the trust of the emergency session key

S K_{E M G}

, which was exchanged during the Registration phase. □

Lemma 2.

The session keys

S K_{C G M}

and

S K_{I P}

are securely exchanged between CGM and CONT, and between IP and CONT, respectively.

Proof of Lemma 2.

CGM and CONT have direct beliefs in the session key

S K_{C G M}

through the derivations (50) and (58). Furthermore, they can trust that each other has belief in the session key

S K_{C G M}

through the derivation (55) and (69). Similarly, IP and CONT can verify their direct beliefs in the session key

S K_{I P}

through the derivations (65) and (73). Their indirect beliefs in the session key can be confirmed through the derivations (70) and (85). □

Lemma 3.

The proposed security protocol can provide the perfect forward secrecy in the session keys

S K_{C G M}

and

S K_{I P}

Proof of Lemma 3.

From (49) and (57), CGM and CONT derive the session key

S K_{C G M}

through ECDHE key exchange. ECDHE key exchange utilizes the ephemeral key, and, thus, the private key is deleted immediately after the key exchange. This prevents the restoration of future keys and eliminates the relationship between keys, allowing for perfect forward secrecy. The session key

S K_{I P}

also satisfies perfect forward secrecy through ECDHE key exchange between IP and CONT from (64) and (72). □

Lemma 4.

The proposed security protocol can provide a secure channel between CGM and IP in emergency situations.

Proof of Lemma 4.

The proposed security protocol in this paper provides not only the Registration phase and the Communication phase but also the Emergency phase. During the Emergency phase, CGM and IP can communicate securely using the emergency session key exchanged in the Registration phase. In the above derivations, CGM and IP can verify both direct beliefs (80), (88) and indirect beliefs (93), (97) for the emergency session key

S K_{E M G}

. □

Lemma 5.

The proposed security protocol can provide the perfect forward secrecy in the emergency session key (

S K_{E M G}

Proof of Lemma 5.

According to (79) and (87), the emergency session key

S K_{E M G}

is generated with the ECDHE session key. As same as Lemma 3, the emergency session key also satisfies the perfect forward secrecy. □

Lemma 6.

The proposed security protocol can provide confidentiality and integrity.

Proof of Lemma 6.

The confidentiality of the protocol depends on the secure exchange of keys and the safety of the keys themselves. The security protocol proposed in this paper has demonstrated secure key exchange for the session keys

S K_{C G M}

S K_{I P}

, and

S K_{E M G}

in Lemma 2 and Lemma 4. In addition, Lemma 3 and Lemma 5 have confirmed that perfect forward secrecy is provided for each key. Therefore, the session keys exchanged in the proposed security protocol are secure and can provide confidentiality. As confirmed by Lemma 1, CGM, IP, and CONT all have both direct and indirect trust in the pre-shared keys, allowing them to believe that messages have not been altered during transmission. □

As a result, the safety of the proposed security protocol has been proven through the Theorem and Lemmas presented in this paper, and it can be considered secure from malicious attacks.

4.2. AVISPA

In the previous section, we proved the security of the proposed security protocol using BAN logic. BAN logic is a useful tool for representing and analyzing security protocols based on modal logic. However, previous research has pointed out the limitations of BAN logic, such as inaccurate message representation and the absence of inference rules for hash functions, in clearly transforming security protocols into an idealization form. While acknowledging that BAN logic is a useful formal verification tool, this research recommends using automated formal verification tools in conjunction with BAN logic [21,22]. Therefore, in this paper, we verify the security of the proposed security protocol using AVISPA [20], an automated formal verification tool, in conjunction with BAN Logic.

AVISPA provides a toolset that includes a high-level protocol specification language (HLPSL) [23] to describe security protocols and to specify intended security properties. HLPSL2IF converts HLPSL specifications into an intermediate format (IF), which is a low-level language directly read by the backend of AVISPA tools. The IF specification of the protocol is then input to the backend of the AVISPA tool to analyze the specified security goals. Figure 3 illustrates this process.

The HLPSL specification consists of three modules, basic roles used in the roles, session, and environment. The basic roles represent the specifications of each protocol participant modeled with known initial information as parameters. Then, these roles are invoked to specify how the resulting participants interact by linking various basic roles to the configured roles. The transition part of the HLPSL specification includes a set of transitions between different roles. Each transition symbolizes message acceptance and response message transmission. Figure 4 a,b, and Figure 5 show the AVISPA verification results and protocol simulation results for the protocol. Since the results obtained from both options of AVISPA, the proposed security protocol has been analyzed as ’SAFE’, which can be seen as secure against known attacks.

4.3. Discussion

In this section, we present the comparison evaluation results based on two aspects, security analysis and overhead analysis. For the comparison, we have adopted not only IMD security protocols (Wu et al. [13], Chi et al. [14], HAT [15]) presented in Related Works but also widely adopted protocols in communication devices, such as Bluetooth [16] and TLS 1.3 [18]. In the security analysis, we compare the support for seven security requirements. In the overhead analysis, we implement the system as described in Section 5 and analyze the Computational Overhead and Communication Overhead based on the implementation.

4.3.1. Security Analysis

The proposed security protocol is compared to existing protocols in terms of the seven security requirements (Mutual Authentication, Confidentiality, Integrity, Secure Key Exchange, Perfect Forward Secrecy, Privacy, and Emergency Phase) presented in Section 3. The security requirements that each security protocol satisfies are shown in Table 6.

According to Table 6, all protocols can support Mutual Authentication (AUTH), Confidentiality (CONF), Integrity (INT), and Secure Key Exchange (SKE). Perfect Forward Secrecy (PFS) was satisfied by HAT, TLS 1.3, and the proposed protocol and Privacy (PRV) can be provided by TLS 1.3 and the proposed protocol. It can be observed that the Emergency phase (EMEG), which was presented as an important security requirement of APS in this paper, is only satisfied by the proposed protocol. Finally, all protocols except for Bluetooth LE can provide countermeasures against Replay Attacks (RPA) and Man-in-The-Middle Attacks (MiTM). In summary, only the proposed protocol can satisfy all seven security requirements presented in this paper.

4.3.2. Overhead Analysis

To the best of our knowledge, there is limited meaningful research on security protocols focused on APS, and this paper aims to pioneer this area by designing and verifying a security protocol. To demonstrate the feasibility of the proposed security protocol, we conduct a comparative analysis of computational (Table 7) and communication (Table 8) overheads with existing studies designed for IMD, a field similar to APS.

Table 7 and Table 8 compare our proposed protocol with existing IMD security protocols, as well as Bluetooth LE and TLS 1.3, in terms of computational and communication overheads. Compared with [13,14,16,18], our proposed protocol is more efficient due to the exclusion of asymmetric key operations based on the characteristics of APS, which is based on low-performance devices. On the other hand, our proposed protocol may have higher computational costs than [15] due to the additional computations required for exchanging the session keys for Emergency phase only supported by our proposed protocol.

5. Experiment

To prove the feasibility of the proposed protocol, we have set up the environment for the APS and implemented the protocol. We used the Arduino Nano 33 kit for the Insulin pump, nRF52840 development kit (DK) for CGM, and Galaxy S20 series with Android 13 for the controller. Detailed specifications of the implementation environment are shown in Table 9.

Figure 6 shows the implemented emulation for the APS. Note that this emulation is based on a real product on a market to enhance the credibility of the test. Though we have proposed our protocol, hoping to replace the security protocol of Bluetooth, we have implemented the protocol on the application layer, which is on top of the Bluetooth layer, for fast testing purposes.

After successfully implementing our proposed protocol, we conducted a test to compare the computation overhead and energy consumption with the widely used BLE mode in the IoT industry. This comparison is important for assessing feasibility. To ensure accuracy, we needed to standardize the test scenario. Our proposed protocol establishes secure channels among IP, CONT, and CGM at once. However, BLE only supports one-to-one communication. Therefore, we assumed three separate BLE connections in order to compare with the proposed protocol in the same APS environment. In other words, each device should establish two BLE connections. The following Table 10 presents the computation overhead in each environment based on a unified scenario.

The experimental comparison shows significantly different results depending on the processor. IoT devices took more than 400 times longer to handle cryptographical computation. This means that feasibility is much more dependent on how much it is suitable for IoT devices, not the controller. Figure 7 shows a more detailed comparison of our protocol and BLE.

In this section, we present a comparative analysis between our proposed protocol and Bluetooth Low Energy (BLE) regarding the computational overhead incurred during the Registration phase. The APS environment, as outlined in this paper, consists of a closed network comprising three wireless terminals. BLE has gained traction in various applications due to its advantages of low computational overhead and ease of connection. However, based on the findings presented in Table 10 and Figure 7, our proposed protocol demonstrates a lower computational overhead compared to BLE, with a reduction of 26.4%. This reduction in overhead showcases the efficiency and optimization achieved by our proposed protocol, making it a proper approach for APS environments where power-constrained IoT devices are prevalent.

Furthermore, our proposed protocol offers additional security services, as elaborated in Section 4.3, which BLE fails to provide. These services include perfect forward secrecy, privacy, emergency phase, defense against replay attacks and man-in-the-middle attacks. These security features further enhance the applicability and robustness of our proposed protocol in real-world scenarios.

In conclusion, our analysis reveals that our proposed protocol outperforms BLE in terms of computational overhead and offers advanced security services tailored to the unique requirements of APS environments utilizing power-constrained IoT devices.

6. Conclusions

The increasing demand for self-operating APS to elevate the medical care of patients with Type 1 Diabetes has opened a wide range of security threats due to its structure and inevitable integration with wireless transmission medium. Hence, protecting the communication channels of all the devices composing the APS is of paramount importance since sensitive information about the patient is involved. It is essential to balance security, reliability, and resiliency when crafting solutions that ensure patient safety and the protection of personal information. To this end, we designed a security protocol for the APS environment and formally verified its security and correctness using BAN logic and AVISPA. Furthermore, the proposed protocol was also emulated in a controlled environment with actual devices while comparing its computation and communication overhead with other existing work. Based on the experimental results, the proposed protocol demonstrated superior security and performance over existing protocols and standards for the IoT ecosystem.

Healthcare-target systems commonly collect and analyze the health information of patients or users, which can then be utilized for clinical decision support in providing appropriate medical care, preventive measures, and the like. Meanwhile, this article will explore the possibility of leveraging the biological distinction of a patient for authentication strategy, potentially elevating the proposed security protocol.

It would be highly impactful to utilize artificial intelligence and machine learning technology in analyzing medical data and delivering personalized treatment approaches to patients. In our future research, we will design protocols that leverage artificial intelligence to determine patient-specific insulin dosage instead of solely exchanging information on dosage and remaining supply. Additionally, we intend to implement our previously studied attack detection technique [11,12] for APS, along with the proposed protocol, in a real-world setting.

Author Contributions

Conceptualization, J.K., and I.Y.; methodology, J.K. and I.Y.; validation, J.K. and D.S.; formal analysis, J.K. and J.O.; investigation, J.O. and D.S.; data curation, J.K. and P.V.A.; writing—original draft preparation, J.K., J.O., D.S., and H.K.; writing—review and editing, J.K., P.V.A., and I.Y.; visualization, J.O. and H.K.; supervision, I.Y.; project administration, I.Y.; funding acquisition, I.Y. All authors have read and agreed to the published version of the manuscript.

Funding

This work was supported by Institute of Information & communications Technology Planning & Evaluation (IITP) grant funded by the Korea government(MSIT) (No.2022-0-00103, Development of security verification technology against vulnerabilities to assure IoT/IIoT device safety).

Institutional Review Board Statement

Not applicable.

Informed Consent Statement

Not applicable.

Data Availability Statement

Not applicable.

Conflicts of Interest

The authors declare no conflict of interest.

References

Astillo, P.V.; Jeong, J.; Chien, W.C.; Kim, B.; Jang, J.; You, I. SMDAps: A specification-based misbehavior detection system for implantable devices in artificial pancreas system. J. Internet Technol. 2021, 22, 1–11. [Google Scholar]
Yoo, J.H.; Kim, J.H. Advances in Continuous Glucose Monitoring and Integrated Devices for Management of Diabetes with Insulin-Based Therapy: Improvement in Glycemic Control. Diabetes Metab. J. 2023, 47, 27–41. [Google Scholar] [PubMed]
Artificial Pancreas Device Systems (APDS) Market: Global Industry Trends, Share, Size, Growth, Opportunity and Forecast 2022–2027; IMARC: Brooklyn, NY, USA, 2021.
Gotadki, R. Artificial Pancreas Device System Market. 2023. Available online: https://www.marketresearchfuture.com/reports/artificial-pancreas-device-system-market-6671 (accessed on 17 March 2023).
Hassija, V.; Chamola, V.; Bajpai, B.C.; Naren; Zeadally, S. Security issues in implantable medical devices: Fact or fiction? Sustain. Cities Soc. 2021, 66, 102552. [Google Scholar] [CrossRef]
Tabasum, A.; Safi, Z.; AlKhater, W.; Shikfa, A. Cybersecurity Issues in Implanted Medical Devices. In Proceedings of the 2018 International Conference on Computer and Applications (ICCA’18), Beirut Lebanon, 25–26 August 2018; pp. 1–9. [Google Scholar]
Pycroft, L.; Aziz, T.Z. Security of implantable medical devices with wireless connections: The dangers of cyber-attacks. Expert Rev. Med Devices 2018, 15, 403–406. [Google Scholar] [CrossRef] [PubMed]
Lazaro, C.; Oruklu, E.; Cinar, A. Security challenges and solutions for closed-loop artificial pancreas systems. In Proceedings of the2017 IEEE 60th International Midwest Symposium on Circuits and Systems (MWSCAS’17), Boston, MA, USA, 6–9 August 2017; pp. 1097–1100. [Google Scholar]
Cybersecurity in Medical Devices: Quality System Considerations and Content of Premarket Submissions Draft Guidance for Industry and Food and Drug Administration Staff; Technical report; US Food and Drug Administration: Silver Spring, MD, USA, 2022.
Content of Premarket Submissions for Management of Cybersecurity in Medical Devices: Guidance for Industry and Food and Drug Administration Staff; Technical report; US Food and Drug Administration: Silver Spring, MD, USA, 2014.
Astillo, P.V.; Duguma, D.G.; Park, H.; Kim, J.; Kim, B.; You, I. Federated intelligence of anomaly detection agent in IoTMD-enabled Diabetes Management Control System. Future Gener. Comput. Syst. 2022, 128, 395–405. [Google Scholar] [CrossRef]
Astillo, P.V.; Duguma, G.C.D.G.; Kim, J.; You, I. TrMAps: Trust Management in Specification-Based Misbehavior Detection System for IMD-Enabled Artificial Pancreas System. IEEE J. Biomed. Health Inform. 2021, 25, 3763–3775. [Google Scholar] [CrossRef] [PubMed]
Wu, L.; Chi, H.; Du, X. A Secure Proxy-based Access Control Scheme for Implantable Medical Devices. arXiv 2018, arXiv:1803.07751. [Google Scholar]
Chi, H.; Wu, L.; Du, X.; Zeng, Q.; Ratazzi, P. e-safe: Secure, efficient and forensics-enabled access to implantable medical devices. In Proceedings of the 2018 IEEE Conference on Communications and Network Security (CNS’18), Beijing, China, 30 May–1 June 2018; pp. 1–9. [Google Scholar]
Duttagupta, S.; Marin, E.; Singelee, D.; Preneel, B. HAT: Secure and Practical Key Establishment for Implantable Medical Devices. In Proceedings of the 13th ACM Conference on Data and Application Security and Privacy (CODASPY’23), Charlotte, NC, USA, 24–26 April 2023; pp. 1–14. [Google Scholar]
Duguma, D.G.; Astillo, P.V.; Gebremariam, Y.E.; Kim, B.; You, I. Comparative Analysis of Bluetooth LE and EDHOC for Potential Security Protocol in Artificial Pancreas System. In Proceedings of the 2021 International Symposium on Mobile Internet Security (MobiSec’21), Jeju, Republic of Korea, 7–9 October 2021; pp. 30–43. [Google Scholar]
Rescorla, E. The Transport Layer Security (TLS) Protocol Version 1.3. Internet Engineering Task Force, RFC 8446. 2018. Available online: https://datatracker.ietf.org/doc/html/rfc8446 (accessed on 28 April 2023).
Dowling, B.; Fischlin, M.; Günther, F.; Stebila, D. A Cryptographic Analysis of the TLS 1.3 Handshake Protocol. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security (CCS’15), Denver, CO, USA, 12–16 October 2015; pp. 1197–1210. [Google Scholar]
Burrows, M.; Abadi, M.; Needham, R.M. A logic of authentication. ACM Trans. Comput. Syst. 1990, 8, 18–36. [Google Scholar] [CrossRef]
Armando, A.; Basin, D.; Boichut, Y.; Chevalier, Y.; Compagna, L.; Cuellar, J.; Drielsma, P.H.; Heám, P.; Kouchnarenko, O.; Mantovani, J.; et al. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV’05), Edinburgh, Scotland, UK, 6–10 July 2005; Volume 3576, pp. 281–285. [Google Scholar]
Boyd, C.; Mao, W. On a limitation of BAN logic. In Proceedings of the 1993 Workshop on the Theory and Application of Cryptographic Techniques (EUROCRYPT’93), Lofthus, Norway, 23–27 May 1993; Volume 765, pp. 240–247. [Google Scholar]
Meadows, C.A. Formal verification of cryptographic protocols: A survey. In Proceedings of the 4th International Conference on the Theory and Applications of Cryptology (ASIACRYPT’94), Wollongong, Australia, 28 November–1 December 1994; pp. 135–150. [Google Scholar]
Chevalier, Y.; Compagna, L.; Cuellar, J.; Drieslma, P.H.; Mantovani, J.; Mödersheim, S.; Vigneron, L. A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. In Proceedings of the 2004 Workshop on Specification and Automated Processing of Security Requirements (SAPS’04), Linz, Austria, 20–25 September 2004; pp. 193–205. [Google Scholar]

Figure 1. An exemplary illustration of the Artificial Pancreas System.

Figure 2. Proposed protocol for secure communication of APS.

Figure 3. Architecture of AVISPA.

Figure 4. AVISPA results of the proposed security protocol.

Figure 5. AVISPA protocol simulation.

Figure 6. Experimental emulation for the APS.

Figure 7. Comparison of two protocols on Arduino Nano 33.

Table 1. Notations.

Notation	Meaning
CGM	Continuous Glucose Monitoring
CONT	Controller
IP	Insulin Pump
$S i d$	Session ID
$P W D_{X}$	X’s passcode
$X, Y, Z$	ECDHE private key
$g^{X}$ , $g^{Y}$ , $g^{Z}$	ECDHE public key
$n_{X}$	x-th nonce
$S K_{X}$	Secret key between X and controller
$S K_{E M G}$	Secret key for emergency situation
$H M_{X}$	x-th Hash-based message authentication code
CMD	Command message
dose	Insulin dose
IoB	Insulin that is still active in the body
Heartbeat	Message to check the status of the controller
Response	Message to respond to Heartbeat message
Alert	Message to inform the emergency situation
BGL	Blood glucose level

Table 2. Ephemeral option of elliptic curve Diffie–Hellman key exchange.

ECDHE Domain Parameters (p, a, b, g, n, and h) are Pre-Shared between Alice and Bob.
1. ECDHE Key Generation
1. Alice generates an ephemeral private key X from {1, $\dots$ , $n - 1$ }.
2. Alice derives a public key $g^{X}$ from X.
3. Bob also generates own ephemeral private key Y from {1, $\dots$ , $n - 1$ }.
4. Bob derives own ECDHE public key $g^{Y}$ from Y.
2. ECDHE Session Key Exchange
1. Alice sends the public key $g^{X}$ to Bob.
2. Bob computes the ECDHE session key S via the following operation.
$S = {(g^{X})}^{Y} = g^{X Y}$
3. After computing the ECDHE session key, Bob sends the public key $g^{Y}$ to Alice.
4. Alice also computes the ECDHE session key S via the following operation.
$S = {(g^{Y})}^{X} = g^{Y X} = g^{X Y}$
5. Alice and Bob successfully exchange the ECDHE session key S and remove each ephemeral private key.
ECDHE domain parameter
p: a prime number indicating the finite field size;
a, b: the coefficients for the chosen elliptic curve equation;
g: the base point to generate a subgroup;
n, h: the order and co-factor of the subgroup;

Table 3. Notations of BAN logic.

Notation	Meaning
$P ∣ \equiv X$	P believes the message X
$P ◃ X$	P receives the message X
$P ∣ \sim X$	P previously sent the message X
$P \Rightarrow X$	P has authority over X
$# (X)$	The message X is fresh
${〈 X 〉}_{K}$	X is combined with a secret K
${X}_{K}$	X is encrypted with a key K
$P \overset{K}{\leftrightarrow} Q$	K is a secret key shared between P and Q
$\overset{K}{⟼} P$	K is the public key of P
$P \overset{K}{⇋} Q$	K is a shared secret between P and Q

Table 4. Rules of BAN logic.

Rule	Formula
Message Meaning Rule (MM)	$\frac{P ∣ \equiv P \overset{K}{\leftrightarrow} Q, P ◃ {X}_{K}}{P ∣ \equiv Q ∣ \sim X}$ $\frac{P ∣ \equiv P \overset{K}{⇋} Q, P ◃ {〈 X 〉}_{K}}{P ∣ \equiv Q ∣ \sim X}$ $\frac{P ∣ \equiv \overset{K}{⟼} Q, P ◃ {X}_{Q^{- 1}}}{P ∣ \equiv Q ∣ \sim X}$
Nonce Verification Rule (NV)	$\frac{P ∣ \equiv # (X), P ∣ \equiv Q ∣ \sim X}{P ∣ \equiv Q ∣ \equiv X}$
Jurisdiction Rule (JR)	$\frac{P ∣ \equiv Q \Rightarrow X, P ∣ \equiv Q ∣ \sim X}{P ∣ \equiv X}$
Freshness Rule (FR)	$\frac{P ∣ \equiv # (X)}{P ∣ \equiv # (X, Y)}$
Decomposition Rule (DR)	$\frac{P ◃ (X, Y)}{P ◃ X}$
Belief Conjunction Rule (BC)	$\frac{P ∣ \equiv X, P ∣ \equiv Y}{P ∣ \equiv (X, Y)}$ $\frac{P ∣ \equiv Q ∣ \equiv (X, Y)}{P ∣ \equiv Q ∣ \equiv X}$ $\frac{P ∣ \equiv Q ∣ \sim (X, Y)}{P ∣ \equiv Q ∣ \sim X}$
Diffie-Hellman Rule	$\frac{P ∣ \equiv Q ∣ \sim \overset{g^{Y}}{⟼} Q, P ∣ \equiv \overset{g^{X}}{⟼} P}{P ∣ \equiv P \overset{g^{X Y}}{\leftrightarrow} Q}$ $\frac{P ∣ \equiv Q ∣ \sim \overset{g^{Y}}{⟼} Q, P ∣ \equiv \overset{g^{X}}{⟼} P}{P ∣ \equiv P \overset{g^{X Y}}{⇆} Q}$

Table 5. Comparison table of security requirements and goal achievements.

Security Requirements	Goals	Derivation
Mutual Authentication	CONT – CGM: (22), (25) CONT – IP: (29), (32) CGM – IP: (42), (43)	CONT – CGM: (47), (54) CONT – IP: (62), (69) CGM – IP: (93), (97)
Secure Key Exchange	$S K_{C G M}$ : (24), (26), (28), (36) $S K_{I P}$ : (31), (33), (35), (39)	$S K_{C G M}$ : (50), (55), (58), (77) $S K_{I P}$ : (65), (70), (73), (85)
Perfect Forward Secrecy	CONT – CGM: (23), (27) CONT – IP: (30), (34) CGM – IP: (37), (40)	CONT – CGM: (49), (57) CONT – IP: (64), (72) CGM – IP: (79), (87)
Emergency Phase	$S K_{E M G}$ : (38), (41), (42), (43)	$S K_{E M G}$ : (80), (88), (93), (97)

Table 6. Comparison in terms of security requirements with existing protocols.

Protocol	Security Requirements
Protocol	AUTH	CONF	INT	SKE	PFS	PRV	EMEG	RPA	MiTM
Wu et al. [13]	◯	◯	◯	◯	×	×	×	◯	◯
Chi et al. [14]	◯	◯	◯	◯	×	×	×	◯	◯
HAT [15]	◯	◯	◯	◯	◯	×	×	◯	◯
Bluetooth LE [16]	◯	◯	◯	◯	×	×	×	×	×
TLS 1.3 [18]	◯	◯	◯	◯	◯	◯	×	◯	◯
Our Proposed	◯	◯	◯	◯	◯	◯	◯	◯	◯

◯: Support; ×: Not support; AUTH: Mutual Authentication; CONF: Confidentiality; INT: Integrity; SKE: Secure Key Exchange; PFS: Perfect Forward Secrecy; PRV: Privacy; EMEG: Emergency phase; RPA: Defense against replay attack; MiTM: Defense against man-in-the-middle attack.

Table 7. Comparison in terms of computational overheads with existing protocols.

Protocol	Overhead
Wu et. al. [13]	$10 T_{H} + 3 T_{S E} + 3 T_{S D} + 1 T_{A E} + 1 T_{A D} + 2 T_{S I G N} + 2 T_{V E R}$
Chi et. al. [14]	$19 T_{H} + 4 T_{S E} + 4 T_{S D} + 1 T_{A E} + 1 T_{A D} + 2 T_{S I G N} + 2 T_{V E R}$
HAT [15]	$9 T_{H} + 2 T_{S E} + 2 T_{S D} + 2 T_{D H E}$
Bluetooth LE * [16]	$2 (12 T_{H} + 2 T_{D H E})$
TLS 1.3 * [18]	$2 (22 T_{H} + 1 T_{S I G N} + 1 T_{V E R} + 2 T_{D H E})$
Our Proposed	$16 T_{H} + 6 T_{D H E}$

T_{H}

: Cryptographic hash function;

T_{S E}

: Symmetric encryption;

T_{S D}

: Symmetric decryption;

T_{A E}

: Asymmetric encryption;

T_{A D}

: Asymmetric decryption;

T_{S I G N}

: Digital signature;

T_{V E R}

: Digital signature verification;

T_{D H E}

: Elliptic curve Diffie–Hellman Ephemeral; * To facilitate comparison in this paper, protocols generally used in two-party environments were; reconfigured into three-party settings for APS environments.

Table 8. Comparison in terms of communication overheads with existing protocols.

Protocol	Round-Trip Times (RTT)
Wu et. al. [13]	3
Chi et. al. [14]	6
HAT [15]	1
Bluetooth LE [16]	4
TLS 1.3 [18]	1
Our Proposed	3

Table 9. Test environment specification.

Specification	Arduino Nano 33 (Insulin Pump)	Galaxy S 20 (Android Controller)	nRF52840 (CGM)
CPU Core	32-bit ARM^® Cortex^{^®}-M4	Samsung Exynos 990(Exynos M5 MP2 + ARM^® Cortex^® - A76 MP2 + ARM^® Cortex^® - A55 MP4)	32-bit ARM^® Cortex^®-M4
Ram	64 KB Flash ram 512 KB Sram	8 GB	64 KB Flash ram 512 KB Sram
Voltage	3.3 V	3.85–4.4 V	3.3 V
Programming Language	C++	Kotlin	C

Table 10. Comparison results of computation overhead.

	Arduino Nano 33 (Insulin Pump)	Galaxy S 20 (Android Controller)	nRF52840 (CGM)
Proposed protocol	333.6 ms	0.76 ms	68.24 ms
Bluetooth LE	452.8 ms	1.28 ms	91.44 ms

Disclaimer/Publisher’s Note: The statements, opinions and data contained in all publications are solely those of the individual author(s) and contributor(s) and not of MDPI and/or the editor(s). MDPI and/or the editor(s) disclaim responsibility for any injury to people or property resulting from any ideas, methods, instructions or products referred to in the content.

© 2023 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (https://creativecommons.org/licenses/by/4.0/).

Share and Cite

MDPI and ACS Style

Kim, J.; Oh, J.; Son, D.; Kwon, H.; Astillo, P.V.; You, I. APSec1.0: Innovative Security Protocol Design with Formal Security Analysis for the Artificial Pancreas System. Sensors 2023, 23, 5501. https://doi.org/10.3390/s23125501

AMA Style

Kim J, Oh J, Son D, Kwon H, Astillo PV, You I. APSec1.0: Innovative Security Protocol Design with Formal Security Analysis for the Artificial Pancreas System. Sensors. 2023; 23(12):5501. https://doi.org/10.3390/s23125501

Chicago/Turabian Style

Kim, Jiyoon, Jongmin Oh, Daehyeon Son, Hoseok Kwon, Philip Virgil Astillo, and Ilsun You. 2023. "APSec1.0: Innovative Security Protocol Design with Formal Security Analysis for the Artificial Pancreas System" Sensors 23, no. 12: 5501. https://doi.org/10.3390/s23125501

Note that from the first issue of 2016, this journal uses article numbers instead of page numbers. See further details here.

Article Menu

APSec1.0: Innovative Security Protocol Design with Formal Security Analysis for the Artificial Pancreas System

Abstract

1. Introduction

2. Related Works

3. Proposed Protocol

3.1. Security Requirement

3.2. Assumptions

3.3. Proposed Protocol

3.3.1. Registration Phase

3.3.2. Communication Phase

3.3.3. Emergency Phase

4. Formal Verification

4.1. BAN Logic

4.1.1. Idealization

4.1.2. Assumptions

4.1.3. Goals

4.1.4. Derivation

4.2. AVISPA

4.3. Discussion

4.3.1. Security Analysis

4.3.2. Overhead Analysis

5. Experiment

6. Conclusions

Author Contributions

Funding

Institutional Review Board Statement

Informed Consent Statement

Data Availability Statement

Conflicts of Interest

References

Share and Cite

Article Metrics

Article Access Statistics

Further Information

Guidelines

MDPI Initiatives

Follow MDPI