Odd Error Message w/SAPIC+, state storage, and symmetric-encryption built-in

[Daniel Zimmerman]

Hi!

I've written a version of the symmetric Needham-Schroeder key exchange protocol in SAPIC+, based on the typed pi-calculus example of the same provided with ProVerif. I use SAPIC+'s state storage/retrieval functions to store the keys shared between the server and the other communicating parties. I also use the Tamarin `symmetric-encryption` built-in to get `senc` and `sdec` functions and the relationship between them.

The theory parses fine with Tamarin (I haven't been able to prove anything about it yet, but that's another issue that I don't want to get into here), but when I try to convert it to ProVerif, I get the following error:

tamarin-prover: user error (The string senc is used for distinct constructs (function name, constant or events). You should rename the constructs.)

However, if I instead remove the `symmetric-encryption` built-in and explicitly declare functions senc/2, sdec/2[destructor], and equation sdec(senc(m, k), k) = m, it converts to ProVerif without that error message. The resulting ProVerif file doesn't parse, because of the way the state handling is translated, but that's another issue that I also don't want to get into here; I'm just wondering why using `symmetric-encryption` instead of declaring those functions "by hand" causes the translation to fail.

I've attached my source code, in case it's useful. Thanks in advance for any help!

-Dan Zimmerman