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.
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.