|
In the spi calculus, the property of secrecy with regard to the process
Inst(M), where
A(M) := !c<M>.0 B := ?c(x).F(x) Inst(M) := (new c)(A(M) | B) is defined as follows: Inst(M) ~ Inst(M') if F(M) ~ F(M'), for any M,M' (~ denotes here testing equivalence) More formally, this can be expressed as \forall M,M'. (F(M) ~ F(M') ==> Inst(M) ~ Inst(M')) However, if we put F(x) = !a<x>, an agent that announces x along a public channel "a", then Inst clearly satisfies the secrecy property, since F(M) ~ F(M') iff [M is M'] is true, in which case also Inst(M) ~ Inst(M'). Worse yet, we can also eliminate restriction on channel c and still get a process that satisfies the secrecy property, for exactly the same reason. The secrecy property seems to be a necessary condition for secrecy,
but far from sufficient, and therefore not suitable as a
definition. Informally, secrecy is defined as the fact that "the message M
cannot be read in transit from A to B". Hence, F(x) does not seem to be not
relevant for the definition of secrecy. Why not then put F(x) = 0, and
define secrecy simply as Inst(M) ~Inst(M') for any M,M'?
Moreover, if F(M) ~ F(M'), in the pi-calculus at least these two agents
should be regarded as indistinguishable in an absolute sense (cf.
the Leibniz principle), not for an intruder only, but for any agent, honest
or not. Thus, F(M) ~ F(M') for any M,M' would mean that
for the agent F it doesn't matter what the secret M is, which
goes against intuition. To my mind the secrecy of M in F(M)
means that M cannot be guessed from the external behaviour of F(M), not
that the behaviour of F(M) is independent of M. As it
were, that F(x) is a "one-way function" of x.
Authenticity, on the other hand, is defined as
follows: Inst(M) ~ Inst_spec(M) for any M,
where
Inst_spec(M) = (new c)(!c<M> | ?c(x).F(M)) This definition is also surprising, as we may deduce that secrecy, as defined above, implies authenticity. Thus, if F is such that F(M) ~ F(M') for any M,M' (i.e. F(M) never reveals M, according to the interpretation given), we may deduce that Inst(M) ~ Inst_spec(M) for any M (we can also eliminate restriction in this case). This seems also to go against intuition (at least mine). José L. Vivas |