On the soundness of authenticate-then-encrypt: formalizing the malleability of symmetric encryption