Closed nocko closed 4 years ago
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
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.
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?
Also noted that the link to the proverif report in the readme file is not updated after moving the report.
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:
It would be neat to have the Proverif model added to the repo for comparison / examination.