Static Equivalence is Harder than Knowledge

There are two main ways of defining secrecy of cryptographic protocols. The first version checks if the adversary can learn the value of a secret parameter. In the second version, one checks if the adversary can notice any difference between protocol runs with different values of the secret parameter. We give a new proof that when considering more complex equational theories than partially invertible functions, these two kinds of secrecy are not equally difficult to verify. More precisely, we identify a message language equipped with a convergent rewrite system such that after a completed protocol run, the first problem mentioned above (adversary knowledge) is decidable but the second problem (static equivalence) is not. The proof is by reduction of the ambiguity problem for context-free grammars. Conference paper presented at the EXPRESS'05 12th International Workshop on Expressiveness in Concurrency 27 August, 2005 San Francisco, US