Towards the automated verification of cyber-physical security protocols: bounding the number of timed intruders

DOI10.1007/978-3-319-45741-3_23MaRDI QIDQ2165489zbMATH OpenOpenAlexFDO

Authors Vivek Nigam, Carolyn Talcott, Abraão Aires Urquiza

Publication date 19 August 2022

Full work available at URL https://arxiv.org/abs/1605.08563

Mathematics Subject Classification ID

Computer security (68M25) Specification and verification (program logics, model checking, etc.) (68Q60) Cryptography (94A60)

Abstract: 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.

Recommendations

• Timed automata based model checking of timed security protocols
• Is Your Security Protocol on Time ?
• Automated verification of timed security protocols with clock drift
• Modelling and checking timed authentication of security protocols
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(6)

• Protocol analysis with time
• Protocol analysis with time and space
• Automated synthesis of enforcing mechanisms for security properties in a timed setting
• A Symbolic Framework to Analyse Physical Proximity in Security Protocols
• Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems
• Measuring robustness in cyber-physical systems under sensor attacks

This page was built for publication: Towards the automated verification of cyber-physical security protocols: bounding the number of timed intruders

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2165489)