University of Limerick
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, the authors outline an extension of their 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. They achieve this by using the output of the ALLIGATOR theorem prover, which constructs explicit and checkable proof objects. They 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.