Volume 4 - Issue 1
Design and Formal Analysis of A Group Signature Based Electronic Toll Pricing System
- Xihui Chen
Interdisciplinary Centre for Security, Reliability and Trust University of Luxembourg, Luxembourg
xihui.chen@uni.lu
- Gabriele Lenzini
Interdisciplinary Centre for Security, Reliability and Trust University of Luxembourg, Luxembourg
gabriele.lenzini@uni.lu
- Sjouke Mauw
Interdisciplinary Centre for Security, Reliability and Trust University of Luxembourg, Luxembourg, Faculty of Science, Technology and Communication University of Luxembourg, Luxembourg
sjouke.mauw@uni.lu
- Jun Pang
Faculty of Science, Technology and Communication University of Luxembourg, Luxembourg
jun.pang@uni.lu
Keywords: location privacy, electronic toll pricing, group signature, formal analysis, unlinkability
Abstract
Location-based vehicle services have been enduring a rapid growth with the prevalence of GNSS
technologies, nowadays freely available for everyone. Given the nature of location data, privacy is of
prime importance in services such as electronic tolling pricing (ETP) and pay-as-you-drive. In this
paper, we first propose a new electronic toll pricing system based on group signatures – GroupETP
which achieves a good balance between privacy and overhead imposed upon user devices. Second,
we give a comprehensive formal analysis of GroupETP. Our analysis, conducted by ProVerif, requires
some abstraction of the system and extensions to the existing analysis methods. The results
show that GroupETP satisfies the desired properties – correctness, accountability and unlinkability.