Formal Verification of Privacy in Pervasive Systems

Mancini, Loretta Ilaria (2015). Formal Verification of Privacy in Pervasive Systems. University of Birmingham. Ph.D.

PDF - Accepted Version

Download (1MB)


Pervasive systems enhance a user's everyday experience. However, the use of pervasive sensing and context aware devices can result very intrusive from a privacy perspective. A familiar pervasive device is a mobile phone. Mobile telephony equipment is daily carried everywhere. Avoiding linkability of subscribers by third
parties, and protecting their privacy is one of the goals of mobile telecommunication protocols.

We use experimental and formal methods to model and analyse the security properties of mobile telephony protocols. We expose novel threats to the user privacy, which make it possible to trace and identify mobile
telephony subscribers, and for some of the attacks we demonstrate the feasibility of a low cost implementation. We propose fixes to these privacy issues. We prove that our privacy friendly fixes satisfy the desired unlinkability and anonymity properties. Finally, we develop the first extension of the Pro Verif tool for the automatic verification of equivalence based properties of stateful protocols.

This work shows how to formally verity privacy properties of pervasive systems. Moreover, we develop an automatic verification tool for the verification of equivalence based properties of stateful protocols. Further work in this direction will eventually widen the class of security protocols and security properties verifiable
using automatic verification tools.

Type of Work: Thesis (Doctorates > Ph.D.)
Award Type: Doctorates > Ph.D.
College/Faculty: Colleges (2008 onwards) > College of Engineering & Physical Sciences
School or Department: School of Computer Science
Funders: Engineering and Physical Sciences Research Council
Subjects: T Technology > T Technology (General)


Request a Correction Request a Correction
View Item View Item


Downloads per month over past year