[Verifpal] Handling of constant messages in protocols
nadim at symbolic.software
Wed Jun 24 13:12:00 CEST 2020
Thank you for identifying this interesting discussion point.
The issue with allowing principals to receive constants they already know is that we would then need to determine what happens in that case.
Imagine Alice sends “hello” to Bob, but that the message is modified by the attacker along the way. There are two options as to how we could handle this:
- Bob drops the “hello” value they know in favor of the one that is received (overwriting it with the received “hello" value)
- Bob keeps the “hello” they know and disregards the received “hello” value in the event that it differs from the one they know.
Neither of these two options seems to me more legitimate or intuitive than the other, which is exactly why I opted to disallow Verifpal models where principals receive values they are supposed to already know.
Indeed, in this event it seems to me that having “knows private hello” and then sending it is no big deal and clearer than having to compromise by choosing one of the two above proposed behaviors for Bob.
I am happy to hear thoughts and feedback.
Symbolic Software • https://symbolic.software
> On 23 Jun 2020, at 2:24 PM, Renaud Lifchitz via Verifpal <verifpal at lists.symbolic.software> wrote:
> As discussed yesterday night on the Discord channel, there is currently no easy way to model a fixed message in an exchange (for example the "HELLO" message to initiate a handshake) :
> - The "knows public HELLO" statement followed by HELLO transmission throws an error in current Verfpal "Verifpal! Error: Device is receiving constant (HELLO) despite already knowing it.", which prevents any further analysis of the whole protocol
> - The only workaround I've found so far is to use "knows private HELLO" and send HELLO, which is obviously not private...
> I suggest current Verifpal error be converted into a warning to allow this useful and frequent kind of use.
> Best regards,
> Renaud Lifchitz
> Verifpal mailing list
> Verifpal at lists.symbolic.software
More information about the Verifpal