Information Technology Reference
In-Depth Information
cution that contains this pattern it will also violate the security property. Thus
our
is
finitely refutable
with a known complexity — the refutation information
is concentrated in a locus of a constant complexity. What is to be proved for
the decidability is the following property of
Ψ
Φ
that we call
finite satisfiability
:if
we take a model of
(in our case an execution of the protocol under consider-
ation) and choose any sub-model of a fixed complexity then we are be able to
extend this sub-model to a total finite model with a controllable augmentation
of the complexity. If to prove finite satisfiability of practical protocols (and intu-
itively it looks plausible), the decidability of the security will be implied by the
decidability of some logic where one can describe models of a fixed complexity.
If go out of limitations of model-checking, the verification problem is a prob-
lem of determining appropriate classes of logic formulas in appropriate logics;
for cryptographic protocols, taking into account time stamps and timing attacks,
we are in particular domain of verification of real-time (reactive) systems.
Φ
5 Types and Security
Many access security properties can be expressed and checked on the basis of
the idea of types. The declared Java type security, though it failed in its initial
context, stimulated research in this direction.
As an example consider the problem of buffer overflow for C language. Given
a C program we wish to be sure that no buffer overflow will happen during its
execution. We can try to check it statically. Paper [27] describes an algorithm for
static analysis of C code. The analysis is reduced to a constraint solving problem,
and though no theoretical analysis of computational complexity is given, the
fact that experimental complexity is linear, shows an interesting question for
the theory. The algorithm outputs many false alarms, and this implies another
question what quality of analysis is achievable within a given complexity. The sets
of questions arising within this approach seem to have the flavor of approximate
solutions to some optimization problems.
Another way to solve such problems is to supply an executable with a proof
that the security property is valid. This idea of proof carrying code is being
studied since [19]. The problem is to develop an adequate language for express-
ing security properties and an inference system which gives rather short proofs
that can be eciently found. Clear, that such properties can be satisfied si-
multaneously only for particular problem domains. In addition to traditional
complexity problems one can see here a problem a minimizing the entropy of
domain-oriented knowledge representation in the sense of [25].
In the same setting one finds other ideas concerning the enforcement security
policies [13,22,5]
5
. The main open complexity problem concerns the verification
of whether global security property is achieved via local checks of applied security
policies.
5
Here
security policies
is a special term related to programming; in a wider context of
security this term usually means activities related to the administration of security.
