verifpal
verifpal copied to clipboard
Proverif translation error
Here's a full log demonstrating the issue and hopefully giving enough to reproduce it.
$ verifpal --version
verifpal version 0.27.2
$ cat chap.vp # available at https://verifhub.verifpal.com/10b484cb797eb532e64c8896eaa2d35b
attacker[active]
principal Initiator[
knows password secret
]
principal Authenticator[
knows password secret
generates challenge
]
Authenticator -> Initiator: challenge
principal Initiator[
response = HASH(secret, challenge)
]
Initiator -> Authenticator: response
principal Authenticator[
_ = ASSERT(HASH(secret, challenge), response)?
]
queries[
authentication? Initiator -> Authenticator: response
]
$ verifpal translate pv chap.vp > chap.pv
$ proverif --help
Proverif 2.04. Cryptographic protocol verifier, by Bruno Blanchet, Vincent Cheval, and Marc Sylvestre
[…]
$ proverif chap.pv
File "chap.pv", line 1, characters 5-24:
Warning: Setting expandIfTermsToTerms is deprecated.
File "chap.pv", line 121, characters 87-101:
Warning: identifier const_challenge rebound.
File "chap.pv", line 126, characters 39-53:
Warning: identifier const_challenge rebound.
File "chap.pv", line 148, characters 31-39:
Error: variable Authenticator_unnamed_0 is declared of type bitstring but should be of type bool.