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.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:659153 |
| Date | January 2015 |
| Creators | Mancini, Loretta Ilaria |
| Publisher | University of Birmingham |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://etheses.bham.ac.uk//id/eprint/6105/ |
Page generated in 0.0022 seconds