Re: [saag] ASN.1 vs. DER Encoding

[Benjamin Kaduk <[e-mail]>]

On Sat, Mar 30, 2019 at 05:25:35PM -0500, Nico Williams wrote:
> On Sat, Mar 30, 2019 at 10:31:02AM -0500, Benjamin Kaduk wrote:
> > On Wed, Mar 27, 2019 at 10:15:46AM -0500, Nico Williams wrote:
> > > On Wed, Mar 27, 2019 at 09:45:16AM +0000, Peter Gutmann wrote:
> > > > >Thus there is almost zero benefit to self-describing encodings.
> > > > 
> > > > ... apart from the fact that they can be statically analysed to check whether
> > > > they're well-formed or not, unlike the encodings in PGP, TLS, IPsec, SSH, ...
> > > 
> > > The protocols you list don't use a formal syntax, which instantly makes
> > > validity checking harder (can't generate the code!).  But if they had
> > > used XDR, or ASN.1 with PER/OER/..., you could in fact automatically
> > > check the validity of the encoding of a message.
> > 
> > N.b. that the protocol descriptions in RFC 8446 were run through an
> > automated syntax checker (IIRC, by Kazuho, though I'm not confident of that
> > and only bought 20MB of data for this  plane flight).  So I'm not entirely
> > convinced that this claim applies to TLS 1.3.
> 
> ISTR hearing about that, but the RFC does say:
> 
>   3.  Presentation Language
> 
>      This document deals with the formatting of data in an external
>      representation.  The following very basic and somewhat casually
>      defined presentation syntax will be used.
> 
> which is basically saying it's not a formal syntax.

We never bothered to remove the disclaimer, but the meaning is well-defined
and that's really all you need to make it a "formal syntax".  That text
seems unchanged from RFC 5246 (which really was a bit more slapdash about
the formal definition).

> Now, perhaps it can be be formalized.  If so, was that done for the
> checking you mentioned, and was it lost?  That would be unfortunate.
> 
> Are there implementations that generate codecs for TLS?

It looks like (per https://github.com/tlswg/tls13-spec/pull/999) I was
thinking of Kazu Yamamoto's
https://github.com/kazu-yamamoto/tls13-spec-validator which I guess will
generate haskell for the presentation language.
https://github.com/tlswg/tlswg-wiki/blob/master/IMPLEMENTATIONS.md does
list a Haskell implementation with Kazu as author (if we chase the link).
But I don't know if the implementation uses the generated code directly or
not.

Kazu, can you enlighten us?

Thanks,

Ben