Intruder deduction problem for locally stable theories with normal forms and inverses
- Submitting institution
-
King's College London
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 87030215
- Type
- D - Journal article
- DOI
-
10.1016/j.tcs.2017.01.027
- Title of journal
- Theoretical Computer Science
- Article number
- TCS-D-14-00678R4
- First page
- 64
- Volume
- 672
- Issue
- -
- ISSN
- 0304-3975
- Open access status
- Compliant
- Month of publication
- February
- Year of publication
- 2017
- URL
-
-
- 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
-
2
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Intruder deduction is an important problem in security-protocol analysis. This paper provides a characterisation of equational theories for which this problem is decidable. Novel rewriting techniques to analyse intruder knowledge are developed, which, unlike previous approaches, provide fine-grained characterisations of deduction that are general enough to cover all the usual theories in cryptographic protocols. Moreover, using these techniques, the paper identifies and corrects errors in a highly influential award-winning paper (see Section 4). A published MathSciNet review (MR3627366) concluded that the paper "offers a wealth of nice results which will surely be helpful in the field of security protocols".
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -