Symmetric key-based patient controlled secured electronic health record management protocol

Abstract

In our progressive era of technology, digitization is becoming the link between businesses, people, processes, and data. Since digitization is now a common practice for storing and retrieving data, Electronic Health Record (EHR) management services are rapidly becoming popular as it allows users to store and access their data anywhere at any time. EHR management is bringing many benefits including easy storage, cost effectiveness, shareable with health professionals to a remote location, etc. However it is very challenging to adopt cloud-based EHR services, due to the risk of data breaches and the resulting compromise of patient data. Since EHR stores very sensitive data, a number of security properties including privacy, secrecy, integrity, authenticity and availability of data must be ensured during data transmission, storing and sharing with health professionals. In this study, we have studied symmetric key based technique in designing EHR management protocol. The protocol allows the patient to handle the responsibility of authorizing data access, thus this is a patient-centric protocol. Attributes (e.g., specialization, location, affiliated hospital, etc.) of a health professional is used to delegate access to EHR of a patient, and thus attribute-based access control has been achieved. The protocol we have designed is then validated using AVISPA, an industry-strength security protocol validation tool. AVISPA has confirmed our protocol free from known attacks and confirmed the desired security properties as well.

Keywords

Electronic Health Record (EHR)secured EHR AVISPA patient-controlled

1. Introduction

As Internet is becoming an intricate part of our day to day life, it is now a common practice to use its benefits and advantages to make life easier. Technology and the digital revolution are bringing benefits in many ways by providing a platform that connects people from across the globe. This might require individuals to share their private information demanding the data to be kept secured in a simple yet secured way. As the information are vulnerable to security exploits and data theft if remote servers leave the data open [32], the valuable information requires confidentiality, security and privacy [26,35]. Among the many benefits of improved technology, Electronic Health Record (EHR) management is one.

EHR is any health related information or data of patient stored digitally using electronic methods maintaining top notch security to assure privacy. This information can only be accessed instantly by authorized users, e.g., doctors or the patients themselves. EHR contains sensitive information including patients’ medical and treatment histories, administrative and billing data, prescriptions provided by the doctors, medical test reports, personal information (e.g., age, weight and height), etc. Security and privacy is the prime concern as EHR contains valuable information. The EHR system can also be created to go further than typical clinical data collected in a medical institution and can add various other facilities to allow a broader view of a patient’s care [7]. For example it can allow access to tools to help doctors in making decisions about a patient’s care. As EHRs are stored digitally they can be easily shared from one place to another through electronic media via connected private networks, e.g., from one branch of a hospital to another distant branch [39]. Security and privacy are essential not only for patient health information but also for clinical care, research, payment, and healthcare policymaking. Thus various cryptographic protocols that use cryptographic techniques have been developed to achieve secured management of EHR. Various initiatives have been formed to establish the definition of standard methods for secure and inter-operable EHR exchanges, e.g., Integrating the Healthcare Enterprise (IHE) [20].

Fig. 1.

General EHR management architecture.

EHR management architecture models the system that makes it feasible to store and transfer EHR. A general and very basic EHR management architecture is shown in Fig. 1 where ‘doctor’, refers to any health professionals in general. The patient updates or stores the medical records after receiving treatment from doctor-1. The patient can also authorize doctor-1 to store the medical records on behalf of the patient to a remote EHR server. This same patient might get referred to doctor-2 for further medical treatment. Doctor-2 can view the patient’s previous record after the patient grants doctor-2 the access to data at the EHR server. This model is extended to enhance the structure in various ways to suit the need and meet the objectives of protocols or designs, applied in various works. For example [19] illustrates the incorporation of encryption-decryption function along with transaction code (TAC) service and private key generator (PKG) to provide flexibility with security.

Below we have summarized the required security properties that generally a secured EHR management should support.

Privacy and Secrecy: Patient privacy and secrecy is crucial while records on remote servers leave the data open to security exploits and data theft [32]. Encryption is usually applied to ensure secrecy [19].

Integrity: Integrity, internal consistency, and accuracy of information in the patient’s EHR are imperative to ensure accuracy of the health record [5]. It involves information such as patient identification, authorship validation, amendments and record corrections.

Access Control: The purpose of authentication is to allow authorship and assign responsibility for an act, event, opinion, or diagnosis made by the doctor [5]. Entries in the healthcare record should be authenticated by the patient [26]. Patient can permit or reject sharing their information with other healthcare practitioners [19]. To implement patient consent in a healthcare system, patient may grant permissions to users on the basis of a role or attribute held by the respective user [35].

Availability: It is essential for any EHR system to be available and provide the accessibility of information when it is needed [5]. This means that the computing systems used to store and process the EHR data, the security controls used to protect it, and the communication channels must be operating properly and are reachable all the time.

In our research, we have developed a simple symmetric key based EHR management protocol. The initial version of this EHR management protocol was published in [23]. In this study, we focus to combine the advantages of attribute-based access control and the simplicity of symmetric key-based encryption and authentication. Note that the idea of attribute-based access control is adopted from Attribute-Based Encryption (ABE), which has been first introduced in [17,33] to store and share encrypted data based on public-key. In ABE, the decryption key is associated with the ciphertext through some attributes [17]. If A encrypts data using $K_{A}$ to generate the ciphertext, B can decrypt this data using $K_{B}$ , only if there is a match between the attributes of the ciphertext and B’s key, $K_{B}$ . In this system, the sender, A or the encryptor selects a set of attributes to be associated with the ciphertext. The receiver, B can decrypt data using its secret key only if the attributes of $K_{B}$ matches with those selected attributes. Thus, it was termed as Attribute-Based Encryption (ABE).

