Stéphanie Delaune: Formal verification of protocols based on short authenticated strings

Formal verification of protocols based on short authenticated strings

Stéphanie Delaune, Steve Kremer, and Ludovic Robin. Formal verification of protocols based on short authenticated strings. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), IEEE Computer Society Press, Santa Barbara, CA, USA, August 2017.

Download

[PDF]

Abstract

Modern security protocols may involve humans, in order to compare or copy short strings between different devices. Multi-factor authentication protocols, such as Google 2-factor or 3D-secure are typical examples of such protocols. However, such short strings may be subject to brute force attacks. In this paper we propose a symbolic model which includes attacker capabilities for guessing short strings, and producing collisions when short strings are produced by weak hash functions. We propose a new decision procedure for analysing (a bounded number of sessions of) protocols that rely on short strings. The procedure has been integrated in the Akiss tool and tested on protocols from the ISO/IEC 9798-6:2010 standard.

BibTeX

@inproceedings{DKR-csf17,
  abstract =      {
  Modern security protocols may involve humans, in order to compare or
  copy short strings between different devices. Multi-factor
  authentication protocols, such as Google 2-factor or 3D-secure are
  typical examples of such protocols. However, such short strings may
  be subject to brute force attacks. 
  In this paper we
  propose a symbolic model which includes attacker capabilities for
  guessing short strings, and producing collisions when short strings
  are produced by weak hash functions. We propose a new decision
  procedure for analysing (a bounded number of sessions of) protocols
  that rely on short strings. The procedure has been integrated in the
  Akiss tool and tested on protocols from the ISO/IEC 9798-6:2010 standard.
},
  address =       {Santa Barbara, CA, USA},
  author =        {Delaune, St{\'e}phanie and Kremer, Steve and Robin, Ludovic},
  booktitle =     {{P}roceedings of the 30th {IEEE} {C}omputer
                   {S}ecurity {F}oundations {S}ymposium ({CSF}'17)},
  month =         aug,
  OPTpages =         {},
  publisher =     {{IEEE} Computer Society Press},
  title =         {Formal verification of protocols based on short authenticated strings},
  year =          {2017},
  acronym =       {{CSF}'17},
  nmonth =        {8},
  OPTLONGPDF =       {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
                  DKR-csf17-long.pdf},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}