Formal Analysis of an E-Health Protocol
This work addresses privacy and security issues in e-health protocols, which is critical for protecting sensitive health data, but it is incremental as it builds on existing protocol analysis.
The paper tackled the problem of ensuring doctor privacy in e-health systems by formalizing new privacy properties and analyzing the DLV08 protocol, uncovering ambiguities that lead to security and privacy flaws and proposing fixes.
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.