The protocol we have developed is patient controlled meaning only the patient-authorized health professional (e.g., a doctor) will have access to the patient’s EHR. Moreover, there will be fine grained access control, i.e., access control will be both doctor and health record specific. Although our proposal is primarily based on symmetric key, it identifies the doctors using their attributes [19,28]. We have developed protocols for both data storage and retrieval. The security properties of this protocol have been validated by modeling the protocol using Automated Validation of Internet Security Protocols and Applications (AVISPA) [3]. AVISPA is an automatic tool with industrial-strength technology for the investigation of different Internet security protocols and applications [14]. It is used equally by the developers of diverse security protocols and by academics [21,22]. In our validation, AVISPA testified the proposed protocol free from attacks.

The rest of the paper is organized as follows: Section 2 presents the existing solutions and our motivation of this work. Section 3 depicts the proposed architecture and protocols for EHR management. Section 4 introduces AVISPA briefly and then presents the model we have developed for the proposed EHR management. The results of security protocol analysis provided by AVISPA are also shown. Finally, Section 5 concludes the paper by summarizing the contribution of this paper.

2. Related work and motivation

The vast researches so far in securing EHR have taken various diverse approaches with focus on different areas of the total EHR management system. Some have worked with a focus on modeling and testing a proposed protocol that confirms only secrecy property or other security property requirements. While others have extended their work with a deeper evaluation study and actually verified the systems and tools within healthcare systems to examine if it supports the real life implementation or integration [29].

2.1. Classical cryptography based solutions

For wireless medical sensor networks (WMSN), a two-factor authentication protocol for health-care applications has been proposed that allows the users to be anonymous [40]. The security weaknesses and efficiency of this protocol are further improved in [36] by designing an efficient symmetric key based authentication protocol. Privacy of patient’s data is provided by ensuring secured and authorized communication in WMSN which consists of distributed sensors. The security of the proposed protocol is analyzed using a formal security proof algorithm to show the scheme is secure and is also verified by AVISPA.

A secure communication protocol between a patient at home and a doctor at a clinical center in Telecare Medical Information System (TMIS) has been designed in [2] using user authentication for the medical servers. Using cryptographic, one-way hash function, this protocol proposed a smart card based user authentication and key agreement protocol for TMIS system allowing access to several medical services of the multi-medical server. Thus, a user is able to directly communicate with the doctor of the medical server securely. The security properties of the proposed authentication scheme has been analyzed using AVISPA.

An anonymity-preserving remote user authentication protocol that uses the personal biometrics of a user, her password and the smart card is presented in [11]. The user’s biometrics is verified using BioHashing. Further efficiency of this protocol is achieved by using collision-resistant, one-way hash function and exclusive-or (XOR) operations. Several security flaws of this protocol including flaws in login and authentication, password change, protection from privileged insider attack and man-in-the middle attack have been addressed in an improved version [13]. The security analysis of the improved version has been carried out using AVISPA to prove the security of the protocol against possible passive and active attacks.

In [12] a secure and efficient password-based remote user authentication scheme using smart cards for the integrated Electronic Patient Record (EPR) information system is proposed using one-way hash function and bitwise exclusive-or (XOR) operations. This scheme overcomes the security weaknesses such as design flaws in password change phase, failures to protect privileged insider attack and lackings in the formal security verification found in the previously proposed protocol in [27] and [38]. This protocol also establishes a symmetric secret session key between the user and the server for their future secure communications. Security analysis and formal security verification are carried out using AVISPA to show the scheme is secure against passive and active attacks.

A security model has been proposed in [18] to sustain patient’s privacy and data confidentiality by using pseudonymization. In this method, both health records and patients’ information are given randomly-selected pseudonyms, which act as access tokens and allow linking of the health record with the patient. The pseudonyms are encrypted with a patient-specific secret key. Thus the authorization model is patient-centric. The patient is labeled as the data owner who maintains full control over his or her health data and is able to delegate access authorizations to trustworthy persons for particular health record. Micro controller smart-cards with integrated crypto chips are used for secured authentication. Both symmetric key and asymmetric key encryption are used in the model to provide authentication and authorization layers. This pseudonymization protocol is validated using AVISPA and is also practically demonstrated by developing a prototype. Note that pseudonymization requires a sufficiently large number of individuals and records to be effective. Moreover, it requires trustworthy depersonalization for certain kinds of health data, which can be quite difficult.

Hierarchical Key Assignment Scheme (HKAS) [8–10] is a fine-grained access control mechanism where users or participants are organized in hierarchies formed by a certain number of disjoint classes. HKAS provides some encryption keys and private information to the users of a higher class. Using that private information, the users of a higher class can derive the keys of all lower classes that are descendent of that higher class. HKAS can be successfully used for access control to selective users where hierarchy exists inside the system such as database management systems, computer networks, operating systems, military and government communications, etc.

2.2. ABE based solutions

In ABE, access policy is encoded either into the receiver’s secret key (known as Key-Policy Attribute-Based Encryption (KP-ABE)) or into the ciphertext (known as Ciphertext-Policy Attribute-Based Encryption (CP-ABE)). In KP-ABE, assume that $(A \land B) \lor (A \land C)$ has been encoded into the user’s secret key as access policy. Now, a receiver would be able to decrypt a ciphertext if it were encrypted with respect to the set of attributes ${A, C}$ , but would not be able to decrypt if it were encrypted with respect to the set of attributes ${B, C, D}$ . In CP-ABE, the access policy is specified into the ciphertext over a defined universe of attributes. A user, whose attributes satisfy the policy of the respective ciphertext can decrypt the ciphertext. Assume that a ciphertext is encrypted with respect to the policy $(A \land B) \lor C$ and the universe of attributes is defined to be ${A, B, C, D}$ . Now, if user-1 and user-2 receive their keys to attributes ${A, B}$ and ${B, D}$ , respectively, then only user-1 will be able to decrypt.

