Formal Analysis of a Privacy-Preserving Billing Protocol