[Verifpal] Nonce reuse in Verifpal models

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


Loup,

> 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
attacker[active]

principal I[
   knows private p1
   knows private zero

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

queries[
   confidentiality? H1
]
// file end 

(mike)


More information about the Verifpal mailing list