ASN1-light: A Verified Message Encoding for Security Protocols

There is a mismatch between the data format used in implementations of security protocols and the data types used in formal verification of security protocols. We present a verified encoding scheme for data used in security protocols, which links the abstract data types of the formal world to a byte format usable in implementations. The encoding is inspired by the ASN1 encoding scheme. The encoding is implemented in Java and the implementation is proven to be correct against a formal specification. The implementation can be used as a reusable reference library in security protocol implementations. The benefit is a separation of concerns: The protocol can be verified on an abstract level. The mapping to bytes is automatically correct by linking the library. Additionally the encoding is a challenging Java verification case study in its own.