A Trace Logic for Local Security Properties

TL;DR

This paper introduces a trace logic framework for specifying and verifying local security properties in cryptographic protocols, aiding protocol design and exposing vulnerabilities.

Contribution

It presents a new trace logic for local security properties, enabling formal specification and verification integrated into protocol design.

Findings

Identifies new attacks on the TMN protocol

Provides a formal method for local security property specification

Demonstrates the logic's utility in protocol analysis

Abstract

We propose a new simple \emph{trace} logic that can be used to specify \emph{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 protocol TMN.