Formal Verification of Access Control Model for My Health Record System
This work addresses privacy and security concerns for users of a national digital health record system, but it is incremental as it applies an existing formal verification method to a specific domain.
The paper tackled the problem of ensuring secure access control in Australia's My Health Record system by formally specifying and verifying consumer control and system adherence to access rules, using the Event-B method to prove properties.
My Health Record system is the Australian Government's digital health record system that holds My Health Record. My Health Record is a secure online health record containing consumers' health information. The system aims to provide health care professionals with access to key health information, e.g. listing medicines, allergies and key diagnoses; radiology and pathology test results. The system (previously named Personally Controlled Electronic Health Record) enables consumers to decide how to share information with any of their health care providers who are registered and connected to the system. The My Health Record system operates under the Australian legislative framework My Health Records Act 2012. The Act establishes, inter alia, a privacy framework specifying which entities can collect, use and disclose certain information in the system and the penalties that can be imposed on improper collection, use and disclosure of this information. This paper presents the formal specification (from the legislation) and verification of the My Health Record regarding how consumers can control who access the information, and how the system adheres to such access. We rely on the correct-by-construction Event-B method to prove control and access properties of the system.