Licensing Services: Formal Analysis and Implementation