A Formal Privacy System and Its Application to Location Based Services