On the design and analysis of protocols for Personal Health Record storage on Personal Data Server devices

The electronic Personal Health Records (PHRs) such as medical history, lab reports, and insurance are stored in systems such as Microsoft Health Vault where a medical care provider or a patient is responsible for uploading and managing the health information. Storing PHRs in such a manner prohibits the patients from having complete control over their data and also may make the PHR system the target of security attacks. Towards this end, we proposed a new architecture, namely Personal Data Server overlay, where the data is stored on a set of Secure Portable Tokens (SPTs) that are under the control of individual users. SPTs are cheap, portable, and secure devices that combine the computing power and tamper-resistant properties of the smart cards and the storage capacity of NAND flash memory chips and they can act as a Personal Data Server (PDS). We need formal assurance of data availability when information is stored in PDS overlays. Thus, data must be replicated at multiple PDSs. We propose a data replication protocol that ensures that the PHRs for each user have replicas in the PDS overlay. It is crucial to ensure correctness of the data replication protocol. Consequently, we formalize the protocol using the Unified Modeling Language (UML) and specify a number of desirable properties. We need to provide formal assurance of these properties in an automated manner. We demonstrate how the UML model can be transformed into Alloy using the UML-to-Alloy transformations. This obviates the need for the protocol designer to know Alloy. The analysis uncovers a significant error in the protocol. Uncovering such errors help refine the protocol and ensures its correctness before deployment. (C) 2016 Elsevier B.V. All rights reserved.