symbolicsoft / verifpal Goto Github PK
View Code? Open in Web Editor NEWCryptographic protocol analysis for real-world protocols.
Home Page: https://verifpal.com
License: GNU General Public License v3.0
Cryptographic protocol analysis for real-world protocols.
Home Page: https://verifpal.com
License: GNU General Public License v3.0
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.
HASH(pwd)^r^k^(1/r)
)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:
SIGN
/SIGNVERIF
pair of operations does not work with all available guarantees (i.e. n
from both parties must be same if SIGNVERIF
succeeds), orSIGN
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:
[pk]
was done some other time, in another way, some other channel. This is the way I know to model known information between parties.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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.