A number of papers utilising Tamarin (e.g. Secure Authentication in the Grid:
A formal analysis of DNP3: SAv5) use M4 to reorder rules in order to improve proof speed. Is anyone able to shed some light on how to work out this improved ordering?
Thanks in advance,