16-08-2012, 03:00 PM
A Tool of Analysis and Implementation of Security Protocols on Distributed Systems
A Tool of Analysis.pdf (Size: 366.3 KB / Downloads: 21)
ABSTRACT
In this paper we present an analysis and automatic
implementation tool of security protocols based on Techniques
of Formal Description. A sufficiently complete and concise
formal specification that has allowed us to define the state
machine that corresponds to a cryptographic protocol has been
designed to achieve our goals. This formal specification also
makes it possible to incorporate in a flexible way the
mechanisms and functions of security. Our system makes it
possible to automatically translate formal specifications of
protocols to a group of derivation Prolog rules. Our work
improves the solution first proposed by J.K. Millen in [1]. We
study the vulnerability of security protocols exploring, in an
automatic way, all its possible behaviors in agreement both with
their formal specification and with the information potentially
recorded by an intruder.
INTRODUCTION
The Formal Description Techniques are the base of the
automated support in different development activities. The
formal specification is an essential tool in the engineering of
communications protocols. Using the Techniques of Formal
Description significant improvements can be obtained in the
quality of the product, availability in the market and cost of the
lifecycle.
The formal models of security have evolved in parallel with the
development of the computer systems (software, hardware,
operating systems), as well as with the technology and
extension of the data networks. Initially, the formal models have
treated the problem of control access in individual systems. The
criteria of security TCSEC (Trusted Computer System
Evaluation Criteria) of the DoD (Departament of Defense) of
the government of USA [4] or the European ITSEC
(Information Technology Security Evaluation Criteria) [5]
criteria are an example of the formalization in the field of secure
computer systems.
STRUCTURE AND SCOPE OF THE ANALYZER OF
ATTACKS
The Analyzer of Attacks (A.N.A.) is the name of the model of
analysis, verification and implementation of security protocols
proposed in this work. On the one hand, this model is able to
generate in an automatic way a group of derivation rules in
Prolog that represent a security protocol starting from its formal
specification. The rules make it possible to carry out an
exhaustive analysis of the vulnerability of the protocol. On the
other hand, the Analyzer of attacks is able to generate in an
automatic way a real implementation of the protocol. We have
designed a system that makes it possible to incorporate in a
dynamic and flexible way security services in the TCP/IP
protocol suite.
LOGICAL ELEMENT OF ANALYSIS
The Logical Element of Analysis translates in an automatic way
a formal specification of a security protocol according to some
predefined syntactic rules (Formal Specification I) to a group of
Prolog derivation rules (Formal Specification II) that represent
the protocol and that makes it possible an exhaustive analysis of
its vulnerability. The Logical Element of Analysis of our model
consists of several modules that in turn contain a series of
associate procedures whose description is detailed in [18].
Example of Analysis using the Analyzer of Attacks
In what follows an example of analysis of security protocol in
function of the exhaustive search of alternatives provided by the
Prolog specification is described. In this example, we begin
with a specification of a security protocol made up of four
exchanges (see figure 3).
It has to be taken into account, that in the specification of the
protocol the initial knowledge on the part of an intruder of the
fields "kx" (old key) and “encrypt(ksa,x)" (encryption pattern)
has been defined. In the following queries the Prolog interpreter
behavior regarding the generation of possible fields and
histories of alternative messages is shown.
CONCLUSIONS
In this paper a tool for the analysis and automatic
implementation of security protocols has been presented. The
result of this work is twofolf:
• On the one hand it has been proven that the automatic
translation of a security protocol to a group of Prolog rules is
a valid choice for the exhaustive study of attacks. Either the
supplantation of fields of a message, or the complete
supplantation of a message, makes it possible to analyze and
to study the attacks to a security protocol and its possible
vulnerability. Having some information about the contents of
the exchanges that an intruder could know and thanks to the
Prolog backtracking property one can explore, if there is any
possibility, of an intruder accessing sensitive information.