Analyse en ontwerp van cryptografische protocollen voor IoT-apparaten

The Internet of Things already counts into the tens of billions of devices, outnumbering people and spreading into every corner of daily life. Yet no single body owns the definition of ``IoT''. The Internet Engineering Task Force (IETF) frames it in terms of end-to-end connectivity between resource-constrained devices. The European Commission stresses economic and social impact. Industrial alliances focus on seamless interoperability. All these perspectives acknowledge the same hard facts: embedded processors have only a few kilobytes of memory, batteries must last for years, and user interfaces often shrink to a lone status LED, without any input/output ports for usual authentication or pairing. These limits sharpen an old tension between cryptographic rigour, ease of use and large-scale deployment. Heavy public-key arithmetic drains power. Manual key entry discourages adoption. Extra security chips increase cost and reduce openness. The central question of this thesis is therefore how to design and analyse protocols that respect all three pressures while relying only on hardware that manufacturers already ship. The design part of the work contributes a family of protocols that address different faces of the problem. First, an access-control architecture for implantable medical devices moves the vulnerable, ad-hoc setting towards a secure arrangement in which access control for the implant is outsourced to a companion smartphone (handset) that the patient already owns. The implant itself performs only a lightweight token check and one short-field Diffie-Hellman operation. A formal model in Verifpal and ProVerif proves authentication, forward secrecy and resistance to replay without relying on fresh randomness inside the implant. Second, a zero-interaction geofencing protocol, to help in IoT commissioning, constructs a fingerprint of a room from received-signal-strength (RSS) measurements. Using an autoencoder, the system verifies whether a live trace belongs to the learned geofence and, by binding a public key to the radio-channel geometry, grants or revokes access automatically when a user crosses the boundary. The scheme works with the Bluetooth and Wi-Fi radios already present in most access points and phones and needs no calibration, extra beacons or user actions. Third, a quorum-based location proof distributes a cryptographic secret across several heterogeneous sensors that happen to share the same room. Only when a defined subset of those sensors concur on co-presence can the secret be reconstructed and an authorisation token released. Together, these three designs demonstrate that modern public-key techniques and physical context can be combined to achieve strong guarantees while keeping interaction overhead close to zero. The final part of the thesis focuses on the security analysis of an industry standard that already appears in millions of smart-home products. A full symbolic model of its commissioning workflow is built in applied-$\pi$ calculus and checked with ProVerif. The proofs identify unwritten assumptions about salt freshness and identity binding that, if violated, break secrecy and authenticity. Laboratory tests on certified devices confirm that implementations deviate from the idealised model in exactly those places. The resulting attacks allow an intruder to hijack an onboarding session or to resume a stale session under weaker keys. A responsible-disclosure process coordinated with the standard body and major vendors has led to clarified specification text, patched software development kits and a global update campaign that reached a product range numbering in the many millions. The study shows that formal verification is not limited to academic protocols. When applied carefully, it can reveal subtle design gaps in commercial ecosystems before those gaps turn into large-scale breaches. The thesis thus provides a concrete foundation for building IoT systems that are secure, usable and readily deployable at a global scale.