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

Adds Verifpal model (formal verification) #30

Open
wants to merge 4 commits into
base: master
from

Conversation

@nocko
Copy link

nocko commented Dec 30, 2019

I also moved the Proverif report out to a new formal-verification directory.

Formal verification is interesting. Verifpal's specification is pleasantly intuitive, so I modeled salt-channel.

Here's an example of the output:

$ verifpal verify salt-channel.vp 
Verifpal 0.7.8 (go1.13.5) — https://verifpal.com
WARNING: Verifpal is experimental software.

 Verifpal! parsing model "salt-channel.vp"...
 Verifpal! verification initiated at 15:04:32
 Analysis! Client has sent m1 to Server, rendering it public
 Analysis! Server has sent m2 to Client, rendering it public
 Analysis! Server has sent m3a to Client, rendering it public
 Analysis! Server has sent m3b to Client, rendering it public
 Analysis! Client has sent m4a to Server, rendering it public
 Analysis! Client has sent m4b to Server, rendering it public
 Analysis! Client has sent req to Server, rendering it public
 Analysis! Server has sent resp to Client, rendering it public
     Info! attacker is configured as active
Deduction! G^ec resolves to G^ec
Deduction! G^es resolves to G^es (analysis 0, depth 1)
Deduction! m3a resolves to AEAD_ENC(G^ec^es, G^s, c0) (analysis 0, depth 2)
Deduction! m3b resolves to AEAD_ENC(G^ec^es, SIGN(s, HASH(G^ec, G^es)), c0) (analysis 0, depth 3)
 Analysis! HASH(G^ec, G^es) now conceivable by reconstructing with G^ec, G^es (analysis 0, depth 4)
Deduction! m4a resolves to AEAD_ENC(G^es^ec, G^c, c0) (analysis 0, depth 5)
Deduction! m4b resolves to AEAD_ENC(G^es^ec, SIGN(c, HASH(G^ec, G^es)), c0) (analysis 0, depth 6)
Deduction! req resolves to AEAD_ENC(G^es^ec, pt1, c0) (analysis 0, depth 7)
Deduction! resp resolves to AEAD_ENC(G^ec^es, pt2, c0) (analysis 0, depth 8)
Deduction! G^nil resolves to G^nil (analysis 3, depth 0)
Deduction! G^nil^es found by attacker by reconstructing with nil, G^es (analysis 3, depth 4)
 Analysis! G^s now conceivable by deconstructing AEAD_ENC(G^nil^es, G^s, c0) with G^nil^es (analysis 3, depth 5)
Deduction! AEAD_ENC(G^nil^es, G^s, c0) found by attacker by reconstructing with G^nil^es (analysis 3, depth 5)
 Analysis! SIGN(s, HASH(G^nil, G^es)) now conceivable by deconstructing AEAD_ENC(G^nil^es, SIGN(s, HASH(G^nil, G^es)), c0) with G^nil^es (analysis 3, depth 6)
 Analysis! HASH(G^nil, G^es) now conceivable by reconstructing with G^nil, G^es (analysis 3, depth 6)
Deduction! AEAD_ENC(G^nil^es, SIGN(s, HASH(G^nil, G^es)), c0) found by attacker by reconstructing with G^nil^es (analysis 3, depth 6)
Deduction! G^nil resolves to G^nil (analysis 9, depth 1)
Deduction! G^nil^ec found by attacker by reconstructing with nil, G^ec (analysis 9, depth 4)
Deduction! AEAD_DEC(G^nil^ec, AEAD_ENC(G^ec^es, G^s, c0), c0)? found by attacker by reconstructing with G^nil^ec (analysis 9, depth 5)
Deduction! req resolves to AEAD_ENC(nil, nil, nil) (analysis 15, depth 7)
Deduction! G^nil resolves to G^nil (analysis 24, depth 0)
Deduction! G^nil^es found by attacker by reconstructing with nil, G^es (analysis 24, depth 4)
 Analysis! G^s now conceivable by deconstructing AEAD_ENC(G^nil^es, G^s, c0) with G^nil^es (analysis 24, depth 5)
Deduction! AEAD_ENC(G^nil^es, G^s, c0) found by attacker by reconstructing with G^nil^es (analysis 24, depth 5)
 Analysis! SIGN(s, HASH(G^nil, G^es)) now conceivable by deconstructing AEAD_ENC(G^nil^es, SIGN(s, HASH(G^nil, G^es)), c0) with G^nil^es (analysis 24, depth 6)
 Analysis! HASH(G^nil, G^es) now conceivable by reconstructing with G^nil, G^es (analysis 24, depth 6)
