Katsuyuki Takashima

Satoshi Kura, Katsuyuki Takashima

Side-channel attacks are a major threat to the security of cryptosystems. Masking is a widely used countermeasure against such attacks, but proving the security of masked algorithms is error-prone without formal verification. In this work, we propose a novel approach to formal verification of noninterference properties of masked algorithms based on probabilistic separation logic. By establishing a connection between noninterference and conditional independence, we show how noninterference can be verified using Lilac, a separation logic for conditional independence. We also provide several proof rules that facilitate the verification of probing security and demonstrate their application to example algorithms.

Tsuyoshi Miezaki, Yusaku Nishimura, Katsuyuki Takashima

To analyze the security of code-based cryptosystems, the smoothing parameter, which is closely related to the total variation distance of codes, has been investigated. While previous studies have bounded this distance using the Fourier transform on locally compact abelian groups, we take an alternative approach based on random walks. In this paper, we derive an inequality for the total variation distance of random walks using equitable partitions, and we show that our proposed bound generalizes existing results for finite abelian groups.

Toshiyuki Katsura, Katsuyuki Takashima

We advance previous studies on decomposed Richelot isogenies (Katsura--Takashima (ANTS 2020) and Katsura (ArXiv 2021)) which are useful for analysing superspecial Richelot isogeny graphs in cryptography. We first give a characterization of decomposed Richelot isogenies between Jacobian varieties of hyperelliptic curves of any genus. We then define generalized Howe curves, and present two theorems on their relationships with decomposed Richelot isogenies. We also give new examples including a non-hyperelliptic (resp.\,hyperelliptic) generalized Howe curve of genus 5 (resp.\,of genus 4).

Toshiyuki Katsura, Katsuyuki Takashima

Castryck, Decru, and Smith used superspecial genus-2 curves and their Richelot isogeny graph for basing genus-2 isogeny cryptography, and recently, Costello and Smith devised an improved isogeny path-finding algorithm in the genus-2 setting. In order to establish a firm ground for the cryptographic construction and analysis, we give a new characterization of {\em decomposed Richelot isogenies} in terms of {\em involutive reduced automorphisms} of genus-2 curves over a finite field, and explicitly count such decomposed (and non-decomposed) Richelot isogenies between {\em superspecial} principally polarized abelian surfaces. As a corollary, we give another algebraic geometric proof of Theorem 2 in the paper of Castryck et al.