论文标题
对我的健康记录系统的访问控制模型的正式验证
Formal Verification of Access Control Model for My Health Record System
论文作者
论文摘要
我的健康记录系统是澳大利亚政府的数字健康记录系统，它拥有我的健康记录。我的健康记录是包含消费者健康信息的安全在线健康记录。该系统旨在为医疗保健专业人员提供关键健康信息的访问，例如列出药物，过敏和关键诊断；放射学和病理测试结果。该系统（以前命名为个人控制的电子健康记录）使消费者可以决定如何与已注册并连接到系统的任何医疗保健提供者共享信息。我的健康记录系统根据《 2012年澳大利亚立法框架》的《 2012年《健康记录》法案运行。本文介绍了（根据立法）的正式规范以及对我的健康记录的验证，内容涉及消费者如何控制谁访问信息以及系统如何遵守此类访问。我们依靠正确的构造事件-b方法来证明系统的控制和访问属性。
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.
