Jorma Paananen
Tik-110.501 Seminar on Network Security
Jorma.Paananen@tele.fi
1.1 Reasons to use formalisms
The main reason to use formal description techiques, or formal methods,
is that they give us tools to analyze protocol models and other systems of
interest, and find facts and errors in them, both at the specification level
and at the implementation level. Formal methods can be used in performance
evaluation, and even to find new inplementation techiques. Checking the
conformance between various levels of abstraction is also possible.
There currently exist many computer tools, both free and commercial,
to help us in using formalisms.
The most difficult part of using formalisms is perhaps in choosing the
formalisms to use and the abstraction level of the model. For example in
a state machine, based formalisms balancing between a too simple model and
a too complex model is hard. A simple model will possibly leave some
important details hidden, whereas a complex model can cause combinatorial
explosition in the state space.
2. Petri Nets
Petri Nets were first introduced by C.A. Petri in the 60's as a common
reference model of the net theory [1, 2,
3]. A basic Petri Net consists of a set of
places, a set of transitions and a set of arcs connecting places to
transitions and transitions to places. Semantically a Petri Net can be seen
as a condition/event graph, where places are conditions and transitions are
events. An event can occur if all conditions for the event hold. In a Petri
Net, this means that there is a mark in all the places that are connected to
the transition as input places. When an event happens, that is, a transition
fires, marks are removed from those places and marks are added to all those
places that are connected to the transition as output places.
This is a graphical representation (a directed net) of a simple communication system modelled as a Petri Net. It represents a simplified version of the alternating bit protocol with a lossy communication channel from the sender to the receiver. In the picture the places are drawn as circles and the transitions are drawn as lines. Arcs from places to transitions and from transitions to places have a direction.
In the figure the sender is ready to send (there is a mark, a token, in the place "ready to send") and the receiver is ready to receive. Transition "send" is enabled, ready to fire, because there is a token in the place "ready to send", the only place connected to the transition as the input place. After the transition fires the token disappears from the place "ready to send" and a token appears in the places "in buffer" and "sent". After that the transitions "receive" and "lose" are enabled.
In addition to the places, transitions and arcs we have an initial marking, place capacities and arc weights.
K(p) denotes the capacity of the place. It sets the upper limit to the number of tokens that a place can hold. Alternatively the capacity can be unlimited, i.e. infinite. More formally K can be defined as a function:
W denotes the weight of an arc. The weight tells the number of tokens that the firing of a transition either removes from or adds to the places that are connected to the transition. It can be defined as a function:
Petri Nets with finite capacity, that is, in nets where for all places p
have a restriction in the transition rule: a transition is enabled only
if the number of tokens in each of the output places would not exceed its
capacity after firing the transition. This is called the strict transition
rule. Petri Nets with infinite capacity of places don't have this
restriction and they obey the so called weak transition rule.
2.1 Predicate/Transition Nets (Pr/T Nets)
A Pr/T Net is a more powerful formalism developed from ordinary Petri Nets
by Genrich and Lautenbach. Informally, the Pr/T Nets add individuals,
their changing properties and relations to the ordinary Petri Nets. In
other words, tokens have an identity and arcs are labeled with variables,
and the transitions may be annotated with a formula. The formula limits
the conditions when the transition can fire.
The transition is drawn as a box so that the logical formula fits inside it.
The most common property of a Petri Net or Pr/T Net that is used in studying the dynamics of the modelled system is reachability. Marking Mj is reachable from marking Mi if there exists a series of transition firings that end in the marking Mj.
Another important concept that can be studied is liveness. There are different levels of livenesses defined, but basically liveness for the marking M0 means that in all reachable markings it is possible to fire any transition in the net after some firing sequence. In other words, the precense or absence of deadlocks can be studied.
The graphical representation of the formalism gives a clear visual means
for simulating the dynamics of the system, step by step or continuously.
3. Process algebras, LOTOS
A process algebra is a model based on modelling processes and events.
The algebra provides operations for combining events and processes.
The names of the events in the process algebra are called actions.
A process is specified by defining its behaviour as a sequence of possible
events. Examples of process algebraic formalisms are LOTOS, CCS and CSP.
LOTOS (Language Of Temporal Ordering Specification) was developed in the 80's and it became a ISO standard in 1989 [4, 5]. It describes a system by defining all the possible event orderings that an external observer may detect. A LOTOS description consists of two parts, the first part describes the process behaviours and their interactions, and the second part describes the data stuctures and value expressions. Data type description is based on a language called ACT ONE.
This is an example of a system that has four events: send_request, ok, error and deliver. Send_request and deliver events include data in the event. The system is a box with a number of action points (gates in LOTOS) that can be seen from its environment. The alphabet of the system is the set of possible actions of a system.
This is a more detailed model of our previous example. The inside of the box consists of processes and connections between them. Communication between processes is synchronous; an event is possible if and only if all processes that are intrested in it are ready to perform it, and they all perform it simultaneously. Asychronous communication can be modelled placing queues between processes. The queue is specified as a process. A process has a similar structure as the whole system itself.
LTS is not directly a LOTOS concept. Data in a LTS can be included as typed variables and the values of the variables can be tested.
Some basic LOTOS syntax describing the testing, input, output and synchonization and some examples:
The primitive propositions themself are also propositional formulas. Examples of primitive propositions are the following:
A: "It is raining" B: "The window is open"Now a sentence "It is raining and the window is not open" can be formulated as a proposotional formula as:
A propositional modal formula is a propositional formula added with a modal operator, expressed here with the letter K [6, 7]. A modal operator often expresses a temporal or epistemic "mode" of its operand. Some examples of modal operators are "knows", "next", "believes" and "until". In a multimodal logic there can be more than one modal operator. For example, we can fomulate "Bob knows that it is raining" as
and "Alice knows that Bob knows that it is raining and the window is open" as
Arcs connecting the worlds show which player thinks that both worlds connected with the arc are possible. There should be also a self loop at each world denoting that the player considers the actual world possible, but they are left out to make the picture more clear. The situation where the player 1 has card C is outlined in the following picture:
In addition to the basic knowledge operator K, when modelling knowledge, there are two important modal operators. Those are E, everyone knows and C, common knowledge. If "a" is a formula, then veryone knows "a" simply means that everyone knows "a". Common knowledge means that everyone knows "a" and everyone knows that everyone knows "a" and so on. If G is the group of agents, we can formalize:
4.1 Other modal logics
Modal logics are in no way restricted to a particular logic. If we take,
for example, first order logic we can create a first order modal logic
by adding one or more modal operators. For example, let's consider a first
order formula "Every house has a door". It can be formalized as:
Now we can formalize the sentence "Bob knows that every house has a door" is:
The same possible worlds semantic works well also for this kind of logic.
5. Temporal logic
Temporal logic is a form of modal logic where the modal operators deal
with the concept of time [6, 8].
Common temporal operators are the following:
6. Conclusions
Formal description techiques, or formal methods, give us tools to analyze
protocol models and other systems of interest.
Petri Nets and process algebras concentrate more on modelling the state of
the protocol; modal and temporal logic are used more on modelling the
knowledge of communication parties.
References