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

Revisiting and Improving Algorithms for the 3XOR Problem (Tr. on Symmetric Crypto, 2018)
Charles Bouillaguet, Claire Delaplace and PierreAlain Fouque hide
 paper : [ PDF]
 Abstract :
The 3SUM problem is a wellknown problem in computer science and many geometric problems have been reduced to it. We study the 3XOR variant which is more cryptologically relevant. In this problem, the attacker is given blackbox access to three random functions $F, G$ and $H$ and she has to find three inputs $x, y$ and $z$ such that $F(x) \oplus G(y) \oplus H(z) = 0$. The 3XOR problem is a difficult case of the moregeneral $k$list birthday problem.
Wagner's celebrated $k$list birthday algorithm, and the ones inspired by it, work by querying the functions more than strictly necessary from an informationtheoretic point of view. This gives some leeway to target a solution of a specific form, at the expense of processing a huge amount of data.
However, to handle such a huge amount of data can be very difficult in practice. This is why we first restricted our attention to solving the 3XOR problem for which the total number of queries to $F$, $G$ and $H$ is minimal. If they are $n$bit random functions, it is possible to solve the problem with roughly $\bigO{2^{n/3}}$ queries. In this setting, the folklore quadratic algorithm finds a solution after $\bigO{2^{2n/3}}$ operations.
We present a 3XOR algorithm that generalizes an idea of Joux, with complexity $\bigO{2^{2n/3} / n}$ in times and $\bigO{2^{n/3}}$ in space. This algorithm is practical: it is up to $3\times$ faster than the quadratic algorithm. Furthermore, using Bernstein's ‘‘clamping trick'', we show that it is possible to adapt this algorithm to any number of queries, so that it will always be at least as good as, if not better than, Wagner's descendants in the same settings.
We also revisit a 3SUM algorithm by BaranDemaineP\v{a}tra\c scu which is asymptotically $n^2 / \log^2 n$ times faster than the quadratic algorithm when adapted to the 3XOR problem, but is otherwise completely impractical.
To gain a deeper understanding of these problems, we embarked on a project to solve actual 3XOR instances for the SHA256 hash function. We believe that this was very beneficial and we present practical remarks, along with a 96bit 3XOR for SHA256.

Parallel Sparse PLUQ Factorization modulo p (PASCO, 2017)
Charles Bouillaguet, Claire Delaplace and MarieEmilie Voge hide
 paper : [ PDF ACM]
 Abstract :
In this paper, we present the results of our experiments to compute the rank of several large sparse matrices from Dumas's Sparse Integer Matrix Collection, by computing sparse PLUQ factorizations. Our approach consists in identifying as many pivots as possible before performing any arithmetic operation, based solely on the location of nonzero entries in the input matrix. These ``structural'' pivots are then all eliminated in parallel, in a single pass. We describe several heuristic structural pivot selection algorithms (the problem is NPhard). These algorithms allows us to compute the ranks of several large sparse matrices in a few minutes, versus many days using Wiedemann's algorithm. Lastly, we describe a multithread implementation using OpenMP achieving 70% parallel efficiency on 24 cores on the largest benchmark.

Fast LatticeBased Encryption: Stretching Spring (PQ Crypto, 2017)
Charles Bouillaguet, Claire Delaplace, PierreAlain Fouque and Paul Kirchner hide
 paper : [ PDF Springer]
 code : github
 Abstract :
The SPRING pseudorandom function (PRF) has been described by Banerjee, Brenner, Leurent, Peikert and Rosen at FSE 2014. It is quite fast, only 4.5 times slower than the AES (without hardware acceleration) when used in counter mode. SPRING is similar to the PRF of Banerjee, Peikert and Rosen from EUROCRYPT~2012, whose security relies on the hardness of the Learning With Rounding (LWR) problem, which can itself be reduced to hard lattice problems. However, there is no such chain of reductions relating SPRING to lattice problems, because it uses small parameters for efficiency reasons. Consequently, the heuristic security of SPRING is evaluated using known attacks and the complexity of the best known algorithms for breaking the underlying hard problem. In this paper, we revisit the efficiency and security of SPRING when used as a pseudorandom generator. We propose a new variant which is competitive with the AES in counter mode without hardware AES acceleration, and about four times slower than AES with hardware acceleration. In terms of security, we improve some previous analysis of SPRING and we estimate the security of our variant against classical algorithms and attacks. Finally, we implement our variant using AVX2 instructions, resulting in high performances on highend desktop computers.

