Séminaire SoSySec

Sécurité des logiciels et des systèmes

Accueil     Présentation     Archives

Florian Kammueller (Middlesex University London)


Formal Analysis of Insider Threats for Auctions

This talk 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 crucial. It allows proving correctness, scrutinizing vulnerability to security and privacy attacks, and generating certified code. 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.