Information Technology Reference
In-Depth Information
and for optimisation. Type systems thereby raise the level of abstraction of an
operationally dened programming language; their role in the bottom-up devel-
opment of a theory is complementary to that of healthiness conditions, which
in a top-down development bring abstract denotational specications closer to
implementable reality.
Operational presentations of semantics are particularly appropriate for anal-
ysis of security aspects of communication in an open distributed network, where
co-operation between a known group of agents is subject at any time to acciden-
tal or deliberate interference by an outsider. The main role of the language is
to dene and limit the capabilities of the outsider. For example, the localisation
operator (
new
) enables an agent in the system to invent an arbitrary secret
code or a
nonce
, and the structural laws of the language are designed to ensure
that it remains secret except to those who have received it in an explicit com-
munication. It is then the responsibility of an implementation of the language to
enforce this level of secrecy by choice of an appropriate cryptographic method.
Furthermore, if the proof of security of a protocol depends on observance of type
constraints, it is essential at run time to check the types of any code written by
an outsider before executing it in a sensitive environment.
The purpose of a secure protocol can often be described most clearly by an
equation
e
P
=
Q
,where
P
describes the situation before some desired interaction
takes place, and
Q
describes the desired result afterwards. For example, we might
use the equation
(
e:P j e:Q
)=
PjQ
to describe the intended eect of transmission of a signal
. But this
is not a valid equation in the calculus, because it is not secure against interference
by an outsider
e
from
Q
to
P
R
, which can intercept and divert the signal, as permitted by the
reduction
e:P j e:Q j e:R ! e:P j Q j R
This reduction will be inhibited if the name
e
is kept secret from the outside, so
it is valid to equate
(
new
e
)(
e:P j e:Q
)=
new
e
)(
P j Q
)
Since it is assumed that the outsider is limited to the capabilities of the pro-
gramming language, an arbitrary attack can be modelled by a context C[ ] placed
around both sides of the equation. A standard proof of contextual equivalence
would be sucient to show that there is no such context. That is exactly what
is needed to show that no outsider can detect or aect the desired outcome
described by the equation. As in this example, the required protection is often
achieved with the aid of the
new
operator, which prevents an outsider from de-
tecting or communicating a signal with the new name. It is much more dicult
to design a top-down theory for application to problems of security, privacy and
authentication. A top-down theory has to start with a decision of exactly what
an intruder could observe of another agent in the system, and what attacks are
Search WWH ::
Custom Search