Steve Kremer: Adaptive Soundness of Static Equivalence

Adaptive Soundness of Static Equivalence

Steve Kremer and Laurent Mazaré. Adaptive Soundness of Static Equivalence. In Proceedings of the 3rd Workshop on Formal and Computational Cryptography (FCC'07), Venice, Italy, July 2007.

Download

[PDF]

Abstract

We define a framework to reason about implementations of equational theories in the presence of an adaptive adversary. We particularly focus on soundess of static equivalence. We illustrate our framework on different equational theories: symmetric encryption, modular exponentiation and also joint theories of encryption and modular exponentiation. Finally, we define a model for symbolic analysis of dynamic group key exchange protocols, and show its computational soundness.

BibTeX

@inproceedings{KM-FCC2007,
  abstract =      {We define a framework to reason about implementations
                   of equational theories in the presence of an adaptive
                   adversary. We~particularly focus on soundess of
                   static equivalence. We~illustrate our framework on
                   different equational theories: symmetric encryption,
                   modular exponentiation and also joint theories of
                   encryption and modular exponentiation. Finally, we
                   define a model for symbolic analysis of dynamic group
                   key exchange protocols, and show its computational
                   soundness.},
  address =       {Venice, Italy},
  author =        {Kremer, Steve and Mazar{\'e}, Laurent},
  booktitle =     {{P}roceedings of the 3rd {W}orkshop on {F}ormal and
                   {C}omputational {C}ryptography ({FCC}'07)},
  editor =        {Backes, Michael and Lakhnech, Yassine},
  month =         jul,
  title =         {Adaptive Soundness of Static Equivalence},
  year =          {2007},
  acronym =       {{FCC}'07},
  nmonth =        {7},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KM-fcc07.pdf},
}