[Verifpal] Nonce reuse in Verifpal models

Mike tankf33der at disroot.org
Wed Nov 25 14:36:25 CET 2020


> The second workaround uses ENC twice:
> H1 = ENC(H0, zero)
> K1 = ENC(H0, zero)
> But then I have another problem: in the real world, this would mean
> nonce reuse, and I'd have H1 == K1. So unless Verifpal considers
> different ENC calls to be independent as if they had different nonces,
> I may have problems with K1 and H1 not being independent from each
> other.
> So my questions are:
> - Does ENC() behaves as if it uses a different nonce each time?

This minimal model shows it use the same.

// file min.vp

principal I[
   knows private p1
   knows private zero

   H1 = ENC(p1, zero)
   K1 = ENC(p1, zero)
   _ = ASSERT(H1, K1)?

   confidentiality? H1
// file end 


More information about the Verifpal mailing list