CVE-2021-3449 is not caused by a flaw of the protocol itself, but because of an implementation issue. To demonstrate that tlspffin is able to find this vulnerability we encode the attack as a symbolic trace.
Input Step #0
Output Step #1
We tell Agent 1 to output messages and annotate them with the observed ID $(0,x)$, where $x$ is the index of the message sent during this step.
Input Step #2
Input Step #3
Input Step #4
Input Step #5
The Big Picture
The above terms are quite hard to read as they contain cloned sub-terms. By clustering the terms and reusing sub-terms we can make it visually clear that sub-terms are indeed reused.
Note that the above trace does not use a client agent. Is uses a single agent which uses the OpenSSL library and acts as a server. After executing the above trace OpenSSL crashes with a segementation fault.