(************************************ ================================================================ Modelling AS02 protocol in ProVerif ================================================================ Let the price list be: p1, p2, p3, and p1