Here is a list of my publications. Click on titles for abstracts and additionnal information.

1. Second Preimage Attacks on Dithered Hash Functions (EUCROCRYPT'08)
   Elena Andreeva, Charles Bouillaguet, Pierre-Alain Fouque, Jonathan Hoch, John Kelsey, Adi Shamir and Sebastien Zimmer, April 2008 hide

   • Accepted in EUROCRYPT'08 [ PS, PDF ]
     
   • Available on ePrint
   • Also see the presentations list
   • Abstract :

     We develop a new generic long-message second preimage attack, based on combining the techniques in the second preimage attacks of Dean and Kelsey and Schneier with the herding attack of Kelsey and Kohno. We show that these generic attacks apply to hash functions using the Merkle-Damgard construction with only slightly more work than the previously known attack, but allow enormously more control of the contents of the second preimage found. Additionally, we show that our new attack applies to several hash function constructions which are not vulnerable to the previously known attack, including the dithered hash proposal of Rivest, Shoup's UOWHF and the ROX hash construction. We analyze the properties of the dithering sequence used in, and develop a time-memory tradeoff which allows us to apply our second preimage attack to a wide range of dithering sequences, including sequences which are much stronger than those in Rivest's proposals. Finally, we show that both the existing second preimage attacks and our new attack can be applied even more efficiently to multiple target messages; in general, given a set of many target messages with a total of 2^R message blocks, these second preimage attacks can find a second preimage for one of those target messages with no more work than would be necessary to find a second preimage for a single target message of 2^R message blocks.

2. Sécurité et preuves de sécurité des fonctions de hachage (Master's thesis, in french)
   Charles Bouillaguet, September 2007 hide

   • Master's thesis : [ PS, PDF ]
     
   • Also see the presentations list
3. Using First-Order Theorem Provers in the Jahob Data Structure Verification System (VMCAI'07)
   Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee and Martin Rinard, January 2007 hide

   • Long version : [ PS, PDF ]
   • Tech report : [ PS, PDF ]
     
   • Also see the presentations list
   • Abstract :

     This paper presents our integration of efficient resolution-based theorem provers into the Jahob data structure verification system. Our experimental results show that this approach enables Jahob to automatically verify the correctness of a range of complex dynamically instantiable data structures, including data structures such as hash tables and search trees, without the need for interactive theorem proving or techniques tailored to individual data structures.

     Our primary technical results include: (1) a translation from higher-order logic to first-order logic that enables the application of resolution-based theorem provers and (2) a proof that eliminating type (sort) information in formulas is both sound and complete, even in the presence of a generic equality operator. Moreover, our experimental results show that the elimination of this type information dramatically decreases the time required to prove the resulting formulas.

     These techniques enabled us to verify complex correctness properties of Java programs such as a mutable set implemented as an imperative linked list, a finite map implemented as a functional ordered tree, a hash table with a mutable array, and a simple library system example that uses these container data structures. Our system verifies (in a matter of minutes) that data structure operations correctly update the finite map, that they preserve data structure invariants (such as ordering of elements, membership in appropriate hash table buckets, or relationships between sets and relations), and that there are no run-time errors such as null dereferences or array out of bounds accesses.