- Abstract:
-
Automated tools for finding attacks on flawed security protocols ofthen fail to deal adequately with group protocols. This is because the abstractions made to improve performance on fixed 2 or 3 party protocols either preclude the modelling of group protocols all together, or permit modelling only in a fixed scenario, which can prevent attacks from being discovered. This paper describes CORAL, a tool for finding counterexamples to incorrect inductive conjectures, which we have used to model protocols for both group key agreement and group key management, without any restrictions on the scenario. We will show how we used CORAL to discover 6 previously unknown attacks on 3 group protocols
- Links To Paper
- 1st link
- Bibtex format
- @Article{EDI-INF-RR-0268,
- author = {
Graham Steel
and Alan Bundy
},
- title = {Attacking Group Protocols by Refuting Incorrect Inductive Conjectures},
- journal = {Journal of Automated Reasoning, Volume 36, Numbers 1-2, January 2006.},
- publisher = {Springer},
- year = 2006,
- month = {Jan},
- volume = {36},
- pages = {149-176},
- doi = {10.1007/s10817-005-9016-8},
- url = {http://homepages.inf.ed.ac.uk/gsteel/papers/jar-05.pdf},
- }
|
