[Verifpal] Incrementing a constant

Friedrich Wiemer friedrich.wiemer at rub.de
Thu Feb 27 12:39:54 CET 2020

Thanks for the quick answer and explanation!
I'll try this approach.

Sadly I cannot attend EC but would be very interested in the verifpal event! Thanks again for your superb work!


On February 27, 2020 11:13:16 AM GMT+01:00, 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
>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
>effect as IncrementNonce(Nonce) or Nonce + 1. So what you can do in
>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
>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
>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
>> > 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/f339d28b/attachment.htm>

More information about the Verifpal mailing list