Towards explaining rebuttals in security arguments

Yu, Yijun; Piwek, Paul; Tun, Thein Than and Nuseibeh, Bashar (2014). Towards explaining rebuttals in security arguments. In: 14th Workshop on Computational Models of Natural Argument, 10 Dec 2014, Krakow, Poland.

URL: http://cmna.csc.liv.ac.uk//CMNA14/Yu.pdf

Abstract

The satisfaction of software security requirements can be argued using supporting facts and domain assumptions. Sometimes, these facts or assumptions may be questioned, as more knowledge about vulnerabilities becomes available. This results in rebuttals that can be derived from the new information. In this paper, we outline an extension of our OpenArgue tool with an explanation facility that makes a rebuttal more transparent by showing, step by step, why the original security argument does not hold. We achieve this by using the output of the Alligator theorem prover, which constructs explicit and checkable proof objects. We illustrate the feasibility of this approach by applying it to an existing case study of a PIN entry device which involves a security argument that has been rebutted. The output of the prover enables us to unpack the logical reasoning behind the rebuttal at a much greater level of detail. This promises to be useful for argument explanation.

Viewing alternatives

Item Actions

Export

You can export this page using these formats