[Verifpal] Authenticating keys with a hash sent over a second channel

Nadim Kobeissi nadim at symbolic.software
Sun Jan 5 14:07:36 CET 2020

Dear Alexander,

Thank you for raising this point. After thinking about it for a while, I've
decided that the way that Verifpal treats "force ASSERT passes" (an
internal term I used to describe this scenario) is indeed misleading, and
have made some changes in Verifpal 0.8.4 (which I am about to publish) that
should render your proposed model valid. I think this is the better and
more intuitive way to model such scenarios.

Thanks again for your contributions,

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office

On Sun, Jan 5, 2020 at 11:42 AM Alexander Krotov via Verifpal
<verifpal at lists.symbolic.software> wrote:

> > It models Alice sending her public key over the network to Bob, while at
> > the same time showing a QR code of the key hash to him. Bob then
> > computes the same key and verifies that the key is valid.
> I am also not sure if there is a better way to model transmission over
> the QR code. Guarded values only prevent attacker from modifying the
> values, but with QR code an attacker also does not know the value of
> "AUTH". A workaround I can think of is to also create a known private
> symmetric key and use it only to encrypt the QR code.
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200105/cee2df90/attachment.htm>

More information about the Verifpal mailing list