我的健康记录系统访问控制模型的形式化验证
软件工程
2020-06-15 v1 密码学与安全
摘要
我的健康记录系统（My Health Record system）是澳大利亚政府的数字健康记录系统，持有我的健康记录（My Health Record）。我的健康记录是一种安全的在线健康记录，包含消费者的健康信息。该系统旨在为医疗专业人员提供对关键健康信息的访问，例如所列药物、过敏与关键诊断；放射与病理检测结果。该系统（前称个人控制电子健康记录）使消费者能够决定如何与任何在其注册并接入系统的医疗提供者共享信息。我的健康记录系统在澳大利亚立法框架《2012 年我的健康记录法》（My Health Records Act 2012）下运行。该法案尤其确立了隐私框架，规定哪些实体可收集、使用与披露系统中的特定信息，以及对不当收集、使用与披露该信息可施加的处罚。本文给出（源自立法的）形式化规约并验证我的健康记录中关于消费者如何控制谁可访问信息，以及系统如何遵循此类访问。我们依赖构造即正确的 Event-B 方法来证明系统的控制与访问属性。
引用
@article{arxiv.2006.06933,
title = {Formal Verification of Access Control Model for My Health Record System},
author = {Victor Rivera},
journal= {arXiv preprint arXiv:2006.06933},
year = {2020}
}