Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proverif translation error #3

Open
cym13 opened this issue Nov 9, 2023 · 0 comments
Open

Proverif translation error #3

cym13 opened this issue Nov 9, 2023 · 0 comments

Comments

@cym13
Copy link

cym13 commented Nov 9, 2023

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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

No branches or pull requests

1 participant