|
Insider Threats and Auctions: Formalization, Mechanized Proof, and Code Generation Florian Kammueller1+,
Manfred Kerber2, and Christian W. Probst3 1Middlesex
University, The Burroughs London NW4 4BT, United Kingdom F.Kammueller@mdx.ac.uk 2University
of Birmingham, Edgbaston Birmingham B15 2TT, United
Kingdom M.Kerber@cs.bham.ac.uk 3Technical
University of Denmark, Anker Engelunds Vej 1 Bygning 101A 2800 Kgs. Lyngby, Denmark cwpr@dtu.dk Abstract This paper applies machine assisted formal methods to
explore insider threats for auctions. Auction systems, like eBay, are an
important problem domain for formal analysis because they challenge modelling
concepts as well as analysis methods. We use machine assisted formal
modelling and proof in Isabelle to demonstrate how security and privacy goals
of auction protocols can be formally verified. Applying the costly scrutiny
of formal methods is justified for auctions since privacy and trust are
prominent issues and auctions are sometimes designed for one-off occasions
where high bids are at stake. For example, when radio wave frequencies are on
sale, auctions are especially created for just one occasion where fair and
consistent behaviour is required. Investigating the
threats in auctions and insider collusions, we model and analyze auction
protocols for insider threats using the interactive theorem prover Isabelle.
We use the existing example of a fictitious cocaine auction protocol from the
literature to develop and illustrate our approach. Combining the Isabelle
Insider framework with the inductive approach to verifying security protocols
in Isabelle, we formalize the cocaine auction protocol, prove that this
formal definition excludes sweetheart deals, and also that collusion attacks
cannot generally be excluded. The practical implication of the formalization
is demonstrated by code generation. Isabelle allows generating code from
constructive specifications into the programming language Scala. We provide
constructive test functions for cocaine auction traces, prove within Isabelle
that these functions conform to the protocol definition, and apply code
generation to produce an implementation of the executable test predicate for
cocaine auction traces in Scala. Keywords: Insider Threats, Auctions,
Formal Methods, Code generation. +: Corresponding author: Florian Kammueller London,
United Kingdom, Tel: +44-2084-114930 Journal
of Wireless Mobile Networks, Ubiquitous Computing, and Dependable
Applications (JoWUA) |