Transformational verification of parameterized protocols using array formulas