The help of formal models for healthcare security policies.

This article is a personal contribution (i.e., from a strict security expert point of view) towards the help for specification, validation and/or evaluation of reliable, but also secure, healthcare security policies (HSP). The first part is dedicated to show, according to the various aspects of the security policy concept, that healthcare information systems (HIS) offer such a diversity of particularities and potential security needs, that it is necessary for healthcare security policies to be defined as flexible, but also as robust, as possible. Then the formal modelling approach, a wide area of solutions providing both flexibility (by means of modelling) and robustness (by means of formalization), is presented. The most well-known examples of security models are recalled. All of them try to use formal models as a security policy specification/validation tool, but none of them can be helpfully used in the very demanding context of HIS. Lastly, a new approach for the modelling of healthcare security policies, based on modal logic (i.e., epistemic and/or deontic logic) is proposed. It permits to take into account the flexibility (by means of high expressiveness due to modality) and the robustness (by means of high provability due to modelling) needs.