As you observe, sometimes specifications with an arbitrary F are equivalent to special cases, and we did exploit that in our proofs. (It might have been much harder to do the proofs otherwise, because the statements of theorems are both co- and contra-variant in may-testing equivalence, so working with conservative approximations to may-testing equivalence would not have sufficed.)
As you also observe, we did not have a very general model of the system surrounding a protocol, and had no formal boundary between the protocol and the rest of the system. We have since made much progress in this respect, in my opinion. Please see for example "Secure implementation of channel abstractions", which I wrote with C. Fournet and G. Gonthier sometime after the initial work on the spi calculus.
Regards,
Martin
José L. Vivas wrote:
We are interested in describing and analyzing protocols that are part of systems, and any guarantees about protocols may be subject to hypotheses on the rest of the systems. This manifests itself in several ways---for example, as hypotheses on the messages that the application-level message that the protocol transmits, or as hypotheses on what the recipients of those messages do with them. Formally, those are the M's and the F's of the message below. If we were to assume that F(x) = F'(x) = 0 and define secrecy only for that case, as suggested in the message, then we would be providing a guarantee for the protocol only in the case it which its payload is discarded by the recipient. It is easy to make up protocols that work in that special case but not otherwise.
I think we are in this way providing guarantees for all F such that F(M) ~ F(M') for any M,M'. The proof of secrecy given in page 37 of the extended version can be used to show this. By letting F(x) = 0 we obtain
Inst(M) ~ Inst_spec(M) ~ (new c)(Inst(M,!c<*>) | c(y).0) ~ (new c)(Inst(M,!c<*>) | c(y).0) ~
Inst(M')
Since ~ is a congruence, we may substitute equals for equals on both sides of an equality, obtaining
(new c)(Inst(M,!c<*>) | c(y).F(M)) ~ (new c)(Inst(M,!c<*>) | c(y).F(M'))
i.e. Inst(M) ~ Inst(M') for the general case. Also, the case F(M) ~ F(M') means discarding the secret as much as in the case F(x) ~ 0, at least in the pi-calculus, as I argued in my previous email. If you cannot observe any difference, they are indiscernible in an absolute sense, both for malicious and for honest agents.
The secrecy guarantees are of interest for every F, or every reasonable F. Therefore, observing that they may be vacuous for some particular F's (e.g., !a<x> below) does not seem problematic.
According to the definition of secrecy the resulting agent can be proved to satisfy the secrecy property, although it gives away the secret, so it is not a vacuous case. Nowhere it is stated that the secrecy property is only valid for reasonable F. The definition, once again, is the following:
Inst(M) ~ Inst(M') if F(M) ~ F(M'), for any M,M'
No restrictions are put here on F. The property says simply that Inst(M) ~ Inst(M') whenever F(M) ~ F(M'). The restrictions on F, stated elsewhere, are the following: the bound parameters of the protocol (M,c, and x) cannot occur free in F. Nowhere it is assumed that F must be "reasonable" (by which I presume it is meant that F(M) ~ F(M') for any M,M'). Now, assume we make this assumption. Then the premise of the secrecy property is superfluous. It would be better simply to define secrecy as follows:
Secrecy2: Inst(M) ~ Inst(M') for any M,M'.
This, by the way, should imply that F(M) ~ F(M') for any M,M', i.e. F is reasonable.
Now if we define
Secrecy3: Inst(M) ~ Inst(M') for any M,M', where F(x) = 0,
we may prove, if my argument above is correct, that Secrecy2 is equivalent to Secrecy3. In any case, there seems to be no need to make any assumptions about F in the definition. This seems to be in harmony with the informal definition of secrecy: "The message M cannot be read in transit from A to B". Of course, the behaviour of F cannot change the truth value of this assertion.
Another point is that it seems arbitrary to take into consideration the continuation of agent B after input, but not that of agent A after output. We may assume that A will continue communicating with B, and this behaviour is not less or more important for the correctness of the protocol than the behaviour of B.
Finally, it would be helpful to have a good definition of what a protocol is. This concept is not used consistently in the spi calculus papers. Sometimes it refers to Inst(M), together with F, sometimes it excludes F.
Regards,
José L. Vivas
On authenticity, I agree that the definition may be surprising, and we probably would not have claimed that it is a general definition, only that it leads to a useful analysis in the protocols under consideration. You may wish to look at the work of Focardi, Gorrieri, and Martinelli on definitions of authentication ("A comparison of three authentication properties").
Regards, Martin
José L. Vivas wrote:
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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html