Formal Verification of Access Control Model for My Health Record System

TL;DR

This paper formally specifies and verifies the access control mechanisms of Australia's My Health Record system using Event-B to ensure compliance with legislative privacy requirements.

Contribution

It introduces a formal specification and verification approach for the access control model of My Health Record based on legislative rules.

Findings

Verified that the system enforces access control policies.

Proved compliance with privacy legislation.

Demonstrated correctness of access control mechanisms.

Abstract

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.