ABE has been incorporated in various forms to provide a secure EHR environment and flexible desired access control [19,28]. For example, [28] focuses on allowing a patient to be able to provide access to their health data based on the attribute (e.g., profession, specialization, location, etc.) of the users and also control what portions of the medical data a patient wants to share. [1] has presented a design and implementation of Electronic Medical Records (EMRs) using attribute based encryption on mobile devices. In [31], the situation where multiple data owners exist is considered and patient’s Personal Health Records (PHR) are encrypted and stored in semi-trusted servers proposing a privacy-preserving multi-authority CP-ABE scheme. Recently to overcome current EHR server limitations two approaches are explored which guarantee the security and flexibility of sharing EHR on the cloud, by proposing a new architecture called Crypt-EHR server which combines attribute based cryptography and CryptDB SQL query-searchable encryption [41].

In [25], a cloud-based EHR management solution is developed to guarantee a secure, encrypted access control and patient data security mechanism. It incorporates a semantically rich, policy based approach using Attribute Based Access Control (ABAC) [24] to contemplate a person’s access and use ABE to encrypt and store the patient EHRs. ABAC is a policy-based access control where policy, by combining different types of attributes (e.g., user attributes, resource attributes, object, environment attributes etc.), grants access rights to users.

To implement secure access control and attribute based encryption, the system extracts the user and EHR field attributes from a knowledge graph that details the roles and attributes of the different stakeholders of the medical organization along with the various relationships between them. [37] presents a secure EHR management system using ABE and Identity-Based Encryption (IBE) to encrypt medical data. IBE [34] is a flexible, public-key based encryption that does not depend on traditional certificate distribution. It can compute the public key of an entity from some general, public parameters and an identity of the entity including e-mail or telephone number. To compute the corresponding private key, Private Key Generator (PKG), a trusted third-party is needed. Once an entity receives its private key from the PKG, the entity may generate its digital signature. This digital signature is verifiable by a recipient and no certificate is needed for this process. This is known as Identity-Based Signature (IBS). Note that [37] used IBS to implement digital signatures, and blockchain technology to ensure integrity, traceability and confidentiality.

2.3. Selecting appropriate cryptographic techniques and tools

The security requirements of our proposed EHR management protocol are presented in Section 3.1.2. In designing the proposed protocol we have selected the appropriate cryptographic techniques and the validation method. In the literature, both classical cryptographic techniques (i.e., symmetric or public key based encryption, hash function, etc.) and ABE or variants of ABE (e.g., KP-ABE, CP-ABE, etc.) are widely used. The primary advantage of ABE is fine-grained access control through attributes of the users. Thus, a patient has control over her privacy and she can share a specific health data to a specific or a group of health professional(s). In spite of its different attractive features ABE based protocols are only used in mathematical and theoretical research community but have not experienced the wide scale deployment in day to day applications yet. According to [42], not all ABE based solutions have been implemented and only few of them have up-to-date libraries. On the other hand, classical cryptographic techniques are being used in numerous applications for a longtime. Open-source implementations of these techniques are readily available. Therefore, in our proposed EHR management protocol we used symmetric key based encryption, i.e., a classical cryptographic technique. However, in our design we have also successfully incorporated the attribute-based access control. Note that although [18] has some similarities with our security requirements, they have not presented any detailed protocols or validation model. To the best of our knowledge, this is the first comprehensive work that developed an attribute-based, patient-centric access control using symmetric key encryption.

We congregated research work that is similar to our pursuit of EHR involving AVISPA for validation of security properties. We have mentioned a few including [2,6,13,18,36]. Note that AVISPA has been used by wide variety of protocols in many other study work for validation of security properties [21,22,30]. Therefore, we have also selected AVISPA in validation of the security properties of our protocols.

Fig. 2.

Proposed EHR management architecture.

3. Proposed electronic health record (EHR) management protocol

A general and very basic EHR management architecture is already shown in Fig. 1. By extending that EHR management architecture we have structured our proposed EHR architecture.

3.1. Proposed architecture

The structure of our proposed EHR architecture is given in Fig. 2 depicting that the EHRs are stored centrally in a data store (DS) by a doctor after receiving the authorization permission from a patient. The patient can store data by herself or give permission to a local health professional (Doctor-1) or a remote health professional (Doctor-2) to store. In our model, we have introduced a key server (KS) that shares or provides the encryption key (K) to the doctor, if the doctor has been approved by the patient (P). This key, (K), is used to encrypt the patient’s data before storing in the data store. We have developed a very simple architecture that only focuses on storing data and retrieving data by the patient’s authorized doctors, incorporating attribute-based access control in symmetric-key solution.

3.1.1. Threat model

A threat model is used to identify and express the underlying threats in a security system. In the following we summarize the threats we have anticipated in the proposed EHR management protocol. We have identified the following three areas where the intruder can attempt to attack:

