Protocol analysis with time

Damián Aparicio-Sánchez, Santiago Escobar, Catherine Meadows, José Meseguer, Julia Sapiña

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationProgress in Cryptology – INDOCRYPT 2020 - 21st International Conference on Cryptology in India 2020, Proceedings
EditorsKarthikeyan Bhargavan, Elisabeth Oswald, Manoj Prabhakaran
PublisherSpringer Science and Business Media Deutschland GmbH
Pages128-150
Number of pages23
ISBN (Print)9783030652760
DOIs
StatePublished - 2020
Event21st International Conference on Cryptology in India, INDOCRYPT 2020 - Bangalore, India
Duration: Dec 13 2020Dec 16 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12578 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st International Conference on Cryptology in India, INDOCRYPT 2020
CountryIndia
CityBangalore
Period12/13/2012/16/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Protocol analysis with time'. Together they form a unique fingerprint.

Cite this