Deduction! AEAD_ENC(G^nil^es, SIGN(s, HASH(G^nil, G^es)), c0) found by attacker by reconstructing with G^nil^es (analysis 24, depth 6)
Deduction! resp resolves to AEAD_ENC(nil, nil, nil) (analysis 44, depth 8)
Deduction! G^nil resolves to G^nil (analysis 53, depth 1)
Deduction! G^nil^ec found by attacker by reconstructing with nil, G^ec (analysis 53, depth 4)
Deduction! AEAD_DEC(G^nil^ec, AEAD_ENC(G^ec^es, G^s, c0), c0)? found by attacker by reconstructing with G^nil^ec (analysis 53, depth 5)
Deduction! AEAD_DEC(G^nil^ec, AEAD_ENC(nil, nil, nil), c0)? found by attacker by reconstructing with G^nil^ec (analysis 66, depth 3)
Deduction! req resolves to AEAD_ENC(nil, nil, nil) (analysis 73, depth 7)
Deduction! G^nil resolves to G^nil (analysis 82, depth 0)
Deduction! G^nil^es found by attacker by reconstructing with nil, G^es (analysis 82, depth 4)
 Analysis! G^s now conceivable by deconstructing AEAD_ENC(G^nil^es, G^s, c0) with G^nil^es (analysis 82, depth 5)
Deduction! AEAD_ENC(G^nil^es, G^s, c0) found by attacker by reconstructing with G^nil^es (analysis 82, depth 5)
 Analysis! SIGN(s, HASH(G^nil, G^es)) now conceivable by deconstructing AEAD_ENC(G^nil^es, SIGN(s, HASH(G^nil, G^es)), c0) with G^nil^es (analysis 82, depth 6)
 Analysis! HASH(G^nil, G^es) now conceivable by reconstructing with G^nil, G^es (analysis 82, depth 6)
Deduction! AEAD_ENC(G^nil^es, SIGN(s, HASH(G^nil, G^es)), c0) found by attacker by reconstructing with G^nil^es (analysis 82, depth 6)
Deduction! resp resolves to AEAD_ENC(nil, nil, nil) (analysis 102, depth 8)
Deduction! G^nil resolves to G^nil (analysis 111, depth 1)
Deduction! G^nil^ec found by attacker by reconstructing with nil, G^ec (analysis 111, depth 4)
Deduction! AEAD_DEC(G^nil^ec, AEAD_ENC(G^ec^es, G^s, c0), c0)? found by attacker by reconstructing with G^nil^ec (analysis 111, depth 5)
Deduction! AEAD_DEC(G^nil^ec, AEAD_ENC(nil, nil, nil), c0)? found by attacker by reconstructing with G^nil^ec (analysis 124, depth 3)
 Stage 3, Analysis 128...
 Verifpal! verification completed at 15:04:33
 Verifpal! thank you for using verifpal!
     Info! verifpal is experimental software and may miss attacks.
`

It would be neat to have the Proverif model added to the repo for comparison / examination.

@nocko

This comment has been minimized.

Copy link
Author

nocko commented Dec 30, 2019

I've also modeled the WTP certificate exchange used in the Alure2/Poseidon BLE protocol. This doesn't belong in this repo. I put it here

nocko added 2 commits Dec 30, 2019
…dels to match Proverif report

The ServerSigKey on ServerAuth and FullAuth are a bit of a hack. Verifpal doesn't
support multiple assignment, aliasing or anything that would allow a principal to
send the same information twice. That's what ServerSigKey is sending the public key
that we *already* got via pre-auth. By hashing the sig in M1's ServerSigKey, we can
model the function.

Could be revisited if Verifpal gains the ability in the future.
@nocko

This comment has been minimized.

Copy link
Author

nocko commented Dec 31, 2019

I added commits to improve the model added two models. There are now three models that should correspond to the three models tested in the Proverif report:

SaltChannel.pv: this is the naïve protocol run in which providing ServerSigKey is optional.

SaltChannelServerAuth.pv: here, providing ServerSigKey is not only mandatory, but the server is
pre-authenticated to the client out of band.

SaltChannelFullAuth.pv: the strongest model, in which both the server and the client are
mutually pre-authenticated out of band before the session commences.

I named the Verifpal files to match (notice vp suffix vs. pv suffix).

If you're interested in committing these changes, I'll squash them down to a single commit.

@sijohans

This comment has been minimized.

Copy link
Contributor

sijohans commented Jan 8, 2020

This looks really interesting. I have no idea how to interpret the input, but looking into the tool now. Tried running SaltChannelFullAuth.vp on my computer, but it seems to take very long time (didn't complete during the night). Does it take this long for you as well?

@sijohans

This comment has been minimized.

Copy link
Contributor

sijohans commented Jan 9, 2020

Also noted that the link to the proverif report in the readme file is not updated after moving the report.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

None yet

2 participants
You can’t perform that action at this time.