Where do they show this? What would such a handshake look like?

I'm not 100% percent certain but I think it's supposed to follow from 5.4? And it's more like we proof that the same can be done in less as equivalency steps? There also are two giant tex files in the cryptoverif folder of the repo that I did not bother compiling or reading yet. @keks might be able to shed a light on this.