A Sound Abstraction of the Parsing Problem

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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, variable-length 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 pair wise 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 un-ambiguous, 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
Title of host publicationProceedings of the IEEE 27th Computer Security Foundations Symposium, CSF 2014
PublisherIEEE
Publication date2014
Pages259-273
ISBN (Print)978-1-4799-4290-9
DOIs
Publication statusPublished - 2014
Event27th Computer Security Foundations Symposium (CSF 2014) - Vienna, Austria
Duration: 19 Jul 201422 Jul 2014
Conference number: 27
http://csf2014.di.univr.it/index

Conference

Conference27th Computer Security Foundations Symposium (CSF 2014)
Number27
CountryAustria
CityVienna
Period19/07/201422/07/2014
Internet address
SeriesI E E E Computer Security Foundations Symposium. Proceedings
ISSN1940-1434

Keywords

  • Computing and Processing
  • Abstracts
  • Algebra
  • compositional reasoning
  • Encoding
  • Encryption
  • formal verification
  • Law
  • message formats
  • Protocols
  • Security protocols
  • soundness

Cite this

Mödersheim, S. A., & Katsoris, G. (2014). A Sound Abstraction of the Parsing Problem. In Proceedings of the IEEE 27th Computer Security Foundations Symposium, CSF 2014 (pp. 259-273). IEEE. I E E E Computer Security Foundations Symposium. Proceedings https://doi.org/10.1109/CSF.2014.26