Ensuring Privacy in Location-Based Services: An Approach Based on Opacity Enforcement

With the proliferation of mobile devices, Location-Based Services (LBS) that provide networked services based on users' locations have become increasingly popular. Such services, providing personalized and timely information, have raised privacy concerns such as unwanted revelation of users' current locations to potential stalkers. Many prior studies have proposed to address LBS privacy by sending “cloaking queries” that contain coarser location information. However, this method has been shown to be insufficient and no formal methodology exists for enforcing LBS privacy in mobile environments. In this work, we show that this problem can be formally addressed using the notion of opacity in discrete event systems. We use non-deterministic finite-state automata to capture the mobility patterns of users and label the transitions by the location information in the queries. Using opacity verification techniques, we show that the technique of sending cloaking queries to the server can still reveal the exact location of the user. To enforce location privacy, we apply the opacity enforcement technique by event insertion proposed in our prior work. Specifically, we synthesize suitable insertion functions that insert fake queries into the cloaking query sequences. The generated fake queries are always consistent with the mobility model of the user and provably ensure privacy of the user's current location. Finally, to minimize the overhead from fake queries, we design an optimal insertion function that introduces minimum average number of fake queries.