symbolicsoft / verifpal Goto Github PK

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.

I'm trying out verifypal to prove some PAKE protocols, and I'm struggling with OPRF using passwords for blind salt, as in OPAQUE.

• I cannot find out how to invert a scalar (the blinding factor, as I want to compute HASH(pwd)^r^k^(1/r) )
• the verifier is unhappy because HASH(pwd)^r reveals the password. Ideally I want H2C(HASH(pwd))^r, I'm not sure how to communicate that to verifypal, but I guess that shouldn't reveal the password if r remains secret?

I want to prove the identity of one party through signing an arbitrary value provided by the other party.

Either:

• I do not know/have the appropriate query to express this verification, or
• the SIGN/SIGNVERIF pair of operations does not work with all available guarantees (i.e. n from both parties must be same if SIGNVERIF succeeds), or
• verification prematurely fails with conclusion that SIGN received malicious n

Furthermore, it isn't clear whether the query authentication? Bob -> Alice: n means "Alice is convinced that the n that Bob sent is authentic", or that it means "the n that Bob sent to Alice remains/arrived unchanged, i.e. is authentic". One takes a particular principal into the equation, while the other takes the perspective of the variable.

Goal: express/prove that n has remained unchanged as confirmed by Bob through signature verification? (Therefore, Bob knows that "Alice" is the Alice of the identity (sk, pk) and that she received the unchanged n.)

Clarification to the script below:

• assume sending [pk] was done some other time, in another way, some other channel. This is the way I know to model known information between parties.
• at the end of this sample, Bob has initiative. The sample is a (reduced) part of a larger protocol where Bob next needs to decide whether or not to continue.

attacker[active]
principal Alice[
	knows private sk
	pk = G^sk
]
Alice -> Bob: [pk]
principal Bob[
	generates n
]
Bob -> Alice: n
principal Alice[
	sig = SIGN(sk, n)
]
Alice -> Bob: sig
principal Bob[
	_ = SIGNVERIF(pk, n, sig)?
]

queries[
	confidentiality? sk
	authentication? Alice -> Bob: sig
	// The protocol detects when 'n' is not authentic, because Alice's signature will fail to verify against Bob's (original) 'n'.
	authentication? Bob -> Alice: n
]

See mailinglist conversation for more details and elaboration.