Sparse Gaussian Elimination modulo p: an Update (CASC, 2016)
Charles Bouillaguet and Claire Delaplace hide
 paper : [ PDF Springer]
 Abstract :
This paper considers elimination algorithms for sparse matrices over finite fields. We mostly focus on computing the rank, because it raises the same challenges as solving linear systems, while being slightly simpler. We developed a new sparse elimination algorithm inspired by the GilbertPeierls sparse LU factorization, which is wellknown in the numerical computation community. We benchmarked it against the usual rightlooking sparse gaussian elimination and the Wiedemann algorithm using the Sparse Integer Matrix Collection of JeanGuillaume Dumas. We obtain large speedups (1000x and more) on many cases. In particular, we are able to compute the rank of several large sparse matrices in seconds or minutes, compared to days with previous methods.

New SecondPreimage Attacks on Hash Functions (Journal of Cryptology, 2016)
Elena Andreeva, Charles Bouillaguet, Orr Dunkelman, PierreAlain Fouque, Jonathan Hoch, John Kelsey, Adi Shamir, Sébastien Zimmer, October 2016 hide
 Springer website : http://link.springer.com/article/10.1007/s0014501592064.
 Abstract :
In this work, we present several new generic secondpreimage attacks on hash functions. Our first attack is based on the herding attack and applies to various Merkle–Damgårdbased iterative hash functions. Compared to the previously known longmessage secondpreimage attacks, our attack offers more flexibility in choosing the secondpreimage message at the cost of a small computational overhead. More concretely, our attack allows the adversary to replace only a few blocks in the original target message to obtain the second preimage. As a result, our new attack is applicable to constructions previously believed to be immune to such secondpreimage attacks. Among others, these include the dithered hash proposal of Rivest, Shoup’s UOWHF, and the ROX constructions. In addition, we also suggest several timememorydata tradeoff attack variants, allowing for a faster online phase, and even finding second preimages for shorter messages. We further extend our attack to sequences stronger than the ones suggested in Rivest’s proposal. To this end we introduce the kite generator as a new tool to attack any dithering sequence over a small alphabet. Additionally, we analyse the secondpreimage security of the basic tree hash construction. Here we also propose several secondpreimage attacks and their timememorydata tradeoff variants. Finally, we show how both our new and the previous secondpreimage attacks can be applied even more efficiently when multiple short messages, rather than a single long target message, are available.

