[Verifpal] gxyz

Nadim Kobeissi nadim at symbolic.software
Sun Jul 12 23:26:00 CEST 2020


Dear Anders,

Yes, as noted in Verifpal and the Verifpal User Manual, this is something that is not currently supported. It may be supported in the future.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On 29 Jun 2020, at 4:58 PM, Pittsburgh penguins Tv via Verifpal <verifpal at lists.symbolic.software> wrote:
> 
> Dear Nadim,
> some protocols might need the '^' operator applied several times for an expression. The manual doesn't state any limitation on how many times the operator can be applied. Is there any reason, such as performance, why it currently can't be used several times?
> Note that the model below is only to exemplify.
> 
> Best regards
> Anders N.
> 
> 
> // https://verifpal.com/res/pdf/manual.pdf, 
> // page 31:
> // 'equations can be built on top of other equations 
> // (as in the case of gxy and gyx)'
> 
> attacker[active]
> 
> principal Server[ 
>     generates x 
>     generates y
>     generates z // added
> 
>     gx = G^x 
>     gy = G^y 
> 
>     gxy = gx^y 
>     gyx = gy^x 
> 
>     gxyz = gxy^z // invalid model?
> ]
> 
> queries [
>     freshness? gyx
> ]
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal



More information about the Verifpal mailing list