Formal Analysis of an E-Health Protocol

TL;DR

This paper formally analyzes an e-health protocol to identify privacy and security flaws, proposing fixes to ensure stronger privacy guarantees like doctor privacy, anonymity, and untraceability.

Contribution

It introduces formal privacy properties for doctor privacy and analyzes a practical e-health protocol, revealing ambiguities and security flaws, and suggests improvements.

Findings

Identified ambiguities in the protocol

Showed the protocol's failure to satisfy certain privacy properties

Proposed fixes to enhance security and privacy

Abstract

Given the sensitive nature of health data, security and privacy in e-health systems is of prime importance. It is crucial that an e-health system must ensure that users remain private - even if they are bribed or coerced to reveal themselves, or others: a pharmaceutical company could, for example, bribe a pharmacist to reveal information which breaks a doctor's privacy. In this paper, we first identify and formalise several new but important privacy properties on enforcing doctor privacy. Then we analyse the security and privacy of a complicated and practical e-health protocol (DLV08). Our analysis uncovers ambiguities in the protocol, and shows to what extent these new privacy properties as well as other security properties (such as secrecy and authentication) and privacy properties (such as anonymity and untraceability) are satisfied by the protocol. Finally, we address the found ambiguities which result in both security and privacy flaws, and propose suggestions for fixing them.