Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures (bibtex)
by Graham Steel, Alan Bundy, Monika Maidl
Abstract:
Automated tools for finding attacks on flawed security protocols often struggle to deal with protocols for group key agreement. Systems designed for fixed 2 or 3 party protocols may not be able to model a group protocol, or its intended security properties. Frequently, such tools require an abstraction to a group of fixed size to be made before the automated analysis takes place. This can prejudice chances of finding attacks on the protocol. In this paper, we describe \textscCoral, our system for finding security protocol attacks by refuting incorrect inductive conjectures. We have used \textscCoral to model a group key protocol in a general way. By posing inductive conjectures about the trace of messages exchanged, we can investigate novel properties of the protocol, such as tolerance to disruption, and whether it results in agreement on a single key. This has allowed us to find three distinct novel attacks on groups of size two and three
Reference:
Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures (Graham Steel, Alan Bundy, Monika Maidl), In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR'04) (David A. Basin, Michaël Rusinowitch, eds.), Springer-Verlag, volume 3097, 2004.
Bibtex Entry:
@inproceedings{SBM-ijcar04,
  abstract =      {Automated tools for finding attacks on flawed
                   security protocols often struggle to deal with
                   protocols for group key agreement. Systems designed
                   for fixed 2 or 3 party protocols may not be able to
                   model a group protocol, or its intended security
                   properties. Frequently, such tools require an
                   abstraction to a group of fixed size to be made
                   before the automated analysis takes place. This can
                   prejudice chances of finding attacks on the protocol.
                   In this paper, we describe \textsc{Coral}, our system
                   for finding security protocol attacks by refuting
                   incorrect inductive conjectures. We have used
                   \textsc{Coral} to model a group key protocol in a
                   general way. By posing inductive conjectures about
                   the trace of messages exchanged, we can investigate
                   novel properties of the protocol, such as tolerance
                   to disruption, and whether it results in agreement on
                   a single key. This has allowed us to find three
                   distinct novel attacks on groups of size two and
                   three},
  address =       {Cork, Ireland},
  author =        {Steel, Graham and Bundy, Alan and Maidl, Monika},
  booktitle =     {{P}roceedings of the 2nd {I}nternational {J}oint
                   {C}onference on {A}utomated {R}easoning ({IJCAR}'04)},
  DOI =           {10.1007/b98691},
  editor =        {Basin, David A. and Rusinowitch, Micha{\"e}l},
  month =         aug,
  pages =         {137-151},
  publisher =     {Springer-Verlag},
  series =        {Lecture Notes in Artificial Intelligence},
  title =         {Attacking a Protocol for Group Key Agreement by
                   Refuting Incorrect Inductive Conjectures},
  volume =        {3097},
  year =          {2004},
  acronym =       {{IJCAR}'04},
  nmonth =        {8},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SBM-ijcar04.pdf},
  PDF =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SBM-ijcar04.pdf},
  lsv-category =  {intc},
  lsv-time =      {ant},
  wwwpublic =     {perso},
}
Powered by bibtexbrowser