Information Technology Reference
In-Depth Information
enjoys it. To obtain such result we will assume some restrictions on the class of
inference systems. Here we use the terminology of [4] about inference systems.
Given a well-founded measure on messages, we say that a rule
r
.
=
m
1
...
m
n
m
0
is a S-rule (
shrinking
rule), whenever the conclusion has a smaller size than
one of the premises (call such premises
principal
); moreover all the variables
occurring in the conclusion must be in all the principal premises. The rule
r
is
a G-rule (
growing
rule) whenever the conclusion is strictly larger than each of
the premises, and each variable occurring in the premises must also be in the
conclusion.
Definition 1.
We say that an inference system enjoys a G/S property if it con-
sists only of G-rules and S-rules, moreover whenever a message can be deduced
through a S-rule, where one of the principal premises is derived by means of a
G-rule, then the same message may be deduced from the premises of the G-rule,
by using only G-rules.
Several of the inference systems used in the literature for describing crypto-
graphic systems enjoy this restriction.
It is worthy noticing that using G-rules for inferring the principal premises of
an S-rules, is unuseful. Thus, shrinking rules may be significantly applied only to
messages in
φ
and to messages obtained by S-rules. However, since the measure
for classifying the S-rules is well founded then such application phase would
eventually terminate.
Consistency Check.
We will be interested in establishing whether or not a list
of constraints is satisfiable. There are several formats for the lists of constraints
whose satisfiability problems can be easily solved.
We say that a list
M
of constraints is in
normal form
(
nf
for short) whenever
the followings hold:
-
the left hand side of each constraint is a variable,
-
each variable occurs in the left hand side at most once,
-
each deduction which occurs in the right hand side only consists of
G−rules
.
We say that a list
M
of constraints is in
simple
normal form (
snf
for short) if
it is in normal form and moreover all the constraints but
false
are of the form
x ∈ t
.
We first study the consistency problem for lists in simple normal form. We
can define a dependency relation between the variables that occur in lists of
constraints in simple normal form: we say
x
M
y
) whenever there
exists in
M
a constraints like
x ∈ F
(
t
1
,...t
n
)(
x ∈ y
) and
y
occurs in
t
i
, for
i
≤
1
M
y
(
x
≤
0
∈{
1
,...n}
. Consider the relation
≤
M
which is obtained by considering the
1
0
M
transitive closure of the relation
≤
M
∪≤
where at least one step of closure is
