Protocol Analysis with Time and Space

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

Research output: Chapter in Book/Report/Conference proceedingChapter


We present a formal framework for the analysis of cryptographic protocols that make use of time and space in their execution. In a previous work we provided a timed process algebra syntax and a timed transition semantics. The timed process algebra only made message sending-and-reception times available to processes whereas the timed transition semantics modelled the actual time interactions between processes. In this paper we extend the previous process algebra syntax to make spatial location information also available to processes and provide a transition semantics that takes account of fundamental properties of both time and space. This time and space protocol framework can be implemented either as a simulation tool or as a symbolic analysis tool in which time and space information are not represented by specific values but by logical variables, and in which the properties of time and space are reasoned about in terms of constraints on those time and space logical variables. All these time and space constraints are carried along the symbolic execution of the protocol and their satisfiability can be evaluated as the analysis proceeds, so attacks that violate the laws of physics can be discarded 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 and location constraints. We provide a sound and complete protocol transformation from our time and space process algebra to the Maude-NPA syntax and semantics, and we prove its soundness and completeness. We analyze two protocols using time and space constraints.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Number of pages28
StatePublished - 2021

Publication series

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Protocol Analysis with Time and Space'. Together they form a unique fingerprint.

Cite this