key: 2015-automated-verification-of-secrecy-using-phases
type: inproceedings
title: Automatically Checking Commitment Protocols in ProVerif without False Attacks
authors:
  - Tom Chothia
  - Ben Smyth
  - Chris Staite
year: 2015
month: 1
booktitle: "POST'15: 4th Conference on Principles of Security and Trust"
series: LNCS
volume: "9036"
publisher: Springer
doi: 10.1007/978-3-662-46666-7_8
description: >-
  This paper introduces techniques for analysing secrecy using ProVerif. The techniques rely on
  inserting phases to avoid some false attacks.
keywords: >-
  Analysis, applied pi calculus, automated reasoning, BlueTooth, commitment protocols, false
  attacks, formal methods, pairing protocol, phases, ProVerif, protocol, reachability, secrecy,
  security, verification
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.
links:
  - file: Smyth15-analysing-secrecy-using-phases.pdf
    text: Conference paper
  - url: https://doi.org/10.1007/978-3-662-46666-7_8
    text: Official version