该论文研究了数字签名方案在标准不可伪造性之外的安全性质，包括恶意生成密钥下的安全性、消息知晓性（要求签名者知晓被签名的消息）以及不可重签名性（防止将现有签名重新用于不同消息）。作者首先回顾并梳理了这些性质之间的关系，并首次给出了不可重签名性的正式定义。随后提出了一种高效且可证明安全的变换（BUFF变换），能够为任何给定签名方案赋予这些额外性质。论文特别关注了后量子签名方案：在NIST后量子密码标准化第三轮中的六个最终候选方案，作者深入分析了它们在不可伪造性之外的安全性。结果表明，许多候选方案尚未提供这些更强的保证，这意味着后量子签名方案的安全性并不严格强于经典方案，而是与之不可比较。论文展示了如何应用所提出的变换高效地解决这一问题，从而为标准化的后量子方案提供这些额外保证，降低误用风险。该研究对于密码学研究者、协议设计者以及后量子密码标准化具有重要参考价值。

本论文针对后量子密码（PQC）硬件实现中的掩码Barrett reduction的侧信道泄漏问题，提出首个通用且机器验证的基数界限——1-Bit Barrier。Barrett reduction是基于NTT的PQC实现（如ML-KEM、ML-DSA）的非线性核心，但现有组合框架（ISW、t-SNI、PINI、DOM）仅针对GF(2)上的布尔掩码，无法直接应用于素域上的算术掩码。作者基于此前系列工作（QANARY、partial-NTT-masking margins、代数基础、蝴蝶组合），填补了这一空白。核心贡献在于：1）证明对于任意模数q>0和移位s，Barrett内部导线映射f_x(m) = ((x + 2^s - m) mod 2^s) mod q的原像基数属于{0,1,2}，绝不超过2——这一性质被称为1-Bit Barrier，意味着每条内部导线最多泄露1比特的最小熵；实际泄漏通常更少，因为计数为0的情况（不可达输出值）使界更为保守。2）引入PF-PINI（素域PINI）概念，证明Barrett满足PF-PINI(2)，Cooley-Tukey蝶形运算满足PF-PINI(1)，并观察到在阶段间加入新鲜掩码时，组合管线的最大原像基数为max(k1, k2)，因此1-Bit Barrier可传播。3）在Lean 4（Mathlib）中完成了12条定理的机器验证，无一个“sorry”，结果对所有q>0通用。4）指出Adams Bridge因缺少阶段间新鲜掩码而违反PF-PINI组合，解释了此前发现漏洞的原因。该工作为NIST IR 8547推荐的形式化方法在PQC实现验证中提供了首个通用机器验证的基数界，并给出1比特泄漏的直观解释。适合侧信道分析、PQC硬件安全、形式化验证领域的研究者和工程师阅读。