Boolean functions are accepted to be cryptographically strong if they satisfy some common pre-determined criteria. It is expected that any design criteria should remain invariant under a large group of transformations due to the theory of similarity of secrecy systems proposed by Shannon. One of the most important design criteria for cryptographically strong Boolean functions is the nonlinearity criterion. Meier and Staffelbach studied nonlinearity preserving transformations, by considering the invertible transformations acting on the arguments of Boolean functions, namely the pre-transformations. In this thesis, first, the results obtained by Meier and Staffelbach are presented. Then, the invertible transformations acting on the truth tables of Boolean functions, namely the post-transformations, are studied in order to determine whether they keep the nonlinearity criterion invariant. The equivalent counterparts of Meier and Staffelbach&rsquo / s results are obtained in terms of the post-transformations. In addition, the existence of nonlinearity preserving post-transformations, which are not equivalent to pre-transformations, is proved. The necessary and sufficient conditions for an affine post-transformation to preserve nonlinearity are proposed and proved. Moreover, the sufficient conditions for an non-affine post-transformation to keep nonlinearity invariant are proposed. Furthermore, it is proved that the smart hill climbing method, which is introduced to improve nonlinearity of Boolean functions by Millan et. al., is equivalent to applying a post-transformation to a single Boolean function. Finally, the necessary and sufficient condition for an affine pre-transformation to preserve the strict avalanche criterion is proposed and proved.

A Boolean function can be represented in several different forms. These different representation have advantages and disadvantages of their own. The Algebraic Normal Form, truth table, and Walsh spectrum representations are widely studied in literature. In 1999, Claude Carlet and Phillippe Guillot introduced the Numerical Normal Form. NumericalNormal Form(NNF) of a Boolean function is similar to Algebraic Normal Form, with integer coefficients instead of coefficients from the two element field. Using NNF representation, just like the Walsh spectrum, characterization of several cryptographically important functions, such as resilient and bent functions, is possible. In 2002, Carlet had shown several divisibility results concerning resilient and correlation-immune functions using NNF. With these divisibility results, Carlet is able to give bounds concerning nonlinearity of resilient and correlation immune functions. In this thesis, following Carlet and Guillot, we introduce the Numerical Normal Form and derive the pairwise relations between the mentioned representations. Characterization of Boolean, resilient and bent functions using NNF is also given. We then review the divisibility results of Carlet, which will be linked to some results on the nonlinearity of resilient and correlation immune functions. We show the M&ouml / bius inversion properties of NNF of a Boolean function, using Gian-Carlo Rota&rsquo / s work as a guide. Finally, using a lot of the mentioned results, we prove a necessary condition on theWalsh spectrum of Boolean functions with given degree.

In cryptography especially in block cipher design, Boolean functions are the basic elements. A cryptographic function should have high nonlinearity as it can be attacked by linear attack. In this thesis the highest possible nonlinear boolean functions in the even dimension, that is bent functions, basic properties and construction methods of bent functions are studied. Also normal bent functions and generalized bent functions are presented.

In this thesis we study Boolean functions from three different perspectives. First, we study the complex- ity of Boolean minimization for several classes of formulas with polynomially solvable SAT, and formulate sufficient conditions for a class which cause the minimization problem to drop at least one level in the polyno- mial hierarchy. Second, we study a class of matched CNFs for which SAT is trivial but minimization remains Σp 2 complete. We prove that every matched CNF has at least one equivalent prime and irredundant CNF that is also matched. We use this fact to prove the main result of this part, namely that for every matched CNF all clause minimal equivalent CNFs are also matched. Third, we look at propagation completeness - the property of a CNF that says that for every partial assignment all entailed literals can be discovered by unit propagation. We can extend every CNF to be propagation complete by adding empowering impli- cates to it. The main result of this section is a the proof of coNP completeness of the recognition problem for propagation complete CNFs. We also show that there exist CNFs to which an exponential number of empowering implicates have to be added to make them propagation complete.

Orientador: Prof. Dr. Jair Donadelli Jr. / Dissertação (mestrado) - Universidade Federal do ABC, Programa de Pós-Graduação em Ciência da Computação, 2014.

Orientador: Prof. Dr. Ronaldo Cristiano Prati / Dissertação (mestrado) - Universidade Federal do ABC, Programa de Pós-Graduação em Ciência da Computação, 2014.

Dans cette thèse, nous nous intéressons à la résolution du problème de la satisfiabilité propositionnelle (SAT). Ce problème fondamental en théorie de la complexité est aujourd'hui utilisé dans de nombreux domaines comme la planification, la bio-informatique, la vérification de matériels et de logiciels. En dépit d'énormes progrès observés ces dernières années dans la résolution pratique du problème SAT, il existe encore une forte demande d'algorithmes efficaces pouvant permettre de résoudre les problèmes difficiles. C'est dans ce contexte que se situent les différentes contributions apportées par cette thèse. Ces contributions s'attellent principalement autour de deux composants clés des solveurs SAT : l'apprentissage de clauses et les heuristiques de choix de variables de branchement. Premièrement, nous proposons une méthode de résolution permettant d'exploiter les fonctions booléennes cachées généralement introduites lors de la phase d'encodage CNF pour réduire la taille des clauses apprises au cours de la recherche. Ensuite, nous proposons une approche de résolution basée sur le principe d'intensification qui indique les variables sur lesquelles le solveur devrait brancher prioritairement à chaque redémarrage. Ce principe permet ainsi au solveur de diriger la recherche sur la sous-formule booléenne la plus contraignante et de tirer profit du travail de recherche déjà accompli en évitant d'explorer le même sous-espace de recherche plusieurs fois. Dans une troisième contribution, nous proposons un nouveau schéma d'apprentissage de clauses qui permet de dériver une classe particulière de clauses Bi-Assertives et nous montrons que leur exploitation améliore significativement les performances des solveurs SAT CDCL issus de l'état de l'art. Finalement, nous nous sommes intéressés aux principales stratégies de gestion de la base de clauses apprises utilisées dans la littérature. En effet, partant de deux stratégies de réduction simples : élimination des clauses de manière aléatoire et celle utilisant la taille des clauses comme critère pour juger la qualité d'une clause apprise, et motiver par les résultats obtenus à partir de ces stratégies, nous proposons plusieurs nouvelles stratégies efficaces qui combinent le maintien de clauses courtes (de taille bornée par k), tout en supprimant aléatoirement les clauses de longueurs supérieures à k. Ces nouvelles stratégies nous permettent d'identifier les clauses les plus pertinentes pour le processus de recherche. / In this thesis, we focus on propositional satisfiability problem (SAT). This fundamental problem in complexity theory is now used in many application domains such as planning, bioinformatic, hardware and software verification. Despite enormous progress observed in recent years in practical SAT solving, there is still a strong demand of efficient algorithms that can help to solve hard problems. Our contributions fit in this context. We focus on improving two of the key components of SAT solvers: clause learning and variable ordering heuristics. First, we propose a resolution method that allows to exploit hidden Boolean functions generally introduced during the encoding phase CNF to reduce the size of clauses learned during the search. Then, we propose an resolution approach based on the intensification principle that circumscribe the variables on which the solver should branch in priority at each restart. This principle allows the solver to direct the search to the most constrained sub-formula and takes advantage of the previous search to avoid exploring the same part of the search space several times. In a third contribution, we propose a new clause learning scheme that allows to derive a particular Bi-Asserting clauses and we show that their exploitation significantly improves the performance of the state-of-the art CDCL SAT solvers. Finally, we were interested to the main learned clauses database reduction strategies used in the literature. Indeed, starting from two simple strategies : random and size-bounded reduction strategies, and motivated by the results obtained from these strategies, we proposed several new effective ones that combine maintaing short clauses (of size bounded by k), while deleting randomly clauses of size greater than k. Several other efficient variants are proposed. These new strategies allow us to identify the most important learned clauses for the search process.

Title: Boolean techniques in Knowledge representation Author: Miloš Chromý Department: Department of Theoretical Computer Science and Mathematical Logic Supervisor: Doc. RNDr. Ondřej Čepek, Ph.D., Department of Theoretical Com- puter Science and Mathematical Logic Abstract: In this thesis we will investigate switch-list representations of Boolean function and we will explore the biclique satisfiable formulas. Given a truth table representation of a Boolean function f the switch-list rep- resentation of f is a list of Boolean vectors from the truth table which have a different function value than the preceding Boolean vector in the truth table. We include this type of representation in the Knowledge Compilation Map [Dar- wiche and Marquis, 2002] and argue that switch-lists may in certain situations constitute a reasonable choice for a target language in knowledge compilation. First, we compare switch-list representations with a number of standard repre- sentations (such as CNF, DNF, and OBDD) with respect to their relative suc- cinctness. As a by-product of this analysis we also give a short proof of a long standing open question from [Darwiche and Marquis, 2002], namely the incom- parability of MODS (models) and PI (prime implicates) representations. Next, using the succinctness result between...

Dans cette thèse, nous étudions la sécurité de primitives cryptographiques. Ces systèmes sont fondés sur des transformations utilisant des objets mathématiques représentés de multiples manières. Nous utilisons alors certaines structures inhérentes à leurs composantes, et jusqu'alors non prises en compte, pour mettre en évidence de nouvelles vulnérabilités. Par l'exploitation de diverses représentations, nous avons ainsi cryptanalysé des chiffrements authentifiés de la compétition CAESAR, des chiffrements à flot spécifiques et des constructions génériques. Nous avons donné des critères de conception en vue de la standardisation par le NIST de chiffrements à bas coût. Dans le cas des chiffrements à flot, nous avons défini de nouveaux critères cryptographiques plus pertinents que les critères usuels. Plus précisément, nous analysons la sécurité des chiffrements par bloc légers au regard des récentes attaques par invariant, et nous montrons comment les éviter par un choix approprié de la couche linéaire de diffusion et des constantes de tour. Nous proposons une nouvelle cryptanalyse des registres filtrés, grâce à la décomposition des éléments dans les sous-groupes multiplicatifs du corps fini à 2^n éléments. L'analyse du chiffrement FLIP, mais aussi du générateur pseudo-aléatoire de Goldreich a mis en évidence des faiblesses exploitables dans des attaques de type ``supposer et déterminer'', qui nécessitent la prise en compte de nouveaux critères sur les fonctions booléennes utilisées dans ce contexte. Enfin, nous cryptanalysons une version simplifiée du chiffrement authentifié Ketje en utilisant plusieurs techniques, permettant ainsi d'affiner l'évaluation de sa sécurité. / In this thesis, we study the security of symmetric cryptographic primitives. These systems are based on transformations relying on mathematical objects that can be represented in multiple ways. We then exploit different induced structures to highlight new vulnerabilities. By exploiting various representations, we cryptanalyzed some schemes submitted to the CAESAR competition, and also some dedicated and generic stream ciphers. We exhibited design criteria for lightweight block ciphers in view of the NIST standardization process and in the case of stream ciphers we defined new cryptographic criteria more relevant than the usual ones. More precisely, we study the security of lightweight block ciphers with respect to the recent invariant attacks, and we show how to avoid them with an appropriate choice of the linear layer and the round constants. We propose a new cryptanalysis of the filtered registers, by decomposing elements in the multiplicative subgroups of the finite field with 2^n elements. The analysis of the FLIP cipher, but also of the Goldreich pseudo-random generator, revealed weaknesses that are exploitable in ``guess and determine'' attacks. This leads to new criteria on the Boolean functions used in this context. Finally, we cryptanalyze a weaker version of the authenticated encryption scheme Ketje using several techniques, in order to refine the security evaluation of this cipher.