[Verifpal] gxyz

Pittsburgh penguins Tv anderswnilson at gmail.com
Mon Jun 29 16:58:58 CEST 2020


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
]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200629/cd0a6584/attachment.htm>


More information about the Verifpal mailing list