Formal Verification of Probing Security via Conditional Independence
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911715205054464 |
|---|---|
| author | Kura, Satoshi Takashima, Katsuyuki |
| author_facet | Kura, Satoshi Takashima, Katsuyuki |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_23316 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Formal Verification of Probing Security via Conditional Independence Kura, Satoshi Takashima, Katsuyuki Logic in Computer Science Cryptography and Security 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. |
| title | Formal Verification of Probing Security via Conditional Independence |
| topic | Logic in Computer Science Cryptography and Security |
| url | https://arxiv.org/abs/2605.23316 |