symbolicsoft / verifpal

Cryptographic protocol analysis for real-world protocols.
https://verifpal.com
GNU General Public License v3.0
41 stars 4 forks source link

Proverif translation error #3

Open cym13 opened 11 months ago

cym13 commented 11 months ago

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.