[Impressum]
[E-Mail]
Modeling Copy Card with HashValues (2)
The
next step is to describe the data types and messages with UML class
diagrams and the communication structure and attacker capabilities with
an UML deployment diagram.
- Classes with the stereotype <<Terminal>>, <<Smartcard>> 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 between 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 usermessages as well as the user are defined in a separate class diagram (see below).
- The security properties that have to hold for the modeled
application are defined using OCL constraints. In this example, the
security property is defined for the
abstract class Terminal which is the superclass of the component
classes representing the Depositmachine and the CopyingMachine. The
class Terminal has an attribute money that is needed to formulate the
security property only. The stereotype<< Ghostvariable>>
denotes that this attribute is used to express a security property
only. During a protocol run of the Load protocol (to load money
onto the card) the money attribute is increased by the amount that is
loaded onto a card. During a protocol run of the Pay protocol the money
attribute is decreasesd byamount that is paid for the copies (see the
activity diagrams). This means that every decreasing and increasing of
the balance of any card is logged (in attribute money).
- The
security property that was verified for this application ist
that the sum of all money attributes of all instances of the class
Terminal (e.g. all DepositMachines and all CopyingMachines) is always
greater or equal than zero. This implies that "no money is lost", e.g.
the sum of money that was inserted into all DepositMachines is always
greater or equal to the sum of money that was paid out (in the form of
copies). The security property has to hold at any time. 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.
- The
attacker capabilities are described in the deployment diagram by the
stereotype <<Threat>>.
In this example the attacker is able to read all messages that are
exchanged between the terminals (CopyingMachine and DepositMachine) and
the Copycard. Besides the attacker is able to send arbitrary messages
on this communication channel as well as to suppress messages. The user
called CardOwner models a human that interacts with a terminal. The
interaction with the CardOwner (using the interface os the
CopyingMachine and the DepositMachine) is not interefered.
Back, Next Step: Detailed model with activity diagrams