Re: invertible protocol descriptions in Coq

[Jon Crowcroft <jon.crowcroft@xxxxxxxxxxxx>]

hm - so i think this is a weird paper - the example from eric rescorla's TLS work is easily sorted with an LALR1 parser and tokenisning the input stream not at the PACKET level, or byte, but by turning the protocol into a collection of microprotocols- indeed, this is how most people think about TCP - tcp is a collection of seperate protocols (state management for connection setup/teardown; sequenced data delivery; flow control; congestion control' urgent pointer; etc) living inside one packet format - don't get hung up on the packet format - that is a mere _lexical_ problem...

On Sat, Mar 16, 2013 at 9:21 PM, Anil Madhavapeddy <anil@xxxxxxxxxx> wrote:

Found this very cool paper on specifying invertible protocol descriptions in Coq:

http://staff.aist.go.jp/reynald.affeldt/documents/plpv2012-preprint.pdf

..and they cover TLS.  It would be a nice project to extract this to OCaml/Haskell
to guarantee parsing equivalence from the formal spec (this is basically a much
better implementation of MPL or FP, embedded in the Coq proof assistant).

-anil