Safe abstractions of data encodings in formal security protocol models