Cryptographic Schemes Based on the ASASA Structure: Blackbox, Whitebox, and Publickey
(Asiacrypt'14)
Alex Biryukov, Charles Bouillaguet, and Dmitry Khovratovich, December 2014 hide
 paper (full version) : [ eprint ]
 Abstract :
In this paper we pick up an old challenge to design public key or whitebox constructions from symmetric cipher components. We design several encryption schemes based on the ASASA structure ranging from fast and generic symmetric ciphers to compact public key and whitebox constructions based on generic affine transformations combined with specially designed low degree nonlinear layers. While explaining our design process we show several instructive attacks on the weaker variants of our schemes.

Provable Second Preimage Resistance Revisited
(SAC'13)
Charles Bouillaguet and Bastien Vayssière, August 2013 hide
 slides : [ PDF ]
 paper (full version) : [ Springer ][ PDF ]
 Abstract :
Most cryptographic hash functions are iterated constructions, in which a mode of operation specifies how a compression function or a fixed permutation is applied. The MerkleDamgård mode of operation is the simplest and more widely deployed mode of operation, yet it suffers from generic second preimage attacks, even when the compression function is ideal.
In this paper we focus on provable security against second preimage attacks. Based on the study of several existing constructions, we describe simple properties of modes of operation and show that they are sufficient to allow some form of provable security, first in the random oracle model and then in the standard model. Our security proofs are extremely simple. We show for instance that the claims of the designers of Haifa regarding second preimage resistance are valid.
Lastly, we give arguments that proofs of second preimage resistance by a blackbox reduction incur an unavoidable security loss
.

Fast Exhaustive Search for Quadratic Systems in GF(2) on FPGAs
(SAC'13)
Charles Bouillaguet, ChenMou Cheng, Tung Chou, Ruben Niederhagen and BoYin Yang, August 2013 hide
 paper (full version) : [ eprint ]
 Abstract :
In 2010, Bouillaguet et al. proposed an efficient solver for polynomial systems over 𝔽2 that trades memory for speed.
As a result, 48 quadratic equations in 48 variables can be solved on a graphics processing unit (GPU) in 21 min. The research question that we would like to answer in this paper is how specifically designed hardware performs on this task. We approach the answer by solving multivariate quadratic systems on reconfigurable hardware, namely FieldProgrammable Gate Arrays (FPGAs). We show that, although the algorithm proposed in [BCC+10] has a better asymptotic time complexity than traditional enumeration algorithms, it does not have a better asymptotic complexity in terms of silicon area. Nevertheless, our FPGA implementation consumes 20–25 times less energy than its GPU counterpart. This is a significant improvement, not to mention that the monetary cost per unit of computational power for FPGAs is generally much cheaper than that of GPUs.

GraphTheoretic Algorithms for the Isomorphism of Polynomials Problem
(Eurocrypt'13)
Charles Bouillaguet, PierreAlain Fouque, Amandine Véber, May 2013 hide
 paper (full version) : [ PDF ] [ eprint ]
 Abstract :
We give three new algorithms to solve the ``isomorphism of polynomial'' problem, which was underlying the hardness of recovering the secretkey in some multivariate trapdoor oneway functions. In this problem, the adversary is given two quadratic functions, with the promise that they are equal up to linear changes of coordinates. Her objective is to compute these changes of coordinates, a task which is known to be harder than GraphIsomorphism. Our new algorithm build on previous work in a novel way. Exploiting the birthday paradox, we break instances of the problem in time $q^{2n/3}$ (rigorously) and $q^{n/2}$ (heuristically), where $q^n$ is the time needed to invert the quadratic trapdoor function by exhaustive search. These results are obtained by turning the algebraic problem into a combinatorial one, namely that of recovering partial information on an isomorphism between two exponentially large graphs. These graphs, derived from the quadratic functions, are new tools in multivariate cryptanalysis.

Practical Keyrecovery For All Possible Parameters of SFLASH
(Asiacrypt'11)
Charles Bouillaguet, PierreAlain Fouque, and Gilles MacarioRat May 2011 hide
 paper : [ PDF ]
 MAGMA code of the attack : here.
 Abstract :
In this paper we present a new practical keyrecovery attack on the SFLASH signature scheme. SFLASH is a derivative of the older C* encryption and signature scheme that was broken in 1995 by Patarin. In SFLASH, the public key is truncated, and this simple countermeasure prevents Patarin's attack. The scheme is wellknown for having been considered secure and selected in 2004 by the NESSIE project of the European Union to be standardized. However, SFLASH was practically broken in 2007 by Dubois, Fouque, Stern and Shamir. Their attack breaks the original (and most relevant) parameters, but does not apply when more than half of the public key is truncated. It is therefore possible to choose parameters such that SFLASH is not broken by the existing attacks, although it is less efficient. We show a keyrecovery attack that breaks the full range of parameters in practice, as soon as the informationtheoretically required amount of information is available from the publickey. The attack uses new cryptanalytic tools, most notably pencils of matrices and quadratic forms.

Automatic Search of Attacks on roundreduced AES and Applications
(Crypto'11)
Charles Bouillaguet, Patrick Derbez and PierreAlain Fouque, August 2011 hide
 paper : [ PDF ] (long version currently in preparation)
 C code of some attack, and of the tool used to find them : here.
 Abstract :
In this paper, we describe versatile and powerful algorithms for searching guessanddetermine and meetinthemiddle attacks on byteoriented symmetric primitives. To demonstrate the strengh of these tool, we show that they allows to automatically discover new attacks on roundreduced AES with very low data complexity, and to find improved attacks on the AESbased MACs AlphaMAC and PelicanMAC, and also on the AESbased stream cipher LEX. Finally, the tools can be used in the context of fault attacks. These algorithms exploit the algebraically simple byteoriented structure of the AES. When the attack found by the tool are practical, they have been implemented and validated.

New Insights on Impossible Differential Cryptanalysis (SAC'11)
Charles Bouillaguet, Orr Dunkelman, PierreAlain Fouque and Gaëtan Leurent, August 2011 hide
 paper : [ PDF ]
 Abstract :
Since its introduction, impossible differential cryptanalysis has been applied to many ciphers. Besides the specific application of the technique in various instances, there are some very basic results which apply to generic structures of ciphers, e.g., the well known 5round impossible differential of Feistel ciphers with bijective round functions. In this paper we present a new approach for the construction and the usage of impossible differentials for Generalized Feistel structures. The results allow to extend some of the previous impossible differentials by one round (or more), answer an open problem about the ability to perform this kind of analysis, and tackle, for the first time the case of nonbijective round functions.

Low Data Complexity Attacks on AES (IEEE Tr. on Inf. Th.)
Charles Bouillaguet, Patrick Derbez, Orr Dunkelman, Nathan Keller, and PierreAlain Fouque, December 2010 hide
 paper : [ PDF ] [ eprint ] [ Journal ].
 The C code of some of the (practical) attacks is available here.
 Abstract :
The majority of current attacks on reducedround variants of block ciphers seeks to maximize the number of rounds that can be broken, using less data than the entire codebook and less time than exhaustive key search. In this paper, we pursue a different approach, restricting the data available to the adversary to a few plaintext/ciphertext pairs. We show that consideration of such attacks (which received little atten tion in recent years) serves an important role in assessing the security of block ciphers and of other cryptographic primitives based on block ci phers. In particular, we show that these attacks can be leveraged to more complex attacks, either on the block cipher itself or on other primitives (e.g., stream ciphers, MACs, or hash functions) that use a small number of rounds of the block cipher as one of their components. As a case study, we consider the AES — the most widely used block cipher, whose round function is used in various cryptographic primitives. We present attacks on up to four rounds of AES that require at most 10 known/chosen plaintexts. We then apply these attacks to cryptanalyze a variant of the stream cipher LEX, and to mount a new known plaintext attack on 6round AES.

Practical Cryptanalysis of the Identification Scheme Based on the Isomorphism of Polynomial With One Secret Problem (PKC'11)
Charles Bouillaguet, JeanCharles Faugère, PierreAlain Fouque and Ludovic Perret, May 2010 hide
 paper : [ PDF ]
 Available on the eprint archive (report 2010/504).
 MAGMA code of the algorithms : quadratic and cubic cases.
 Abstract :
This paper presents a practical cryptanalysis of the Identification Scheme proposed by Patarin at Crypto 1996. This scheme relies on the hardness of the Isomorphism of Polynomial with One Secret (IP1S), and enjoys shorter key than many other schemes based on the hardness of a combinatorial problem (as opposed to numbertheoretic problems). Patarin proposed concrete parameters that have not been broken faster than exhaustive search so far. On the theoretical side, IP1S has been shown to be harder than Graph Isomorphism, which makes it an interesting target. We present two new deterministic algorithms to attack the IP1S problem, and we rigorously analyze their complexity and success probability. We show that they can solve a (big) constant fraction of all the instances of degree two in polynomial time. We verified that our algorithms are very efficient in practice. All the parameters with degree two proposed by Patarin are now broken in a few seconds. The parameters with degree three can be broken in less than a CPUmonth. The identification scheme is thus quite badly broken.

Fast Exhaustive Search for Polynomial Systems in F_2
(CHES'10)
Charles Bouillaguet, HsiehChung Chen, ChenMou Cheng, Tung Chou, Ruben Niederhagen, Adi Shamir, and BoYin Yang hide
 paper (long version) : [ PDF ]
 Full version available on the eprint archive (report 2010/313).
 Abstract :
We analyze how fast we can solve general systems of multivariate equations of various low degrees over GF_2 ; this is a well known hard problem which is important both in itself and as part of many types of algebraic cryptanalysis. Compared to the standard exhaustive search technique, our improved approach is more efficient both asymptotically and practically. We implemented several optimized versions of our techniques on CPUs and GPUs. Our technique runs more than 10 times faster on modern graphic cards than on the most powerful CPU available. Today, we can solve 48+ quadratic equations in 48 binary variables on a 500dollar NVIDIA GTX 295 graphics card in 21 minutes. With this level of performance, solving systems of equations supposed to ensure a security level of 64 bits turns out to be feasible in practice with a modest budget. This is a clear demonstration of the computational power of GPUs in solving many types of combinatorial and cryptanalytic problems.

Security Analysis of SIMD
(SAC'10)
Charles Bouillaguet, Gaëtan Keurent and PierreAlain Fouque, August 2010 hide
 paper : [ PDF ]
 Full version available on the eprint archive (report 2010/323).
 Abstract :
In this paper we study the security of the SHA3 candidate SIMD. We first show a new freestart distinguisher based on symmetry relations. It allows to distinguish the compression function of SIMD from a random function with a single evaluation. However, we also show that this property is very hard to exploit to mount any attack on the hash function because of the mode of operation of the compression function. Essentially, if one can build a pair of symmetric states, the symmetry property can only be triggered once. In the second part, we show that a class of freestart distinguishers is not a threat to the widepipe hash functions. In particular, this means that our distinguisher has a minimal impact on the security of the hash function, and we still have a security proof for the SIMD hash function. Intuitively, the reason why this distinguisher does not weaken the function is that getting into a symmetric state is about as hard as finding a preimage. Finally, in the third part we study differential path in SIMD, and give an upper bound on the probability of related key differential paths. Our bound is in the order of 2^{n/2} using very weak assumptions. Resistance to related key attacks is often overlooked, but it is very important for hash function designs.

Attacks on Hash Functions based on Generalized Feistel, Application to ReducedRound Lesamnta and SHAvite3/512
(SAC'10)
Charles Bouillaguet, Orr Dunkelman, Gaëtan Keurent and PierreAlain Fouque, August 2010 hide
 paper : [ PDF ]
 Abstract :
In this paper we study the strength of two hash functions which are based on Generalized Feistels. We describe a new kind of attack based on a cancellation property in the round function. This new technique allows to efficiently use the degrees of freedom available to attack a hash function. Using the cancellation property, we can avoid the nonlinear parts of the round function, at the expense of some freedom degrees. Our attacks are mostly independent of the round function in use, and can be applied to similar hash functions which share the same structure but have different round functions. We start with a 22round generic attack on the structure of Lesamnta, and adapt it to the actual round function to attack 24round Lesamnta (the full function has 32 rounds). We follow with an attack on 9round SHAvite3/512 which also works for the tweaked version of SHAvite3/512.

Another Look at Complementation Properties
(FSE'10)
Charles Bouillaguet, Orr Dunkelman, Gaëtan Leurent and PierreAlain Fouque, February 2010 hide
 paper : [ PDF ]
 Abstract :
In this paper we present a collection of attacks based on generalisations of the complementation property of DES. We find symmetry relations in the key schedule and in the actual rounds, and we use these symmetries to build distinguishers for any number of rounds when the relation is deterministic. This can be seen as a generalisation of the complementation property of DES or of slide/relatedkey attacks, using different kinds of relations. We further explore these properties, and show that if the relations have easily found fixed points, a new kind of attacks can be applied.
Our main result is a selfsimilarity property on the Sha3 candidate Lesamnta, which gives a very surprising result on its compression function. Despite the use of round constants which were designed to thwart any such attack, we show a distinguisher on the full compression function which needs only one query, and works for any number of rounds. We also show how to use this selfsimilarity property to find collisions on the full compression function of Lesamnta much faster than generic attacks. The main reason for this is the structure found in these round constants, which introduce an interesting and unexpected symmetry relation. This casts some doubt on the use of highly structured constants, as it is the case in many designs, including the AES and several Sha3 candidates.
Our second main contribution is a new relatedkey differential attack on roundreduced versions of the XTEA blockcipher. We exploit the weakness of the keyschedule to suggest an iterative relatedkey differential. It can be used to recover the secret key faster than exhaustive search using two related keys on 37 rounds. We then isolate a big class of weak keys for which we can attack 51 rounds out of the cipher's 64 rounds.
We also apply our techniques to ESSENCE and PURE.

A Family of Weak Keys in HFE and the Corresponding Practical KeyRecovery
(Journal of Mathematical Cryptology,2009)
Charles Bouillaguet, PierreAlain Fouque, Antoine Joux and Joana Treger, June 2010 hide
 paper : [ PDF ]
 Available on the eprint, or on the site of the Journal
 Abstract :
The HFE (Hidden Field Equations) cryptosystem is one of the most interesting publickey multivariate scheme. It has been proposed more than 10 years ago by Patarin and seems to withstand the attacks that break many other multivariate schemes, since only subexponential ones have been proposed. The public key is a system of quadratic equations in many variables. These equations are generated from the composition of the secret elements: two linear mappings and a polynomial of small degree over an extension field. In this paper we show that there exist weak keys in HFE when the coefficients of the internal polynomial are defined in the ground field. In this case, we reduce the secret key recovery problem to an instance of the Isomorphism of Polynomials (IP) problem between the equations of the public key and themselves. Even though for schemes such as SFLASH or C^* the hardness of keyrecovery relies on the hardness of the IP problem, this is normally not the case for HFE, since the internal polynomial is kept secret. However, when a weak key is used, we show how to recover all the components of the secret key in practical time, given a solution to an instance of the IP problem. This breaks in particular a variant of HFE proposed by Patarin to reduce the size of the public key and called the ``subfield variant''.

Herding, Second Preimage and Trojan Message Attacks Beyond MerkleDamgaard
(SAC'09)
Elena Andreeva and Charles Bouillaguet and Orr Dunkelman and John Kelsey, July 2009 hide
 Available on the Springer's website
 paper : [ PDF ]
 Abstract :
In this paper we present new attack techniques to analyze the structure of hash functions that are not based on the classical MerkleDamgaard construction. We extend the herding attack to concatenated hashes, and to certain hash functions that process each message block several times. Using this technique, we show a second preimage attack on the folklore ``hashtwice'' construction which process two concatenated copies of the message. We follow with showing how to apply the herding attack to tree hashes. Finally, we present a new type of attack  the trojan message attack, which allows for producing second preimages of unknown messages (from a small known space) when they are appended with a fixed suffix.

Analysis of the Collision Resistance of RadioGatún using
Algebraic Techniques (SAC'08)
Charles Bouillaguet and PierreAlain Fouque, June 2008 hide
 paper : [ PS, PDF ]
 Abstract :
In this paper, we present some preliminary results on the security of the RadioGatún hash function. RadioGatún has an internal state of 58 words, and is parameterized by the word size, from one to 64 bits. We study the onebit version of RadioGatún since according to the authors, attacks on this version also affect the reasonablysized versions. On this toy version, we revisit the claims of the designers and first improve some results. Secondly, given a differential path, we show how to find a message pairs colliding more efficiently than the strategy proposed by the authors using algebraic techniques. We experimented this strategy on the onebit version since we can efficiently find differential path by brute force. Even though the complexity of this collision attack is higher than the general security claim on RadioGatún[1], it is still less than the birthday paradox on the size of the internal state.

Second Preimage Attacks on Dithered Hash Functions (submitted + EUCROCRYPT'08)
Elena Andreeva, Charles Bouillaguet, PierreAlain Fouque, Jonathan Hoch, John Kelsey, Adi Shamir and Sebastien Zimmer, April 2008 hide
 A longer version [ PDF ] has been submitted to a journal
 Accepted in EUROCRYPT'08 [ PS, PDF ]
 Available on the ePrint and on Springer's website
 Abstract :
In this work we present new generic second preimage attacks on hash functions. Our first attack is based on the herding attack, and applies to various MerkleDamgårdbased iterative hash functions. Compared to the previously known longmessage second preimage attacks, our attack adds only a small computational overhead. In exchange, our attack gives the adversary a much greater control over the contents of the second message and in particular allows all the difference to be concentrated in a few message blocks. As a result, the new second preimage attack is applicable to hash function constructions such as the dithered hash proposal of Rivest, Shoup's UOWHF, and the ROX hash construction, which were thought to be immune to the earlier known second preimage attacks. We also suggest a few timememorydata tradeoff variants for this type of attacks, allowing for faster online computations, and attacking significantly shorter messages. Furthermore, we analyze the properties of the dithering sequence used in Rivest's hash function proposal, and develop a timememory tradeoff which allows us to apply our second preimage attack to a much stronger than those in Rivest's proposals. Parts of our results rely on the kite generator, a new timememory tradeoff tool. We also exhibit a timememorydata tradeoff attack on tree hashes for second preimages. Finally, we show how both the existing second preimage attacks and our new attacks can be applied even more effiently when given multiple short target messages rather than a single long target message.
 A longer version [ PDF ] has been submitted to a journal

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
 Master's thesis : [ PS, PDF ]

Using FirstOrder 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 resolutionbased 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 higherorder logic to firstorder logic that enables the application of resolutionbased 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 runtime errors such as null dereferences or array out of bounds accesses.