Unbounded verification, falsification, and characterization of security protocols by pattern refinement