TLS Server Hello: Extensions_Length constraint failure

[rssen]

When parsing a Server Hello message, the following error occurs:

E       AssertionError: unresolved field conditions in Server_Hello.Extensions_Length: Random /= [16#CF#, 16#21#, 16#AD#, 16#74#, 16#E5#, 16#9A#, 16#61#, 16#11#, 16#BE#, 16#1D#, 16#8C#, 16#2#, 16#1E#, 16#65#, 16#B8#, 16#91#, 16#C2#, 16#A2#, 16#11#, 16#16#, 16#7A#, 16#BB#, 16#8C#, 16#5E#, 16#7#, 16#9E#, 16#9#, 16#E2#, 16#C8#, 16#A8#, 16#33#, 16#9C#], Random = [16#CF#, 16#21#, 16#AD#, 16#74#, 16#E5#, 16#9A#, 16#61#, 16#11#, 16#BE#, 16#1D#, 16#8C#, 16#2#, 16#1E#, 16#65#, 16#B8#, 16#91#, 16#C2#, 16#A2#, 16#11#, 16#16#, 16#7A#, 16#BB#, 16#8C#, 16#5E#, 16#7#, 16#9E#, 16#9#, 16#E2#, 16#C8#, 16#A8#, 16#33#, 16#9C#]

[treiher]

The error is probably caused by a TLS 1.2 Server Hello, which is not supported by our TLS 1.3 specification. But an unsupported message should not result in an assertion error. Is that a bug in pyrflx?

[rssen]

I think PyRFLX (the __simplified function) cannot handle that values Random is compared with are specified as a sequence.
I'll make a reproducer to verify if that is the case.

[treiher]

I see. Thanks for creating a reproducer (AdaCore/RecordFlux#964). As it seems to be a bug in PyRFLX, I think we can close this ticket here.