[Verifpal] Incrementing a constant

Nadim Kobeissi nadim at symbolic.software
Thu Feb 27 11:13:16 CET 2020

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

More information about the Verifpal mailing list