Communication channels: We consider the Dolev-Yao [15] channels for communications. All communication channels are considered to be a part of the public networks (e.g., the Internet). Thus, the communication channels are subjected to be attacked by the intruders. An intruder or attacker can see all the messages transmitted through these channels and has complete control over message transmission. The intruder can intercept, copy and synthesize any message, and his actions are only restricted by the restraints of the cryptographic methods used.

Playing role of an entity: In our threat model, the key server (KS) and the data store (DS) are considered as trusted entities. Hence the intruder is not granted to play the roles of these two entities. Attackers or intruders are able to play the roles of the doctor or the patient.

Strength of cryptographic primitives: The hash and encryption functions being used are considered as secured and thus are not breakable by the intruder.

3.1.2. Security requirements

The proposed protocol has been aimed to maintain the following security requirements (SR):

SR1: Patient will control the access of his or her EHRs. Only patient-authorized health professional (e.g., a doctor) will have access to the EHR. A patient can define a set of attributes (A). Any doctor with such attribute will have access to EHR of that patient.

SR2: Access control will be both doctor and health record specific, i.e., a doctor D will only have granted access to patient’s health record matching a record-specific transaction code (TAC).

SR3: Although symmetric encryption will be used, an indirect authentication of the doctor will be performed by the key server (KS) based on the doctor’s attributes.

SR4: Data encryption key (K) will be generated by the key server and will only be sent to the authenticated doctor. This key will only be known by the key server and the doctor.

SR5: EHR will only be known by the patient and the authorized doctor.

3.2. Proposed protocols

The proposed protocols are composed of two sub-protocols: data store and retrieve protocols. While designing the protocols, our target is to satisfy all the security requirements presented in the earlier section. At the same time, the threat model explained in Section 3.1.1 needs to be mitigated. Figures 3 and 4 show the data store and retrieval protocols, respectively.

Fig. 3.

The proposed protocol for storing data.

Fig. 4.

The proposed protocol for data retrieval.

The notations being used is the proposed protocol are shown in Table 1. To express the protocols we have used conventional Alice-Bob notation where, P -> D: TAC means the role, P sends the message, TAC to the role, D. In these messages, “{}” means encryption and “.” is used for concatenation. Thus, D -> KS: {D.P.TAC}_Kdks means D sends a message to KS that is encrypted using the symmetric key Kdks. Here, the recipient of a message must be the dispatcher of the next one.

Table 1

The notations being used in this proposed protocol

Notations	Meaning
P, D, KS, DS	Principals: Patient, Doctor, Key server and Data store
$Kchip$	Secret key written in the patient’s chip card
timestamp	Time of an instance
genTAC(), h()	One way function used to generate TAC and hash values
TAC	Transaction Code. Here, $TAC = genTAC (Kchip, timestamp)$
$Kdks$	A symmetric key between Doctor and Key server
$Kpks$	A symmetric key between Patient and Key server
$Kdds$	A symmetric key between Doctor and Data store
K	Data encryption key
A	Attribute set selected and shared by patient
EHR	Electronic Health Record to be stored

3.2.1. Involved principals

Four entities or principals are involved in this proposed protocol, which are mentioned in the following:

Patient (P): Carries a health card with secret key chip (Kchip).

Doctor (D): Generates EHR and stores encrypted EHR to the data store (DS).

Key Server (KS): Authenticates the doctor (D) based on attributes set (A) provided by the patient. Generates encryption key to encrypt EHR. Forwards the key to the authenticated and authorized doctor (D).

Data Store (DS): Stores encrypted EHR corresponding to each transaction code (TAC) and patient ID (P), however does not understand the content of the EHR.

3.2.2. Data store protocol

Data store protocol has five messages. In the following we have explained each message of the data storing protocol and how the message ensures the Security Requirements (SR).

Message 1: The patient generates the TAC, where TAC = genTAC(Kchip, timestamp), and then sends the TAC to the key server with the patient’s ID, P and the attribute set, A selected by the patient. This messages is encrypted with the symmetric key, Kpks, shared between the patient and the key server. Here, the TAC value will be unique for every transaction (i.e., storing or retrieving of data) due to the use of genTAC() function, Kchip and timestamp. On receiving this message, the key server creates an attribute set of tuples with P, member(s) of A and TAC. For example, if A = {D1, D2, D3}, then the tuples of the attribute set will be P.D1.TAC, P.D2.TAC and P.D3.TAC. This attribute set is used in Message 3. (SR1, SR2)

Message 2: The patient forwards this TAC to the doctor. We termed the doctor as doctor-1 for referencing in our proposed model. (SR1, SR2)

Message 3: The doctor sends the patient’s ID, P, doctor’s ID, D, and the TAC to the key server. This message is encrypted with the symmetric key, Kdks, shared between the doctor and the key sever. The key server then: (1) decrypts the received message using Kdks and matches the received TAC with the one sent by the patient earlier (SR2), and (2) checks if the tuple P.D.TAC is a member of its attribute set (as well as if D is a member of attribute set A). (SR1, SR3)

Message 4: The key server generates the data encryption key, K, where K = h(P.TAC.Kpks), and then forwards K to the doctor encrypted with Kdks. (SR4)

Message 5: Finally, the doctor encrypts EHR with the data encryption key, K, and sends the encrypted EHR to the data store to be saved in. The message is encrypted with the symmetric key, Kdds, shared between the doctor and the data store. (SR5)

3.2.3. Data retrieval protocol

In the following we have explained the messages of the data retrieval protocol along with the Security Requirements (SR) achieved by the messages. Note that data retrieval protocol can only be executed after the successful completion of the data store protocol.

