Automated Identification of Desynchronisation Attacks on Shared Secrets

Key-updating protocols are a class of communication protocol
that aim to increase security by having the participants change encryption
keys between protocol executions. However, such protocols can
be vulnerable to desynchronisation attacks, a denial of service attack in
which the agents are tricked into updating their keys improperly, so that
they are no longer able to communicate. In this work we introduce a
method that can be used to automatically verify (or falsify) resistance to
desynchronisation attacks for a range of protocols. This approach is then
used to identify previously unreported vulnerabilities in two published
RFID grouping protocols.