A Trace Logic for Local Security Properties

Ricardo Corin; Antonio Durante; Sandro Etalle; Pieter Hartel

A Trace Logic for Local Security Properties

Ricardo Corin, Antonio Durante, Sandro Etalle, Pieter Hartel

Research output: Book/Report › Report › Other research output

73 Downloads (Pure)

Abstract

We propose a new simple trace logic that can be used to specify local security properties, i.e. security properties that refer to a single participant of the protocol specication. Our technique allows a protocol designer to provide formal specication of the desired security properties, and integrate them naturally to the design process of cryptographic protocols. Furthermore, the logic can be used for formal verication. We illustrate the utility of our technique by exposing new attacks on the well studied protocol TMN.

Original language	English
Place of Publication	Enschede
Publisher	Centre for Telematics and Information Technology (CTIT)
Number of pages	11
Publication status	Published - Apr 2003

Publication series

Name	CTIT technical reports series
Publisher	University of Twente, Centre for Telematics and Information Technology (CTIT)
No.	TR-CTIT-03-21

Keywords

EC Grant Agreement nr.: FP5/34734
SCS-Cybersecurity

Access to Document

Corin03traceFinal published version, 157 KB

http://www.ub.utwente.nl/webdocs/ctit/1/000000c4.pdf

Cite this

@book{7824ab6d6f86428cba1f83f612798a76,

title = "A Trace Logic for Local Security Properties",

abstract = "We propose a new simple trace logic that can be used to specify local security properties, i.e. security properties that refer to a single participant of the protocol specication. Our technique allows a protocol designer to provide formal specication of the desired security properties, and integrate them naturally to the design process of cryptographic protocols. Furthermore, the logic can be used for formal verication. We illustrate the utility of our technique by exposing new attacks on the well studied protocol TMN.",

keywords = "EC Grant Agreement nr.: FP5/34734, SCS-Cybersecurity",

author = "Ricardo Corin and Antonio Durante and Sandro Etalle and Pieter Hartel",

year = "2003",

month = apr,

language = "English",

series = "CTIT technical reports series",

publisher = "Centre for Telematics and Information Technology (CTIT)",

number = "TR-CTIT-03-21",

address = "Netherlands",

}

TY - BOOK

T1 - A Trace Logic for Local Security Properties

AU - Corin, Ricardo

AU - Durante, Antonio

AU - Etalle, Sandro

AU - Hartel, Pieter

PY - 2003/4

Y1 - 2003/4

N2 - We propose a new simple trace logic that can be used to specify local security properties, i.e. security properties that refer to a single participant of the protocol specication. Our technique allows a protocol designer to provide formal specication of the desired security properties, and integrate them naturally to the design process of cryptographic protocols. Furthermore, the logic can be used for formal verication. We illustrate the utility of our technique by exposing new attacks on the well studied protocol TMN.

AB - We propose a new simple trace logic that can be used to specify local security properties, i.e. security properties that refer to a single participant of the protocol specication. Our technique allows a protocol designer to provide formal specication of the desired security properties, and integrate them naturally to the design process of cryptographic protocols. Furthermore, the logic can be used for formal verication. We illustrate the utility of our technique by exposing new attacks on the well studied protocol TMN.

KW - EC Grant Agreement nr.: FP5/34734

KW - SCS-Cybersecurity

M3 - Report

T3 - CTIT technical reports series

BT - A Trace Logic for Local Security Properties

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -