Introducing authenticated encryption?

[S3j5b0]

Hi, I am sorry if this is not appropriate here, as it is probably more a question than a feature request. I just did'nt know where else to ask it.

So the language have really easy-to-use terms for things like encrpytion. But I've really been struggling with how to represent other primitives.

If you for example wanted other primitives like authenticated encryption, would the best approach be to create your own equational theory for something like AEAD, like described for diffie hellman in section 10.2 of the user manual? Does there perhaps exist a list somewhere of examples of how to represent different primitives?

[cascremers]

(oops, missed before) In Scyther's relatively coarse model, (symmetric) encryption effectively models authenticated encryption. This is a known issue with classical Dolev-Yao modeling of primitives. If you want more fine-grained models (and hence more accurate guarantees), I recommend checking out the Tamarin prover.