Well personally I would rather suggest to write a model, not a rigorous proof. A formal proof of any real protocol is both long and tedious journey; production guys will hardly find it useful thing to do.

On the other hand a logical model can be encoded in a rather short amount of time by someone who is doing it periodically.

This hypothetical guy could benefit from this activity by co-authoring the paper. Original authors would benefit from it by reinforcing both the protocol and the paper.