Information Technology Reference
In-Depth Information
Thus, (1) is reduced to a satisfiability (validity) checking problem. For certain
classes of formulas, especially the ones that express reachability properties, such
a satisfiability problem can be eciently solved.
We defined in [9,10] a variant of CCS process algebra suitable to model cryp-
tographic protocols, i.e. CryptoCCS. In [8], a symbolic semantics for Crypto-CCS
has been given. In a symbolic semantics, usually the set of possible messages
that a process may receive in input is implicitly denoted by some kind of sym-
bolic representation (e.g., see [3]). On this representation several operations are
possible that mimic the concrete semantics (usually based on explicit replacing
of variables with messages). Clearly, there must be an agreement between the
concrete semantics and the symbolic one. A symbolic semantics is usually more
technically challenging than the corresponding concrete one. However, analyzing
with the symbolic representation is usually more ecient than with the explicit
one; moreover, as in the case of cryptographic protocols, the symbolic semantics
often allows to finitely describe infinite sets of messages that otherwise could not
be explicitly treated.
In this paper we develop a version of the Hennessy-Milner logic [2] suitable for
describing security properties. We then extend the analysis approach based on
partial model checking (e.g., see [10,11]) to such a symbolic logic. We stress that
we do not have a built-in notion of the intruder. In our framework, an intruder
could be any term of the algebra. This makes our approach, in principle, not
uniquely tailored for security analysis. Moreover, to the best of our knowledge
this is the first attempt to provide a symbolic technique to partial model checking
problems.
The rest of the paper is organized as follows. Section 2 recalls the symbolic se-
mantics for Crypto-CCS based on list of constraints and the necessary technical
tools to analyze such constraints. Section 3 introduces the symbolic Hennessy-
Milner logic. Section 4 presents the analysis for checking security properties
through symbolic partial model checking. Finally, Section 5 gives some conclud-
ing remarks.
2 Symbolic Semantics for Crypto-CCS
This section recalls the symbolic semantics for CryptoCCS defined in [8].
Our model consists of a set of sequential agents able to communicate among
each other by exchanging messages. We decided to parameterize the value pass-
ing CCS calculus through a set of inference rules for coping with the variety
of different cryptosystems. For the application of these rules, we added a new
construct to the language.
2.1 Messages and Inference Systems
Here, we define the data handling part of language. Messages are the data ma-
nipulated by agents. We introduce also the notion of inference system which
models the possible operations on messages. Formally, as messages we consider
the terms of a given algebra (with the usual definitions).
Search WWH ::




Custom Search