本文针对密码系统侧信道攻击的掩码防御机制，提出了一种基于概率分离逻辑的形式化验证方法，用于自动验证掩码算法的非干扰性安全属性。作者首先建立了非干扰性与条件独立性之间的数学联系，从而将安全验证问题转化为条件独立性推理问题。随后，利用现有的Lilac分离逻辑框架（该框架专用于条件独立性推理）来执行验证，并设计了一系列新的证明规则，以支持探测安全性的高效验证。通过若干示例算法，论文展示了该方法能够有效验证典型掩码方案的安全性，同时相比传统手工证明或模型检验方法，降低了误判风险。该工作主要面向密码学实现者、安全验证工具开发者以及侧信道防御研究者，其核心贡献在于为掩码算法的形式化安全验证提供了更简洁、可自动化的理论框架。