Soundness Conditions for Message Encoding Abstractions in Formal Security Protocol Models

In formal methods, security protocols are usually modeled with a high level of abstraction. In particular, marshalling/unmarshalling operations on transmitted messages are generally abstracted away. However, in real applications, errors in this protocol component could be exploited to break protocol security. In order to solve this issue, this paper formally shows that, under some constraints checkable on sequential code, if an abstract protocol model is secure, then a refined model, which takes into account a wide class of possible implementations of the marshalling/unmarshalling operations, is implied to be secure too. The paper also indicates possible exploitations of this result.