Generated Proverif specification can't be equivalent to an example model
The targeted model is "pineedham-shr-orig4-comp.pi".
Here are the impactful differences between the pvspec and the example:
"param keyCompromise = strict." can't be added. It ensures compromised sessions end before non-compromised ones start.
The getKey function should be private.
Keys that are generated by a process should be instantiated in Process___0 instead of Process___start. For instance, in the example, "new k" should be in S___0 instead of S___start.
The same thing applies to keys that are passed as a parameter. Instantiating a key in the init process, then passing it to ___start, and then exchanging it in a channel to ___0 is not equivalent to passing the key directly to ___0.
Finally, removing all ___start processes completely allows to have the expected results.