[Verifpal] Incrementing a constant

Nadim Kobeissi nadim at symbolic.software
Thu Feb 27 11:15:03 CET 2020


Small correction: if you do end up using HASH, since it is a one-way
function you will also want to ensure that you use the `leak` keyword (or
send over the network) on all nonce values or at least the original nonce
value, to be sure that the attacker can obtain all of them.

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


On Thu, Feb 27, 2020 at 11:13 AM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> Dear Friedrich,
>
> In the symbolic model, incrementing constants would not occur
> computationally (i.e. with numeric values such as 1 or 2). If you were to
> model this in other software such as ProVerif, you'd define your own
> function called incrementNonce() which would map some input to some
> bijective output map.
>
> In effect, this means that in the symbolic model, HASH(Nonce) has the same
> effect as IncrementNonce(Nonce) or Nonce + 1. So what you can do in your
> model is use HASH(Nonce) as Nonce + 1, HASH(HASH(Nonce)) as Nonce + 2,
> etc., -- this should work fine and is an appropriate solution to what you
> are trying to achieve.
>
> Very good to hear from you, please do keep in touch if you have further
> questions or comments!
>
> As a reminder, there will be a Verifpal affiliated event at EUROCRYPT this
> year: https://verifpal.com/events/eurocrypt2020/
>
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> Sent from office
>
>
> On Thu, Feb 27, 2020 at 11:08 AM Friedrich Wiemer via Verifpal
> <verifpal at lists.symbolic.software> wrote:
>
>> Hi,
>>
>> does Verifpal support incrementing a constant, something like the following?
>>
>> > generates Nonce
>> > Nonce_b = Nonce + 1
>>
>> Best,
>> Friedrich
>>
>>
>> _______________________________________________
>> 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/20200227/4d9ccbe1/attachment.htm>


More information about the Verifpal mailing list