How to model (and simplify) the SET payment phase for automated verification