Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-642-22137-8_5 | Security Protocols Workshop |
Keywords | Field | DocType |
explicit list,security proof,modelled attacker,major obstacle,verification tool,dolev-yao attacker,security protocol,formal verification method,new approach,new environment | Obstacle,Attack model,Trusted third party,Cryptographic protocol,Computer security,Computer science,Mathematical proof,Formal verification | Conference |
Volume | ISSN | Citations |
6615 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 11 | 1 |