Automatically checking commitment protocols in ProVerif without false attacks

Tom Chothia, Ben Smyth, Christopher Staite

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Citations (Scopus)
170 Downloads (Pure)

Abstract

ProVerif over-approximates the attacker’s power to enable verification of processes under replication. Unfortunately, this results in ProVerif finding false attacks. This problem is particularly common in protocols whereby a participant commits to a particular value and later reveals their value. We introduce a method to reduce false attacks when analysing secrecy. First, we show how inserting phases into non- replicated processes enables a more accurate translation to Horn clauses which avoids some false attacks. Secondly, we generalise our methodology to processes under replication. Finally, we demonstrate the applicability of our technique by analysing BlueTooth Simple Pairing. Moreover, we propose a simplification of this protocol that achieves the same security goal.
Original languageEnglish
Title of host publicationPrinciples of Security and Trust
Subtitle of host publication4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
EditorsRiccardo Focardi, Andrew Myers
PublisherSpringer
Pages137-155
Volume9036
ISBN (Electronic) 9783662466667
ISBN (Print)9783662466650
DOIs
Publication statusPublished - 11 Apr 2015
Event4th International Conference on Principles of Security and Trust (POST) - London, United Kingdom
Duration: 11 Apr 201517 Apr 2015

Publication series

NameLecture Notes in Computer Science
Volume9036
ISSN (Print)0302-9743

Conference

Conference4th International Conference on Principles of Security and Trust (POST)
Country/TerritoryUnited Kingdom
CityLondon
Period11/04/1517/04/15

Fingerprint

Dive into the research topics of 'Automatically checking commitment protocols in ProVerif without false attacks'. Together they form a unique fingerprint.

Cite this