Soundness Conditions for Message Encoding Abstractions in Formal Security Protocol Models