search

mit-plv / cross-crypto

Connecting computational and symbolic crypto models
MIT License
8 stars 19 forks source link

Authenticated Encryption #4

Open andres-erbsen opened 6 years ago

andres-erbsen commented 6 years ago

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 commented 6 years ago

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.