Formal Verification of Probing Security via Conditional Independence

Computer Science > Logic in Computer Science [Submitted on 22 May 2026] Formal Verification of Probing Security via Conditional Independence 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. Subjects: Logic in Computer Science (cs.LO); Cryptography and Security (cs.CR) Cite as: arXiv:2605.23316 [cs.LO]   (or arXiv:2605.23316v1 [cs.LO] for this version)   https://doi.org/10.48550/arXiv.2605.23316 Focus to learn more Submission history From: Satoshi Kura [view email] [v1] Fri, 22 May 2026 07:34:38 UTC (118 KB) Access Paper: HTML (experimental) view license Current browse context: cs.LO < prev   |   next > new | recent | 2026-05 Change to browse by: cs cs.CR References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)