TY - GEN
T1 - Automatically checking commitment protocols in ProVerif without false attacks
AU - Chothia, Tom
AU - Smyth, Ben
AU - Staite, Christopher
PY - 2015/4/11
Y1 - 2015/4/11
N2 - 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.
AB - 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.
UR - http://www.cs.bham.ac.uk/~tpc/projects/falseattacks/
U2 - 10.1007/978-3-662-46666-7_8
DO - 10.1007/978-3-662-46666-7_8
M3 - Conference contribution
SN - 9783662466650
VL - 9036
T3 - Lecture Notes in Computer Science
SP - 137
EP - 155
BT - Principles of Security and Trust
A2 - Focardi, Riccardo
A2 - Myers , Andrew
PB - Springer
T2 - 4th International Conference on Principles of Security and Trust (POST)
Y2 - 11 April 2015 through 17 April 2015
ER -