Formal Analysis of Privacy for Anonymous Location Based Services (bibtex)
by Morten Dahl, Stéphanie Delaune, Graham Steel
Abstract:
We propose a framework for formal analysis of privacy in location based services such as anonymous electronic toll collection. We give a formal definition of privacy, and apply it to the VPriv scheme for vehicular services. We analyse the resulting model using the ProVerif tool, concluding that our privacy property holds only if certain conditions are met by the implementation. Our analysis includes some novel features such as the formal modelling of privacy for a protocol that relies on interactive zero-knowledge proofs of knowledge and list permutations.
Reference:
Formal Analysis of Privacy for Anonymous Location Based Services (Morten Dahl, Stéphanie Delaune, Graham Steel), In Proceedings of the Workshop on Theory of Security and Applications (TOSCA'11), 2011.
Bibtex Entry:
@inproceedings{DDS-tosca11,
  abstract =      {We propose a framework for formal analysis of privacy
                   in location based services such as anonymous
                   electronic toll collection. We give a formal
                   definition of privacy, and apply it to the VPriv
                   scheme for vehicular services. We analyse the
                   resulting model using the ProVerif tool, concluding
                   that our privacy property holds only if certain
                   conditions are met by the implementation. Our
                   analysis includes some novel features such as the
                   formal modelling of privacy for a protocol that
                   relies on interactive zero-knowledge proofs of
                   knowledge and list permutations.},
  address =       {Saarbr{\"u}cken, Germany},
  author =        {Dahl, Morten and Delaune, St{\'e}phanie and
                   Steel, Graham},
  booktitle =     {{P}roceedings of the {W}orkshop on {T}heory of
                   {S}ecurity and {A}pplications ({TOSCA}'11)},
  month =         mar # "-" # apr,
  title =         {Formal Analysis of Privacy for Anonymous Location
                   Based Services},
  year =          {2011},
  acronym =       {{TOSCA}'11},
  nmonth =        {3},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDS-tosca11.pdf},
  PDF =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDS-tosca11.pdf},
  lsv-category =  {intc},
  lsv-status =    {apar},
  wwwpublic =     {public},
}
Powered by bibtexbrowser