Options
Do not model the attacker
Publikationstyp
Conference Paper
Date Issued
2011
Sprache
English
Author(s)
First published in
Number in series
6615 LNCS
Start Page
25
End Page
35
Citation
Security protocols XVI : 16th international workshop, Cambridge, UK, April 16 - 18, 2008 ; revised selected papers. - Berlin, 2011. - (Lecture Notes in Computer Science ; 6615 LNCS (): 25-35 (2011)
Contribution to Conference
Publisher DOI
Scopus ID
Publisher
Springer
We identify attacker modelling as major obstacle when searching for ways to defeat security protocols. For protocols verified to be secure, attacks are discovered. Since this problem is not limited to the Dolev-Yao attacker but applies to all modelled attackers, we propose a new approach. We argue that formal verification methods should be used to show the impact of analyst provided actions have on protocols. This approach frees verification tools from having to know all the actions an attacker could perform. We show the benefits of having both the security proof and an explicit list of considered actions. Implementers can easily determine if the protocol is suited for their application. Additionally, developers understand the requirements an implementation has to fulfil. Lastly, our approach allows proofs to be adapted to new environments without changing the verification tool.
DDC Class
004: Informatik