Message 1: The patient sends the TAC to the doctor, D, selected by the patient. The doctor in this step could be the same doctor (e.g., doctor-1) from the data storing stage or could be a new doctor selected by the patient (e.g., doctor-2). Here, TAC has the same value that was generated and stored by the patient during data storing. (SR1, SR2)

Message 2: The doctor sends the patient’s ID, P, doctor’s ID, D, and the TAC to the key server. The message is encrypted with the symmetric key Kdks. The key server then: (1) decrypts the received message using Kdks and matches the received TAC with the one sent by the patient earlier (SR2), and (2) checks if the tuple P.D.TAC is a member of its attribute set (as well as if D is a member of attribute set A). (SR1, SR3)

Message 3: The key server generates the data encryption key, K, where K = h(P.TAC.Kpks), and then forwards K to the doctor encrypted with Kdks. (SR4)

Message 4: The doctor sends the patient’s ID, P, and the TAC to the data store. This message is encrypted with the symmetric key, Kdds. The data store checks if the encrypted data corresponding to the tuple P.TAC is present in its database. (SR5)

Message 5: The data store sends the encrypted EHR to the doctor. This message is encrypted with the symmetric key, Kdds, shared between the doctor and the data store. (SR5)

4. Security model development

We have developed and verified our proposed model using AVISPA tool. The procedure used in the development model, steps with which we conducted the verification, the model and its output is described in details in this chapter. We have developed two separate AVISPA models for data storing and data retrieval protocols.

4.1. AVISPA

AVISPA is a specialized model checker for security protocols, used to verify that any proposed protocol is free from security threats. AVISPA does not evaluate the performance of the protocol under differing conditions and stresses that might help to conclude the efficiency or analyze performance of the protocol. AVISPA focuses solely on a protocol to deduce if it is totally secure or not. Ensuring the security of cryptographic protocols is the crucial function. It is a security protocol verification tool using fully automatic processes applying various analysis methods, permitting the user to use different tools for a single protocol modeling. Security protocol designs are further aided with the use of a graphical user interface Security Protocol Animator (SPAN) [16].

4.1.1. Architecture of AVISPA

AVISPA uses modular and expressive formal language to specify a protocol and its security properties. It depends on its back-ends, which use an automatic analytic technique to discover the existence of any flaws. The architecture of AVISPA is shown in Fig. 5. In AVISPA, protocol roles are modeled in the High-Level Protocol Specification Language (HLPSL) as state transition systems. The HLPSL2IF tool transforms an HLPSL specification into an Intermediate Format (IF), a transition system of infinite state. This IF specification is being scrutinized by any of the four back-end tools, namely, On-the-Fly Model-Checker (OFMC), Constraint-Logic-based Attack Searcher (CL-AtSe), SAT-based Model Checker (SATMC) and Tree Automata-based Protocol Analyzer (TA4SP).

Fig. 5.

Architecture of the AVISPA tool [4].

4.1.2. Modeling roles in AVISPA

HLPSL is a role-based language where for every participant in a protocol, there exists a basic role with his sequence of actions through transitions. A transition in HLPSL specification denotes the receipt of a message (RCV) and the sending of a reply message (SND). After a basic role is defined, composed roles are needed to be defined which describe sessions of the protocol. A composed role instantiates one instance of each basic role. Thus describing one whole protocol session. By convention, such a composed role is termed session(). In the session() role, all the channels used by the basic roles are stated. Next, environment() is a top-level role containing global constants, a formation of one or more sessions and also a statement describing the initial knowledge of an intruder. In the environment() role, a number of sessions are instantiated corresponding to the composed role session().

4.1.3. Security goal specification

By means of the back-end tools of AVISPA, secrecy and various forms of authentication goals could be validated. AVISPA supports four types of goal predicates: witness, wrequest (for weak authentication), request (for strong authentication) and secret. These predicates are used to lay down the security goals, namely, secrecy and authentication.

Secrecy is tested with the help of the goal predicate secret(E, id, S), which confirms that the secret information E should be known only by the agents of set S. The label id (of type protocol_id) is used to identify the goal. In the HLPSL goal section, the statement secrecy_of id should be given to refer to it. If the intruder learns a value, which he is not allowed to know and is considered as secret, the secrecy property is violated.

Authentication is confirmed using the goal predicates: witness(A, B, id, E) and request(B, A, id, E). The witness predicate is used for authentication of A by B on E. This is the verification that A is a witness for the information E. The request predicate states that B requests A for an inspection of the value E. The authentication property is conveyed in the goal section, which is written as authentication_on id. If any back-end tools discovers a trace in which the request event is preceded by a witness event initiated by an agent other than A, an attack will be informed. Furthermore, an attack trace will also be reported if no valid witness is found for a request.

Fig. 6.

Roles of patient (P) and doctor (D) in data store protocol.

Fig. 7.

Roles of key server (KS) and data store (DS) in data store protocol.

Fig. 8.

Functions session() and environment() in data store protocol.

4.2. Validation model

In the AVISPA model we have developed, there are four agent roles: patient (P), doctor (D1 and D2), keyserver (KS) and datastore (DS). Figures 6 and 7 demonstrate the HLPSL specification that we have developed to model these four roles for data storing protocol. Inside these roles, the messages shown in Fig. 3 for data storing protocol have been modeled. Moreover, all the notations shown in Table 1 have been used in HLPSL code. Note that we have assumed two doctor roles, D1 and D2. D1 is authorized by the patient (P) and thus is present in the attribute set (A) provided by P. D1 is storing the patient’s data to the data store (DS). On the other hand the remote doctor D2 is authorized by the patient to retrieve data. Since we are showing data storage protocol only, D2 is not shown in our HLPSL code.

HLPSL supports numerous basic data types. In the following, we list the data types that are used in our developed model:

agent indicates the principal names. The exclusive identifier i indicates the intruder.

const denotes the constants.

symmetric_key means the key for a symmetric-key cryptosystem.

text is often used for nonces and sometimes for messages.

nat denotes the natural numbers in non-message contexts.

Moreover, we used associative “.” operator for concatenation. The declarations “played_by P” is used to indicate that the agent named P plays the role. Transitions are of the form X =|> Y, relates an event X and an action Y.

These basic roles have been instantiated through the composed role, session.

Four parallel sessions have been started inside the environment role. Figure 8 shows the session and environment roles.

AVISPA is able to validate the secrecy of any message component. As we have mentioned in Section 3.1.2, data encryption key (K) and EHR should be known by specific agents. To validate the secrecy of these two parameters, the HLPSL goal secrecy_of and the following two secret facts have been added:

secret(K’, sec_k,{KS,D1})

secret(EHR, sec_ehr,{D1})

Here, the labels sec_k and sec_ehr identify the goals and {KS,D1}, {D1} are the sets of agents that are allowed to learn the value K and EHR respectively.

4.2.1. Modeling attributes in AVISPA

According to ABE-based authentications, the patient should have provision to select the attributes of the doctor or hospitals, based on which the doctor will be allowed to access the patient’s EHR. While modeling matching of the attributes, we use compound data type set. We declare two sets–A and Attributes–where A is a set of agents and Attributes is a set of 3-tuple that is a compound type of agent.agent.message. In the session role, we initialize these two sets:

init A := {d1, d2, c1, c2} /\ Attributes := {d1.p.tac1, d2.p.tac1, c1.p.tac1, c2.p.tac1}

Here, we assume that d1, d2, c1, c2 are four identities of agents or health-care professionals who have been authorized by the patient to access his/her EHR. The set Attributes has been initialized with tuples that implement fine-grained attribute-based access control. For example, d2.p.tac1 illustrates that doctor d2 has permission to access EHR of patient p that has the TAC value tac1.

HLPSL provides a set membership function, in(), to check if an element or n-tuple is already a member of the set. For example, when the key-server receives D1.P.TAC1 from a doctor, it checks if D1 and D1.P.TAC1 are member of the sets A and Attributes respectively as shown in the following HLPSL codes taken from Fig. 7:

RCV({D1.P.TAC1}_Kdks) /\ in(D1,A) /\ in(D1.P.TAC1, Attribute) =|> State’:= 2 /\ K’:=H(P.TAC1.Kpks) /\ SND({K’}_Kdks)

4.2.2. Freshness, replay and MitM attacks

AVISPA supports a new() function that produces a fresh value at runtime. To ensure the freshness of time, we use the new() function inside the patient role that generates the timestamp (Tstamp), as shown in Fig. 6. Note that in a transition, a primed variable (e.g., Tstamp’) denotes the new value of the variable, i.e., Tstamp. This new value has been either received in the left-hand side or assigned in the right-hand side of the transition. An active intruder, playing concurrently the role of any communicating node, has been introduced. First the intruder_knowledge has been added in the environment() role with the following command:

intruder_knowledge = {p,d1,ks,ds,gentac,kichip,kipks,kidds,kidks}

Following our threat model, the intruder has been assumed to have the capability to play the roles of the doctor or the patient, but not the roles of the key server and datastore. Therefore, the intruder shares necessary keys (i.e., kichip,kipks,kidds,kidks) with the key-server and the datastore as well. Moreover, it knows the TAC generating function, gentac.

Inside the environment() role, we have instantiated the four parallel sessions, where:

To find the existence of any replay attack, we instantiate the first two identical session()s.

The intruder is playing the roles of the doctor and the patient in the last two session()s. Hence, the agent identities p and d have been replaced by the intruder identity, i. This will also detect if any Man-in-the-Middle (MitM) or connection hijack attacks exist.

4.3. Model validation and result analysis

We use SPAN (Security Protocol Animator) [16], a graphical tool that provides the message sequence charts (MSC) showing the simulations steps of all messages. Figure 9 shows the protocol simulation of the model we have developed for data storing.

Fig. 9.

Protocol simulation of the model for data storing.

During protocol simulation no intruder’s role has been added. The sequences of the MSC confirm that the model we have developed is successfully exchanging all messages. AVISPA supports Dolev–Yao channels [15] (denoted by channel(dy) in the roles) for message transmission. As we have already mentioned, we have added an active intruder who can perform the roles of the patient and the doctor simultaneously, during the verification of the model. We have verified our model using all four back-ends of AVISPA to discover if any attack exists. AVISPA cannot concurrently identify several attacks during a single run. Therefore, we have confirmed the security goals one-by-one.

Using hlpsl2if, the HLPSL specification of our protocol is first converted into an intermediate format, called the Intermediate Format (IF). The output format (OF) of AVISPA is created using one of the back-ends. The analysis of the OF is as follows:

SUMMARY: Informs whether the tested protocol is secure, insecure, or the test is indecisive.

DETAILS: States what conditions of the test were taken into consideration to declare the protocol is safe or liable to get attacks or the test to be indecisive.

PROTOCOL: Shows the name of the protocol.

GOAL: Indicates the goal of the test.

BACKEND: Stands for the back-end name used in the test.

COMMENTS & STATISTICS: Displays the trace of an attack (if any present) printed in a standard Alice-Bob notation.

