Investigating airplane safety and security against insider threats using logical modeling
- Submitting institution
-
Middlesex University
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1700
- Type
- E - Conference contribution
- DOI
-
10.1109/SPW.2016.47
- Title of conference / published proceedings
- 2016 IEEE Security and Privacy Workshops (SPW)
- First page
- 304
- Volume
- -
- Issue
- -
- ISSN
- 2375-1207
- Open access status
- Out of scope for open access requirements
- Month of publication
- May
- Year of publication
- 2016
- URL
-
http://eprints.mdx.ac.uk/19713/
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
1
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper pioneers the formal modelling and analysis of Airplane policies motivated by a tragic incident: the 2015 insider attack on a German airplane, in which all 150 people on board died. The work rigorously applies interactive theorem proving with the Isabelle Insider framework, motivating its extension with Kripke structures and the temporal logic CTL to enable reasoning on dynamic system states. This is significant because it can save lives and the induced extensions led to several publications. A comprehensive article published on Elsevier's Science of Computer Programming presents the resulting methodology and a comparative analysis to model checking.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -