Code d'authentification de messagethumb|upright=1.8|Schéma de principe d'un code d'authentification de message Un code d'authentification de message (CAM), souvent désigné par son sigle anglais MAC (de message authentication code) est un code accompagnant des données dans le but d'assurer l'intégrité de ces dernières, en permettant de vérifier qu'elles n'ont subi aucune modification, après une transmission par exemple. Le concept est relativement semblable aux fonctions de hachage. Il s’agit ici aussi d’algorithmes qui créent un petit bloc authentificateur de taille fixe.
Cryptographie asymétriquevignette|320x320px|Schéma du chiffrement asymétrique: une clé sert à chiffrer et une seconde à déchiffrer La cryptographie asymétrique, ou cryptographie à clé publique est un domaine relativement récent de la cryptographie. Elle permet d'assurer la confidentialité d'une communication, ou d'authentifier les participants, sans que cela repose sur une donnée secrète partagée entre ceux-ci, contrairement à la cryptographie symétrique qui nécessite ce secret partagé préalable.
Vérification formelleIn the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.
Attaque par analyse du traficDans le domaine du renseignement et de la sécurité informatique, l'attaque par analyse du trafic désigne les méthodes permettant de tirer des informations de flux de communication de tout type (émissions radio, trafic internet, mais également courrier papier, rencontres entre agents...) sans nécessairement avoir accès au contenu des messages échangés (notamment lorsque les messages sont chiffrés. Ce type d'attaque peut être considéré comme une attaque par canal auxiliaire.
Hypothèse des marchés financiers efficientsL’hypothèse des marchés financiers efficients est une hypothèse utilisée en économie selon laquelle les marchés financiers sont efficients, c'est-à-dire que les prix des actifs reflètent toute l'information disponible au sujet du prix. Si les marchés sont efficients, alors il est impossible de faire mieux que le marché. Les marchés financiers ont fait l'objet d'études académiques visant à déterminer leur caractère efficient ou non.
Program analysisIn computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program optimization and program correctness. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what it is supposed to do.
SHA-3Keccak (prononciation: , comme “ketchak”) est une fonction de hachage cryptographique conçue par Guido Bertoni, Joan Daemen, Michaël Peeters et Gilles Van Assche à partir de la fonction RadioGatún. SHA-3 est issu de la NIST hash function competition qui a élu l'algorithme Keccak le . Elle n’est pas destinée à remplacer SHA-2, qui n’a à l'heure actuelle pas été compromise par une attaque significative, mais à fournir une autre solution à la suite des possibilités d'attaques contre les standards MD5, SHA-0 et SHA-1.
NIST hash function competitionThe NIST hash function competition was an open competition held by the US National Institute of Standards and Technology (NIST) to develop a new hash function called SHA-3 to complement the older SHA-1 and SHA-2. The competition was formally announced in the Federal Register on November 2, 2007. "NIST is initiating an effort to develop one or more additional hash algorithms through a public competition, similar to the development process for the Advanced Encryption Standard (AES).
Isabelle (logiciel)The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring yet supporting explicit proof objects. Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods.
Fonction pseudo-aléatoireUne fonction pseudo-aléatoire (ou PRF pour pseudorandom function) est une fonction dont l'ensemble des sorties possibles n'est pas efficacement distinguable des sorties d'une fonction aléatoire. Il ne faut pas confondre cette notion avec celle de générateur de nombres pseudo-aléatoires (PRNG). Une fonction qui est un PRNG garantit seulement qu'une de ses sorties prise seule semble aléatoire si son entrée a été choisie aléatoirement. En revanche, une fonction pseudo-aléatoire garantit cela pour toutes ses sorties, indépendamment de la méthode de choix de l'entrée.
