ProVerif 2.05中XOR操作类型不匹配及位串比较错误求助

问题场景 #

使用ProVerif 2.05进行密码协议建模时，执行XOR位操作后尝试将结果与0比较触发事件，出现类型不匹配错误。

出错代码 #

let xor_result = XOR(XOR(XOR(Kn, r2), m), XOR(Hash(UID), PRNG(m))) in
if xor_result = 0 then  
    event ToServer();

错误提示 #

Error: Syntax error
Error: bitstring should be a function or a predicate.
Error: Function = expects two arguments of same type but is here given 2 arguments of types bitstring, nat.

解决方法 #

ProVerif中0是自然数类型，而XOR操作返回的是位串类型，两者类型不兼容，不能直接用=比较。需要使用位串类型的全0值替代：

• 先定义一个与你的协议中位串长度匹配的全0常量，比如密钥、随机数是128位的话，定义const zero: bitstring[128]；如果长度不固定，直接定义const zero: bitstring。
• 确保所有参与XOR的变量（Kn、r2、m等）都声明为bitstring类型，避免类型混合引发隐式转换问题。

修改后的代码示例：

const zero: bitstring[128]; // 根据实际场景指定位串长度
let xor_result = XOR(XOR(XOR(Kn, r2), m), XOR(Hash(UID), PRNG(m))) in
if xor_result = zero then  
    event ToServer();

内容的提问来源于stack exchange，提问作者kw33n