[Impressum] [E-Mail]

Modeling the German Electronic Health Card (EGK) (2)

The next step is to describe the components, data types and messages with UML class diagrams.

• Classes with the stereotype <<Terminal>>, <<Smartcard>>, <<Service>> or <<User>> describe components. This components have some attributes and associations to other data classes and use messages to interact with each other. We distinguish messages that are exchanged between a terminal and a smartcard / service or between two services (these are called messages) and messages that are exchanged between a user and a terminal (these are called usermessages). Messages are classes that are derived from a class with the stereotype <<Message>>, usermessages from a class with stereotype <<Usermessage>>. In this example the messages as well as the usermessages are defined in separate class diagrams (one for each protocol).
• The classes of the smartcard components (i.e. health card and Heilberufsausweis) are marked blue. The abstract class Heilberufsausweis is the superclass  of the classes representing the  Heilberufsausweis  of the doctor (HeilberufsausweisArzt) und the one of the pharmacist (HeilberufsausweisApotheker). The classes of the terminal components are marked green. These are the doctor's PC (ArztPC) and the pharmacy PC (ApothekenPC) which have a common abstract superclass LeistungserbringerPC. Also, the kiosk is modeled as a terminal. A kiosk is standing in a pharmacy and used by a patient to read and update his personal data on the health card. The user classes of the application are marked red. These are the patients, the doctors (Arzt), the pharmacists (Apotheker). The classes Arzt and Apotheker have an abstract common superclass called Leistungserbringer. The health insurance company (Krankenkasse) is modeled as a service, the class Krankenkasse is marked yellow. All other classes of the diagram below are marked orange and describe the data of the application. The enumerations define the possible states a component may be in and the class Constants defines the constants used in thes protocols.
• In the class diagram, the class ERezept represents an electronic prescription. An electronic prescription consists of three parts: the data of the prescription, e.g. name and  intake,  as well as  a nonce which is unique for each prescription, a digital signature of this data (issued by the doctors Heilberufsausweis) as well as the certificate of the doctor. The data of the prescription is stored in the class ERezeptdaten. The class ERezept has two associations to the clas ERezeptdaten. The association rezeptdaten stores the data itself, the association sig (annotated with<< signed>>) the signature of the data. The attribute zertifikatAusstellendeArzt of class ERezept stores the certificate of the doctor (resp. his Heilberufsausweis) who has issued the prescription. 
• Three security properties are modeled for the application and were verified interactively using the theorem prover KIV. The properties are defined in the class diagram using OCL constraints:
• The first property states that all prescriptions that are filled in a pharmacy were issued by a doctor previously. This implies that only genuine prescriptions are filled. To be able to express the property, two ghostvariables were added to the application model.If an attribute or association end in the class diagram is annotated with stereotype << Ghostvariable>>, this denotes that this attribute or association end is used to express a security property only. The association between the Terminal class ArztPC (the doctors PC which is used to issue the prescription) and the class ERezeptdaten (the data of a prescription) with association end ausgestellt (issued) stores all prescriptions that were issued by one doctor (using his PC). The association between the Terminal class ApothekenPC (the PC in the pharmacy which is used to fill prescriptions) and the class ERezeptdaten with association end eingeloest (filled) stores all prescriptions that were filled in one pharmacy (using the ApothekenPC). The OCL formula inv : ArztPC.allInstances().ausgestellt -> includesAll(ApothekenPC.allInstances().eingeloest) is defined for the class ApothekenPC and expresses that all prescriptions that are filled in a pharmacy were issued by a doctor previously. For each terminal (doctor's PC and pharmacy PC) all instances of that class, e.g. all PC's of all doctors and all pharmacy PC's, are considered.
• Each prescription contains a nonce. If two prescriptions with the same nonce exist, this means that an attacker was able fill a prescreption twice. This is an attack of the system and has to be forbidden by the application resp. the protocols. The second property is used to express that all prescriptions that are filled in all pharmacies have different nonces:
  inv : ApothekenPC.allInstances().eingeloest.nonce->isUnique(). Since we consider the prescriptions that were filled in all pharmacies, this includes that one prescription is not filled in different pharmacies. Note that the application model has no central component to store all prescriptions that were issued and filled.
• The third security property states that all personal data (e.g. name and insurance number) stored on a health card (Versichertenstammdaten) of each patient cannot be manipulated by an attacker. These data is updated by the health insurance company (Krankenkasse) only. The update is done while the patient is visiting a doctor, using the doctor's PC. The property, formulated as OCL formula, is
  inv : Krankenkasse.allInstances().db->includesAll(Gesundheitskarte.allInstances().daten). The personal data stored on all health cards (association with end daten between the class Gesundheitskarte and Versichertenstammdaten) is the same as the one stored by the health insurance company (modelled by association with end db between class Krankenkasse and class Versichertenstammdaten). This means that the attacker is not able to manipulate the personal data which was sent from the health insurance company to the healthcard.
  
• The formal model that is used for verification of the property is a distributed system with finite but arbitrary components (e.g. smartcards, terminals, services and user). The property has to hold for arbitrary protocol runs that can be interleaved with other protocol runs. Additionally, the attacker is able to interfere the communication as defined in the deployment diagram.      
  

Back, Next Step: Activity diagrams showing the interdependencies between the protocols