Static Equivalence is Harder than Knowledge
2006 (English)In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, Vol. 154, no 3, 45-57 p.Article in journal (Refereed) Published
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.
Place, publisher, year, edition, pages
2006. Vol. 154, no 3, 45-57 p.
Security protocol analysis, Term rewriting, Decidability
IdentifiersURN: urn:nbn:se:uu:diva-161487DOI: 10.1016/j.entcs.2006.05.006OAI: oai:DiVA.org:uu-161487DiVA: diva2:456287
EXPRESS'05 12th International Workshop on Expressiveness in Concurrency 27 August, 2005 San Francisco, USA
Conference paper presented at the EXPRESS'05 12th International Workshop on Expressiveness in Concurrency 27 August, 2005 San Francisco, USA2011-12-062011-11-142011-12-06Bibliographically approved