POPSTAR

The shrinking size of microprocessors as well as the ubiquity of wireless communication have led to the proliferation of portable computing devices with novel security requirements. Whereas traditional security protocols achieve their security goals relying solely on cryptographic primitives like encryptions and hash functions, the protocols employed to secure these devices establish and rely in addition on properties of the physical world. For instance, they may use, as basic building blocks, protocols for ensuring physical proximity, secure localisation, or secure neighbourhood discovery. The aim of the POPSTAR ERC project is to develop techniques and tools to analyse protocols that establish and rely on properties of the physical world. We foresee that, at the end of the project, appropriate verification tools will be available to analyse the security and privacy of these "physical protocols". The research community in logics, program verification, and security has already a long tradition in developing techniques and tools to analyse key establishment and authentication protocols. Distance bounding protocols which are used to provide secure proximity control, raise new research challenges, and can not be analysed today using off-the-shelf verification tools.