[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!

Best,
Friedrich


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
>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/f339d28b/attachment.htm>


More information about the Verifpal mailing list