Towards Formal Analysis of Insider Threats for Auctions

Florian Kammueller, Manfred Kerber, Christian W. Probst

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

Abstract

This paper brings together the world of insider threats and auctions. For online-auction systems, like eBay, but also for high-value one-off auction algorithms as they are used for selling radio wave frequencies, the use of rigorous machine supported modelling and verification techniques is meaningful to prove correctness and scrutinize vulnerability to security and privacy attacks. Surveying the threats in auctions and insider collusions, we present an approach to model and analyze auction protocols for insider threats using the interactive theorem prover Isabelle. As a case study, we use the cocaine auction protocol that represents a nice combination of cryptographic techniques, protocols, and privacy goals suitable for highlighting insider threats for auctions.
Original languageEnglish
Title of host publicationProceedings of the 8th ACM CCS International Workshop on Managing Insider Security Threats, MIST '16
PublisherAssociation for Computing Machinery
Publication date2016
Pages23-34
ISBN (Print)978-1-4503-4571-2
DOIs
Publication statusPublished - 2016
Event 8th ACM CCS International Workshop on Managing Insider Security Threats - Vienna, Austria
Duration: 28 Oct 2016 → …
Conference number: 8

Workshop

Workshop 8th ACM CCS International Workshop on Managing Insider Security Threats
Number8
CountryAustria
CityVienna
Period28/10/2016 → …

Keywords

  • Insider Threat
  • Auctions
  • Formal Methods

Cite this

Kammueller, F., Kerber, M., & Probst, C. W. (2016). Towards Formal Analysis of Insider Threats for Auctions. In Proceedings of the 8th ACM CCS International Workshop on Managing Insider Security Threats, MIST '16 (pp. 23-34). Association for Computing Machinery. https://doi.org/10.1145/2995959.2995963