Insider threats and auctions: formalization, mechanized proof, and code generation

Research output: Contribution to journalArticlepeer-review

Standard

Insider threats and auctions: formalization, mechanized proof, and code generation. / Kammueller, Florian; Kerber, Manfred; Probst, Christian W.

In: Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications, Vol. 8, No. 1, 01.03.2017, p. 44-78.

Research output: Contribution to journalArticlepeer-review

Harvard

APA

Vancouver

Author

Bibtex

@article{1f957909b25b426f90c315970aa836b2,
title = "Insider threats and auctions: formalization, mechanized proof, and code generation",
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",
author = "Florian Kammueller and Manfred Kerber and Probst, {Christian W.}",
year = "2017",
month = mar,
day = "1",
doi = "10.22667/JOWUA.2017.03.31.044",
language = "English",
volume = "8",
pages = "44--78",
journal = "Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications",
issn = "2093-5374",
publisher = "Innovative Information Science & Technology Research Group (ISYOU)",
number = "1",

}

RIS

TY - JOUR

T1 - Insider threats and auctions: formalization, mechanized proof, and code generation

AU - Kammueller, Florian

AU - Kerber, Manfred

AU - Probst, Christian W.

PY - 2017/3/1

Y1 - 2017/3/1

N2 - 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.

AB - 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.

KW - Insider threats

KW - Auctions

KW - Formal Methods

KW - Code generation

U2 - 10.22667/JOWUA.2017.03.31.044

DO - 10.22667/JOWUA.2017.03.31.044

M3 - Article

VL - 8

SP - 44

EP - 78

JO - Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications

JF - Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications

SN - 2093-5374

IS - 1

ER -