Fig. 10.

Validation output of OFMC for data store protocol.

The validation outputs of the two back-ends, OFMC and CL-AtSe, are shown in Figs 10 and 11. Both outputs for BOUNDED_NUMBER_OF_SESSIONS have reported the model SAFE. The other two back-ends, SATMC and TA4SP have reported NOT_SUPPORTED and gave INCONCLUSIVE results. We have to run OFMC with a bounded depth due to the intricacy of the model.

Fig. 11.

Validation output of CL-AtSe for data store protocol.

We conclude from the outputs that the AVISPA model we have developed is free from the attacks that AVISPA is able to find. Moreover, the secrecy security goal of the model that we have aimed to achieve in our protocol have been validated.

5. Conclusion

The major contribution of this paper is developing a symmetric key-based EHR management protocol. We have successfully introduced the attribute-based access control in symmetric-key solution for managing the access and data security of EHRs. Our system incorporates symmetric key along with a set of attributes in a unique way to create a new type of encrypted access control over these attributes that identifies which users are allowed to decrypt the encrypted data. Although the protocol we have developed is simple and has not considered many complexities that may arise during deployment in a real-life world, this AVISPA model of symmetric key-based protocol that also adds attributes can be extended to validate other complex EHR management protocols in the future.

The AVISPA model we have developed is only useful for validating security properties. However, it is not useful for performance study or determining how much overhead the security protocols will add. In future, we will focus on a comprehensive performance study with a comparative analysis of existing solutions.

References

J.A.

Akinyele,

M.W.

Pagano,

M.D.

Green,

C.U.

Lehmann,

Z.N.

Peterson and

A.D.

Rubin, Securing electronic medical records using attribute-based encryption on mobile devices, in: Proceedings of the 1st ACM Workshop on Security and Privacy in Smartphones and Mobile Devices, 2011, pp. 75–86, ACM.

Amin and

G.P.

Biswas, A novel user authentication and key agreement protocol for accessing multi-medical server usable in tmis, Journal of medical systems 39(3) (2015), 33. doi:10.1007/s10916-015-0217-3.

Armando,

Basin,

Boichut,

Chevalier,

Compagna,

Cuellar,

P.H.

Drielsma,

P.C.

Heám,

Kouchnarenko,

Mantovani,

Mödersheim,

von Oheimb,

Rusinowitch,

Santiago,

Turuani,

Viganò and

Vigneron, The AVISPA tool for the automated validation of Internet security protocols and applications, in: Computer Aided Verification,

Etessami and

S.K.

Rajamani, eds, Springer Berlin Heidelberg, Berlin, Heidelberg, 2005, pp. 281–285. doi:10.1007/11513988_27.

AVISPA v1.1 user manual, 2006, http://www.avispa-project.org/package/user-manual.pdf/.

R.C.

Barrows and

P.D.

Clayton, Privacy, confidentiality, and electronic medical records, Journal of the American Medical Informatics Association: JAMIA 3(2) (1996), 139–148. doi:10.1136/jamia.1996.96236282.

Benaloh,

Chase,

Horvitz and

Lauter, Patient controlled encryption: Ensuring privacy of electronic medical records, in: Proceedings of the 2009 ACM Workshop on Cloud Computing Security, 2009, pp. 103–114, ACM. doi:10.1145/1655008.1655024.

Blobel, Comparing approaches for advanced e-health security infrastructures, International Journal of Medical Informatics 76(5–6) (2007), 454–459. doi:10.1016/j.ijmedinf.2006.09.012.

Castiglione,

De Santis and

Masucci, Key indistinguishability versus strong key indistinguishability for hierarchical key assignment schemes, IEEE Transactions on Dependable and Secure Computing 13(4) (2016), 451–460. doi:10.1109/TDSC.2015.2413415.

Castiglione,

De Santis,

Masucci,

Palmieri,

Huang and

Castiglione, Supporting dynamic updates in storage clouds with the Akl–Taylor scheme, Information Sciences 387 (2017), 56–74, http://www.sciencedirect.com/science/article/pii/S0020025516307095 . doi:10.1016/j.ins.2016.08.093.

10.

Castiglione,

A.D.

Santis and

Masucci, Hierarchical and shared key assignment, in: 2014 17th International Conference on Network-Based Information Systems, 2014, pp. 263–270, ISSN 2157-0418. doi:10.1109/NBiS.2014.106.

11.

Y.-F.

Chang,

S.-H.

Yu and

D.-R.

Shiao, A uniqueness-and-anonymity-preserving remote user authentication scheme for connected health care, Journal of Medical Systems 37(2) (2013). doi:10.1007/s10916-012-9902-7.

12.

A.K.

Das, A secure and robust password-based remote user authentication scheme using smart cards for the integrated epr information system, Journal of medical systems 39(3) (2015), 25. doi:10.1007/s10916-015-0204-8.

13.

A.K.

Das and

Goswami, A secure and efficient uniqueness-and-anonymity-preserving remote user authentication scheme for connected health care, Journal of medical systems 37(3) (2013), 9948. doi:10.1007/s10916-013-9948-1.

14.

Deliverable D6.1: List of selected problems, 2005, http://www.avispa-project.org/delivs/6.1/d6-1.ps/.

15.

Dolev and

Yao, On the security of public key protocols, IEEE Transactions on Information Theory 29(2) (1983), 198–208. doi:10.1109/TIT.1983.1056650.

16.

Glouche,

Genet and

Houssay, SPAN: A Security Protocol ANimator for AVISPA, IRISA/Université de Rennes 1: Rennes, France, September (2008).

