A Trace Logic for Local Security Properties | Zendy

Ricardo Corin | Zendy; Sandro Etalle | Zendy; Pieter Hartel | Zendy; Antonio Durante | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Trace Logic for Local Security Properties

Author(s) -

Ricardo Corin,

Sandro Etalle,

Pieter Hartel,

Antonio Durante

Publication year - 2005

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2004.12.019

Subject(s) - computer science , trace (psycholinguistics) , cryptographic protocol , protocol (science) , simple (philosophy) , cryptographic primitive , cryptography , computer security , formal methods , theoretical computer science , programming language , medicine , philosophy , linguistics , alternative medicine , epistemology , pathology

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 specification. Our technique allows a protocol designer to provide a formal specification of the desired security properties, and integrate it naturally into the design process of cryptographic protocols. Furthermore, the logic can be used for formal verification. We illustrate the utility of our technique by exposing new attacks on the well studied TMN protocol

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research