Towards the Automated Verification of Cyber-Physical Security
Protocols: Bounding the Number of Timed Intruders


Timed Intruder Models have been proposed for the verification of
Cyber-Physical Security Protocols (CPSP) amending the traditional
Dolev-Yao intruder to obey the physical restrictions of the
environment. Since to learn a message, a Timed Intruder needs to
wait for a message to arrive, mounting an attack may depend on
where Timed Intruders are. It may well be the case that in the
presence of a great number of intruders there is no attack, but
there is an attack in the presence of a small number of well placed
intruders. Therefore, a major challenge for the automated
verification of CPSP is to determine how many Timed Intruders to
use and where should they be placed. This paper answers this
question by showing it is enough to use the same number of Timed
Intruders as the number of participants. We also report on some
preliminary experimental results in discovering attacks in CPSP.
More details appear in a paper at ESORICS 2016 available from
Nigam's homepage (http://www.nigam.info/).


Bio:

Vivek Nigam is an Associate Professor at the Federal University of
Paraíba. He obtained his PhD in Computational Logic from the École
Polytechnique in France. He was also a post-doctoral researcher at
UPENN and an Alexander von Humboldt postdoctoral researcher at LMU,
Germany. His current interests lie in the border between Formal
Methods, Cyber-Physical Systems, Protocol and Network Security,
Programming Languages and Foundations of Computer Security. For more
visit http://nigam.info/.