17.

Goyal,

Pandey,

Sahai and

Waters, Attribute-based encryption for fine-grained access control of encrypted data, in: Proceedings of the 13th ACM Conference on Computer and Communications Security, 2006, pp. 89–98, ACM.

18.

Heurix and

Neubauer, Privacy-preserving storage and access of medical data through pseudonymization and encryption, in: International Conference on Trust, Privacy and Security in Digital Business, 2011, pp. 186–197, Springer. doi:10.1007/978-3-642-22890-2_16.

19.

Hupperich,

Löhr,

A.-R.

Sadeghi and

Winandy, Flexible patient-controlled security for electronic health records, in: Proceedings of the 2nd ACM SIGHIT International Health Informatics Symposium, 2012, pp. 727–732, ACM. doi:10.1145/2110363.2110448.

20.

Integrating the Healthcare Enterprise (IHE) – IHE International, https://www.ihe.net/.

21.

Islam, Security analysis of LMAP using AVISPA, International journal of security and networks 9(1) (2014), 30–39. doi:10.1504/IJSN.2014.059325.

22.

Islam, Security property validation of the sensor network encryption protocol (snep), Computers 4(3) (2015), 215–233. doi:10.3390/computers4030215.

23.

Islam and

Farzana, Secured electronic health record management protocol, in: Proceedings of the International Conference on Imaging, Signal Processing and Communication, 2017, pp. 158–162, ACM.

24.

Jin,

Krishnan and

Sandhu, A unified attribute-based access control model covering DAC, MAC and RBAC, in: IFIP Annual Conference on Data and Applications Security and Privacy, 2012, pp. 41–55, Springer.

25.

Joshi,

Joshi and

Finin, Attribute based encryption for secure access to cloud based EHR systems, UMBC Information Systems Department Collection (2018).

26.

Katt,

Breu,

Hafner,

Schabetsberger,

Mair and

Wozak, Privacy and access control for ihe-based systems, in: International Conference on Electronic Healthcare, 2008, pp. 145–153, Springer.

27.

T.-F.

Lee,

Chang,

T.-H.

Lin and

C.-C.

Wang, A secure and efficient password-based user authentication scheme using smart cards for the integrated epr information system, Journal of medical systems 37(3) (2013), 9941. doi:10.1007/s10916-013-9941-8.

28.

Narayan,

Gagné and

Safavi-Naini, Privacy preserving EHR system using attribute-based infrastructure, in: Proceedings of the 2010 ACM Workshop on Cloud Computing Security Workshop, 2010, pp. 47–52, ACM. doi:10.1145/1866835.1866845.

29.

Palm, Rehabilitation at home of patients with neglect using a telemedical intervention: A security perspective, 2016.

30.

M.-L.

Pura,

V.-V.

Patriciu and

Bica, Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study, in: Proceedings of the 4th Conference on European Computing Conference, Bucharest, Romania, Vol. 2022, 2010, p. 200206.

31.

Qian,

Li,

Zhang and

Han, Privacy-preserving personal health record using multi-authority attribute-based encryption with revocation, International Journal of Information Security 14(6) (2015), 487–497. doi:10.1007/s10207-014-0270-9.

32.

J.J.

Rodrigues,

De La Torre,

Fernández and

López-Coronado, Analysis of the security and privacy requirements of cloud-based electronic health records systems, Journal of medical Internet research 15(8) (2013).

33.

Sahai and

Waters, Fuzzy identity-based encryption, in: Annual International Conference on the Theory and Applications of Cryptographic Techniques, 2005, pp. 457–473, Springer.

34.

Shamir, Identity-based cryptosystems and signature schemes, in: Workshop on the Theory and Application of Cryptographic Techniques, 1984, pp. 47–53, Springer.

35.

Shang,

Nabeel,

Paci and

Bertino, A privacy-preserving approach to policy-based content dissemination, in: Data Engineering (ICDE), 2010 IEEE 26th International Conference on, 2010, pp. 944–955, IEEE. doi:10.1109/ICDE.2010.5447902.

36.

Srinivas,

Mishra and

Mukhopadhyay, A mutual authentication framework for wireless medical sensor networks, Journal of medical systems 41(5) (2017), 80. doi:10.1007/s10916-017-0720-9.

37.

Wang and

Song, Secure cloud-based EHR system using attribute-based cryptosystem and blockchain, Journal of medical systems 42(8) (2018), 152. doi:10.1007/s10916-018-0994-6.

38.

Wen, A more secure anonymous user authentication scheme for the integrated EPR information system, Journal of medical systems 38(5) (2014), 42. doi:10.1007/s10916-014-0042-0.

39.

K.T.

Win, A review of security of electronic health records, Health Information Management 34(1) (2005), 13–18. doi:10.1177/183335830503400105.

40.

Wu,

Xu,

Kumari and

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

41.

Zhang,

Chow and

L.C.

Hui, Crypt-EHRServer: Protecting confidentiality with attribute-based encryption and encrypted query processing, in: Pervasive Systems, Algorithms and Networks & 2017 11th International Conference on Frontier of Computer Science and Technology & 2017 Third International Symposium of Creative Computing (ISPAN-FCST-ISCC), 2017 14th International Symposium on, 2017, pp. 234–241, IEEE.

42.

Zickau,

Thatmann,

Butyrtschik,

Denisow and

Küpper, Applied attribute-based encryption schemes, in: 19th International ICIN Conference-Innovations in Clouds, Internet and Networks-March, 2016, pp. 88–95.