A Sound Abstraction of the Parsing Problem (Extended Version)

Research output: Book/ReportReportResearch

130 Downloads (Pure)

Abstract

In formal verification, cryptographic messages are often represented by algebraic terms. This abstracts not only from the intricate details of the real cryptography, but also from the details of the non-cryptographic aspects: the actual formatting and structuring of messages. We introduce a new algebraic model to include these details and define a small, simple language to precisely describe message formats. We support fixed-length fields, variablelength fields with offsets, tags, and encodings into smaller alphabets like Base64, thereby covering both classical formats as in TLS and modern XML-based formats. We define two reasonable properties for a set of formats used in a protocol suite. First, each format should be un-ambiguous: any string can be parsed in at most one way. Second, the formats should be pairwise disjoint: a string can be parsed as at most one of the formats. We show how to easily establish these properties for many practical formats. By replacing the formats with free function symbols we obtain an abstract model that is compatible with all existing verification tools.We prove that the abstraction is sound for unambiguous, disjoint formats: there is an attack in the concrete message model if there is one in the abstract message model. Finally we present highlights of a practical case study on TLS.
Original languageEnglish
PublisherDTU Compute
Number of pages16
Publication statusPublished - 2014
SeriesDTU Compute-Technical Report-2014
Number12
ISSN1601-2321

Keywords

  • Security protocols
  • Formal verification
  • Message formats
  • Soundness
  • Compositional reasoning

Fingerprint Dive into the research topics of 'A Sound Abstraction of the Parsing Problem (Extended Version)'. Together they form a unique fingerprint.

Cite this