An intruder model for verifying liveness in security protocols

J.G. Cederquist; Muhammad Torabi Dashti

doi:10.1145/1180337.1180340

An intruder model for verifying liveness in security protocols

J.G. Cederquist, Muhammad Torabi Dashti

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

11 Citations (Scopus)

4 Downloads (Pure)

Abstract

We present a process algebraic intruder model for verifying a class of liveness properties of security protocols. For this class, the proposed intruder model is proved to be equivalent to a Dolev-Yao intruder that does not delay indefinitely the delivery of messages. In order to prove the equivalence, we formalize the resilient communication channels assumption. As an application of the proposed intruder model, formal verification of fair exchange protocols is discussed.

Original language	Undefined
Title of host publication	FMSE '06: Proceedings of the fourth ACM workshop on Formal methods in security
Place of Publication	New York
Publisher	Association for Computing Machinery
Pages	23-32
Number of pages	10
ISBN (Print)	1-59593-550-9
DOIs	https://doi.org/10.1145/1180337.1180340
Publication status	Published - 2006
Event	Fourth ACM Workshop on Formal Methods in Security, FMSE '06 - Alexandria, Virginia, USA Duration: 3 Nov 2006 → 3 Nov 2006

Publication series

Name
Publisher	ACM

Workshop

Workshop	Fourth ACM Workshop on Formal Methods in Security, FMSE '06
Period	3/11/06 → 3/11/06
Other	November 3, 2006

Keywords

SCS-Cybersecurity
EWI-9140
METIS-237420
IR-63933

Access to Document

10.1145/1180337.1180340

Cite this

@inproceedings{344a21d8e93646f5ac44f5b536f48686,

title = "An intruder model for verifying liveness in security protocols",

abstract = "We present a process algebraic intruder model for verifying a class of liveness properties of security protocols. For this class, the proposed intruder model is proved to be equivalent to a Dolev-Yao intruder that does not delay indefinitely the delivery of messages. In order to prove the equivalence, we formalize the resilient communication channels assumption. As an application of the proposed intruder model, formal verification of fair exchange protocols is discussed.",

keywords = "SCS-Cybersecurity, EWI-9140, METIS-237420, IR-63933",

author = "J.G. Cederquist and Dashti, {Muhammad Torabi}",

note = "10.1145/1180337.1180340 ; Fourth ACM Workshop on Formal Methods in Security, FMSE '06 ; Conference date: 03-11-2006 Through 03-11-2006",

year = "2006",

doi = "10.1145/1180337.1180340",

language = "Undefined",

isbn = "1-59593-550-9",

publisher = "Association for Computing Machinery",

pages = "23--32",

booktitle = "FMSE '06: Proceedings of the fourth ACM workshop on Formal methods in security",

address = "United States",

}

Cederquist, JG & Dashti, MT 2006, An intruder model for verifying liveness in security protocols. in FMSE '06: Proceedings of the fourth ACM workshop on Formal methods in security., 10.1145/1180337.1180340, Association for Computing Machinery, New York, pp. 23-32, Fourth ACM Workshop on Formal Methods in Security, FMSE '06, 3/11/06. https://doi.org/10.1145/1180337.1180340

An intruder model for verifying liveness in security protocols. / Cederquist, J.G.; Dashti, Muhammad Torabi.
FMSE '06: Proceedings of the fourth ACM workshop on Formal methods in security. New York: Association for Computing Machinery, 2006. p. 23-32 10.1145/1180337.1180340.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - An intruder model for verifying liveness in security protocols

AU - Cederquist, J.G.

AU - Dashti, Muhammad Torabi

N1 - 10.1145/1180337.1180340

PY - 2006

Y1 - 2006

N2 - We present a process algebraic intruder model for verifying a class of liveness properties of security protocols. For this class, the proposed intruder model is proved to be equivalent to a Dolev-Yao intruder that does not delay indefinitely the delivery of messages. In order to prove the equivalence, we formalize the resilient communication channels assumption. As an application of the proposed intruder model, formal verification of fair exchange protocols is discussed.

AB - We present a process algebraic intruder model for verifying a class of liveness properties of security protocols. For this class, the proposed intruder model is proved to be equivalent to a Dolev-Yao intruder that does not delay indefinitely the delivery of messages. In order to prove the equivalence, we formalize the resilient communication channels assumption. As an application of the proposed intruder model, formal verification of fair exchange protocols is discussed.

KW - SCS-Cybersecurity

KW - EWI-9140

KW - METIS-237420

KW - IR-63933

U2 - 10.1145/1180337.1180340

DO - 10.1145/1180337.1180340

M3 - Conference contribution

SN - 1-59593-550-9

SP - 23

EP - 32

BT - FMSE '06: Proceedings of the fourth ACM workshop on Formal methods in security

PB - Association for Computing Machinery

CY - New York

T2 - Fourth ACM Workshop on Formal Methods in Security, FMSE '06

Y2 - 3 November 2006 through 3 November 2006

ER -