Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries