TY - GEN
T1 - Protocol analysis with time
AU - Aparicio-Sánchez, Damián
AU - Escobar, Santiago
AU - Meadows, Catherine
AU - Meseguer, José
AU - Sapiña, Julia
N1 - Funding Information:
This paper was partially supported by the EU (FEDER) and the Spanish MCIU under grant RTI2018-094403-B-C32, by the Spanish Generalitat Valenciana under grant PROMETEO/2019/098 and APOSTD/2019/127, by the US Air Force Office of Scientific Research under award number FA9550-17-1-0286, and by ONR Code 311.
Publisher Copyright:
© Springer Nature Switzerland AG 2020.
PY - 2020
Y1 - 2020
N2 - We present a framework suited to the analysis of cryptographic protocols that make use of time in their execution. We provide a process algebra syntax that makes time information available to processes, and a transition semantics that takes account of fundamental properties of time. Additional properties can be added by the user if desirable. This timed protocol framework can be implemented either as a simulation tool or as a symbolic analysis tool in which time references are represented by logical variables, and in which the properties of time are implemented as constraints on those time logical variables. These constraints are carried along the symbolic execution of the protocol. The satisfiability of these constraints can be evaluated as the analysis proceeds, so attacks that violate the laws of physics can be rejected as impossible. We demonstrate the feasibility of our approach by using the Maude-NPA protocol analyzer together with an SMT solver that is used to evaluate the satisfiability of timing constraints. We provide a sound and complete protocol transformation from our timed process algebra to the Maude-NPA syntax and semantics, and we prove its soundness and completeness. We then use the tool to analyze Mafia fraud and distance hijacking attacks on a suite of distance-bounding protocols.
AB - We present a framework suited to the analysis of cryptographic protocols that make use of time in their execution. We provide a process algebra syntax that makes time information available to processes, and a transition semantics that takes account of fundamental properties of time. Additional properties can be added by the user if desirable. This timed protocol framework can be implemented either as a simulation tool or as a symbolic analysis tool in which time references are represented by logical variables, and in which the properties of time are implemented as constraints on those time logical variables. These constraints are carried along the symbolic execution of the protocol. The satisfiability of these constraints can be evaluated as the analysis proceeds, so attacks that violate the laws of physics can be rejected as impossible. We demonstrate the feasibility of our approach by using the Maude-NPA protocol analyzer together with an SMT solver that is used to evaluate the satisfiability of timing constraints. We provide a sound and complete protocol transformation from our timed process algebra to the Maude-NPA syntax and semantics, and we prove its soundness and completeness. We then use the tool to analyze Mafia fraud and distance hijacking attacks on a suite of distance-bounding protocols.
UR - http://www.scopus.com/inward/record.url?scp=85098262466&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85098262466&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-65277-7_7
DO - 10.1007/978-3-030-65277-7_7
M3 - Conference contribution
AN - SCOPUS:85098262466
SN - 9783030652760
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 128
EP - 150
BT - Progress in Cryptology – INDOCRYPT 2020 - 21st International Conference on Cryptology in India 2020, Proceedings
A2 - Bhargavan, Karthikeyan
A2 - Oswald, Elisabeth
A2 - Prabhakaran, Manoj
PB - Springer
T2 - 21st International Conference on Cryptology in India, INDOCRYPT 2020
Y2 - 13 December 2020 through 16 December 2020
ER -