Information Technology Reference
In-Depth Information
extends the pi calculus [12] with cryptographic primitives [3]; The applied pi
calculus [1] extends the pi calculus with a general notion of terms; L Y S A [4]
is a variant of the spi calculus with pattern matching. An obvious strength of
process calculus approach is their inherent mechanism for handling concurrency
and communication.
Since there is no general formal framework for the analysis of security pro-
tocols, we intend to devise the GSPM to state various security properties, as
expressed explicitly in a formal specification, and model the protocols in a pre-
cise and faithful manner. GSPM stems from concepts well established in the field
of process calculi (such as CSP, pi calculus and ambient [5] etc.). We discard the
notion of channel and don't explicitly model the intruder, yet our simple model
is powerful.
The next section presents GSPM. Section 3 defines formally some security
properties such as confidentiality, authentication, non-repudiation, fairness, and
anonymity based on our model. Section 4 illustrates an example. Section 5 dis-
cusses our future work and concludes.
2GSPM
In this section we present the main aspects of our model. The motivation for the
model is to be more explicit about the activities of the participants in a protocol
and those of possible attackers, and to express various security properties in a
formal specification.
2.1
The Abstract System Model of Security Protocols
In this subsection we outline how the abstract system model of the security
protocols are constructed in GSPM. Our approach provides a GSPM description
of the Dolev-Yao assumption [7]: the communication medium is entirely under
the control of the enemy, who can block, re-address, duplicate, and fake messages.
In [16], the roles of the passive medium and of the active intruder are described
using different processes. In our framework we see the combination of the intruder
and the medium as a single entity (we call it active environment). Let Id i stand
for the i th participant of a security protocol. The resulting system model of the
protocol is shown in the Figure 1.
Id 1
Id 2
Id n
Active Environment
Fig. 1. The abstract system model of security protocols
Search WWH ::




Custom Search