MSc Thesis Defense: Kağan Gülsüm, VERIFICATION OF PROBING SECURITY FOR MASKED CIRCUITS: A CONSTRUCTIVE APPROACH AND THEORETICAL STUDY, Date & Time: 21 July, 2026 – 3:30 PM, Place: FENS L062

VERIFICATION OF PROBING SECURITY FOR MASKED CIRCUITS: A CONSTRUCTIVE APPROACH AND THEORETICAL STUDY

Kağan Gülsüm
Computer Science and Engineering, MSc Thesis, 2026

Thesis Jury

     Asst. Prof. Süha Orhun Mutluergil (Thesis Advisor)

  Prof. Erkay Savaş

  Asst. Prof. Klaus Freiherr von Gleissenthal

Date & Time: July 21st, 2026 – 3:30 PM

Place: FENS L062

Keywords : masking, probing security, formal verification, side-channel analysis, coupling

Abstract

Masking defends cryptographic hardware and software implementations against side-channel attacks by splitting each secret into randomised shares. The probing model of Ishai, Sahai, and Wagner reduces the security of a masked circuit to a combinatorial question: is every set of $d$ wires, called a probe, jointly independent of the secrets? This thesis studies the exact verification of that property, namely $d$-probing security, for masked arithmetic circuits over the two-element field. We first identify the computational complexity of the problem. Computing the distribution of a single probe is \#P-complete, and the corresponding security decision problem is complete for the exact-counting class C$_=$P, so verifying even a single probe sits above the polynomial hierarchy. Hence, we verify constructively and present Coppula, a $d$-probing security checker implemented in Lean 4 featuring a layered design. At its core is a rewrite engine acting as a probe oracle, which uses substitutions and a multiplicative factoring step to expose and isolate masks buried inside products. It operates alongside a subset-space traversal that avoids explicit enumeration of every $d$-subset by partitioning the space via a set-level Vandermonde identity. Ultimately, a successful discharge is interpreted as a measure-preserving coupling of the randomness space, extending the security guarantee of one certified probe to a larger safe set of wires. The checker is sound but necessarily incomplete; we formally prove its guarantees and evaluate it on masked gadgets, notably verifiying a family of cicruits where comparable tools fail.