Authenticated Encryption

[andres-erbsen]

The existing example uses secret-key authentication and secret-key encryption in the usual verify-then-decrypt manner. Perhaps there would be proof niceness to be gained by defining proof rules for this common combination. In particular, I think an interesting model to try would be to say that the decryption output is not tainted with the secret key but is tainted with all encrypted messages in its subtree.

I guess this also matters for completeness: not all authenticated encryption schemes are black-box constructions from write-only encryption and authenticators.

[andres-erbsen]

for decryption, the "did decryption succeed" output is encrypt_safe. We think this is enough to support authenticated encryption to the same extent as we support mac+cpa.