Specification, Design, and Verification of an Accountability-aware Surveillance Protocol

Though controversial, surveillance activities are more and more performed for security reasons. However, such activities are extremely privacy-intrusive. This is seen as a necessary side-effect to ensure the success of such operations. In this paper, we propose an accountability-aware protocol designed for surveillance purposes. It relies on a strong incentive for a surveillance organisation to register its activity to a data protection authority. We first elicit a list of account-ability requirements, we provide an architecture showing the interaction of the different involved parties, and we propose an accountability-aware protocol which is formally specified in the applied pi calculus. We use the ProVerif tool to automatically verify that the protocol respects confidentiality, integrity and authentication properties.