Using Interval Logics for Temporal  Analysis of Security Protocols

Michael Reichhardt Hansen; Robin Sharp; Michael Backes et a.

doi:10.1145/1035429.1035432

Using Interval Logics for Temporal Analysis of Security Protocols

Michael Reichhardt Hansen
, Robin Sharp
, Michael Backes et a. (Editor)

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Abstract

This paper presents an approach to the analysis of real-time properties of security protocols, based on the use of Interval Logic with durations to express and reason about temporal phenomena. We focus on the analysis of availability, where time is known to play a significant role, illustrate how relevant timing requirements can be formulated and show how Interval Logic can be used to prove that a system can fulfil these requirements in the presence of attackers of a given strength. We link this logic-based approach to more operational approaches.

Original language	English
Title of host publication	Proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering, FMSE'03
Publisher	ACM Press
Publication date	2003
Pages	24-31
ISBN (Print)	978-158113781-1
DOIs	https://doi.org/10.1145/1035429.1035432
Publication status	Published - 2003
Event	ACM Workshop on Formal Methods in Security Engineering - Duration: 30 Oct 2003 → 30 Oct 2003

Workshop

Workshop	ACM Workshop on Formal Methods in Security Engineering
Period	30/10/2003 → 30/10/2003

Access to Document

10.1145/1035429.1035432

OpenUrl availability

Check availability in DTU Findit

Cite this

@inproceedings{23bf41c968784694a289cec0962c692c,

title = "Using Interval Logics for Temporal Analysis of Security Protocols",

abstract = "This paper presents an approach to the analysis of real-time properties of security protocols, based on the use of Interval Logic with durations to express and reason about temporal phenomena. We focus on the analysis of availability, where time is known to play a significant role, illustrate how relevant timing requirements can be formulated and show how Interval Logic can be used to prove that a system can fulfil these requirements in the presence of attackers of a given strength. We link this logic-based approach to more operational approaches.",

author = "Hansen, \{Michael Reichhardt\} and Robin Sharp and \{Backes et a.\}, Michael",

year = "2003",

doi = "10.1145/1035429.1035432",

language = "English",

isbn = "978-158113781-1",

pages = "24--31",

booktitle = "Proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering, FMSE'03",

publisher = "ACM Press",

note = "ACM Workshop on Formal Methods in Security Engineering, FMSE'03 ; Conference date: 30-10-2003 Through 30-10-2003",

}

Using Interval Logics for Temporal Analysis of Security Protocols. / Hansen, Michael Reichhardt ; Sharp, Robin; Backes et a., Michael (Editor).
Proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering, FMSE'03. ACM Press, 2003. p. 24-31.

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Using Interval Logics for Temporal Analysis of Security Protocols

AU - Hansen, Michael Reichhardt

AU - Sharp, Robin

A2 - Backes et a., Michael

PY - 2003

Y1 - 2003

N2 - This paper presents an approach to the analysis of real-time properties of security protocols, based on the use of Interval Logic with durations to express and reason about temporal phenomena. We focus on the analysis of availability, where time is known to play a significant role, illustrate how relevant timing requirements can be formulated and show how Interval Logic can be used to prove that a system can fulfil these requirements in the presence of attackers of a given strength. We link this logic-based approach to more operational approaches.

AB - This paper presents an approach to the analysis of real-time properties of security protocols, based on the use of Interval Logic with durations to express and reason about temporal phenomena. We focus on the analysis of availability, where time is known to play a significant role, illustrate how relevant timing requirements can be formulated and show how Interval Logic can be used to prove that a system can fulfil these requirements in the presence of attackers of a given strength. We link this logic-based approach to more operational approaches.

U2 - 10.1145/1035429.1035432

DO - 10.1145/1035429.1035432

M3 - Article in proceedings

SN - 978-158113781-1

SP - 24

EP - 31

BT - Proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering, FMSE'03

PB - ACM Press

T2 - ACM Workshop on Formal Methods in Security Engineering

Y2 - 30 October 2003 through 30 October 2003