Information Technology Reference
In-Depth Information
The results on multi-party protocols can be very roughly divided into results
related to private channels, many of them can be proved without intractability
conjectures, and results for insecure channels that use some intractability con-
jectures like the existence of trap-door functions with particular properties. The
complexity is measured in the number of rounds and the number of transmitted
bits. The results can be traced starting from [15].
The most relevant topic in our context is the verification of security prop-
erties of cryptographic protocols under the condition that the cryptographic
part enjoy certain security properties. The most common assumption is that
the cryptography involved is absolutely secured (perfect encryption) [3]. Even
within this conjecture the problem, taken theoretically, has not yet been satis-
factorily solved even for abstract specifications of protocols, not to speak about
implementations. The main question for this set of problems is the complexity
of verification of different security properties.
For concreteness, let us take one security property: to guard secret the session
key during a current session in protocols of session key distribution. There are
several results stating the undecidability of this property, the strongest ones are,
apparently, [12] and [1]. The result of [12] is based on a general notion of protocol
that is far from the reality — though the authors speak of bounded messages
(the height is bounded), their bit complexity is unbounded, and this permits to
model any Turing machine execution as a session of the protocol. One can see
also that we have here sessions of unbounded length and, in fact, there is only
one session — that one which is the execution of the modeled Turing machine.
The result of [1] also bounds the height of messages and even does not permit
the pairing function.
If for decidability results, they are too numerous to try to give a complete
survey that would hardly be of interest to people thinking about realistic ap-
plications; a brief overview of main existing approaches can be found in [10].
However, we mention some such results. Under a realistic assumption that the
number of parallel sessions is bounded [21] shows that the problem of insecurity
is NP-complete. If not to bound the number of sessions but to bound the gener-
ation of fresh names then we can still preserve the decidability but with higher
complexity, between simple and double exponential time in [1]. In [9] another
(incomparable) class of protocols, decidable in exponential time, is described
that contains ping-pong protocols [11]; more classes of decidable protocols with
hyper-exponential complexity can be found in [8].
We conjecture that security properties of
practical
protocols are decidable.
One idea why it is likely to be so is that from [6]. This consideration is formulated
without any particular constraints diminishing practical relevance of decidable
classes. Any verification problem can be represented as proving a formula of the
form (
Φ → Ψ
), where
Φ
represents the set of runs on the algorithm to verify
and
means the secrecy. If
the secrecy is violated then there is a session whose complexity is bounded by
a constant for a given protocol (we do not consider recursive protocols [20] that
are not so practical) whose session key is known to intruder. If we take any exe-
Ψ
represents the property to verify. In our example,
Φ
