test_moissonnage_selune
type: Agent

Computer Aided Security for Cryptographic Primitives, Voting protocols, and Wireless Sensor Networks
type: Distribution
access URL: https://theses.hal.science/tel-00807568
format: HTML
issued: 2026-05-11T17:06:46.164833
modified: 2026-05-11T17:06:46.133450

Computer Aided Security for Cryptographic Primitives, Voting protocols, and Wireless Sensor Networks
type: Dataset
contact point: Organization
  fn: CCSD
keyword: habilitation-a-diriger-des-recherches
keyword: neigbourhood-discovery
keyword: computational-model
keyword: wireless-sensor-networks
keyword: concrete-security
keyword: homomorphic-encryption
keyword: encryption-modes
keyword: formal-verification
keyword: mac
keyword: symbolic-model
keyword: infoinfo-crcomputer-science-cscryptography-and-security-cscr
keyword: public-encryption-scheme
keyword: indpendent-intruders
keyword: electronic-voting-protocol
keyword: privacy
keyword: resilience
keyword: infoeu-reposemanticsother
keyword: routing-algorithms
keyword: infoinfo-iacomputer-science-cscomputer-aided-engineering
landing page: https://theses.hal.science/tel-00807568
description: Security is one of the main issues of modern computer science. Nowadays more and more people use a computer to perform sensitive operations like bank transfer, Internet shopping, tax payment or even to vote. Most of these users do not have any clue how the security is achieved, therefore they totally trust their applications. These applications often use cryptographic protocols which are notoriously error prone even for experts. For instance a flaw was found in the Needham-Schroeder protocol seventeen years after its publication. These errors come from several aspects: Proofs ofsecurity of cryptographic primitives can contain some flaws. Security properties are not well specified, making it difficult to formally prove them. Assumptions on the intruder's model might be too restrictive. In this habilitation thesis we propose formal methods for verifying security of these three layers. First, we build Hoare logics for proving the security of cryptographic schemes like public encryption, encryption modes, Message Authentication Codes (MACs). We also study electronic voting protocols and wireless sensor networks (WSNs). In each one of these areas we first analyze the required security properties in order to propose a formal model. Then we develop adequate techniques for their verification.
issued: 2026-05-11T17:06:46.161832
language: en
modified: 2026-05-11T17:06:46.161836