verifpal icon indicating copy to clipboard operation
verifpal copied to clipboard

Proverif translation error

Open cym13 opened this issue 1 year ago • 0 comments

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.

cym13 avatar Nov 09 '23 11:11 cym13