Data Access Specification and the Most Powerful Symbolic Attacker in MSR

Abstract

Most systems designed for the symbolic verification of security protocols operate under the unproved assumption that an attack can only result from the combination of a fixed number of message transformations, which altogether constitute the capabilities of the so-called Dolev-Yao intruder. In this paper, we show that the Dolev-Yao intruder can indeed emulate the actions of an arbitrary symbolic adversary. In order to do so, we extend MSR, a flexible specification framework for security protocols based on typed multiset rewriting, with a static check called data access specification and aimed at catching specification errors such as a principal trying to use a key that she is not entitled to access.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 2002
Accession Number
ADA484516

Entities

People

  • Iliano Cervesato

Tags

Communities of Interest

  • Air Platforms
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Asymetric Encryption
  • Authentication
  • Coding
  • Computer Access Control
  • Computer Science
  • Construction
  • Cryptography
  • Cybersecurity
  • Language
  • Notation
  • Security
  • Security Protocols
  • Specifications
  • Standards
  • Validation
  • Verification

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.
  • Strategic Security Studies