Dear Anders,

Could you please be more specific? I would ask you to write a paragraph explaining what you’re trying to accomplish, what these two CONCAT operations are supposed to represent/accomplish, and what your expected behavior is. As it stands, I don’t understand what the issue you’re encountering is or what it is that requires a “workaround.” So please, be more specific so that I can help you.

Thank you,

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

> On 30 Mar 2020, at 6:45 PM, Pittsburgh penguins Tv via Verifpal <verifpal@lists.symbolic.software> wrote:
>
> Dear Nadim,
> which is the preferred workaround for the CONCAT used below?
>
> Best regards
> Anders N.
>
> // C.P. Schnorr: Efficient Signature Generation by Smart Cards, Journal of Cryptology 4 (1991) 161–174.
> //    a × exp(Pa,Nb)           
> // =  exp(g,Na) × exp(exp(g,Sa),Nb)           
> // =  exp(g,Na) × exp(g,Sa × Nb)               
> // =  exp(g,Na + Sa × Nb)             
> // =  exp(g, r)
>
> attacker[active]
>
> principal Alice[
>     knows private a
>     generates na
>     ga = G^a
>     gna = G^na
> ]
>
> principal Bob[
>     generates nb
> ]
>
> Alice -> Bob: ga, gna
> Bob -> Alice: nb
>
> principal Alice[
>     gnb = G^nb
>     gnba = gnb^a                                  // G^(nb*a)
>     gr = CONCAT(gna, gnba)               // G^na*G^(nb*a)
> ]
>
> Alice -> Bob: gr
>
> principal Bob[
>     ganb = ga^nb                                 // G^(a*nb)
>     gnaganb = CONCAT(gna,ganb)    // G^na*G^(a*nb)
>     _ = ASSERT(gr, gnaganb)?
> ]
>
> queries[
>     authentication? Alice -> Bob: gr
> ]
>
> _______________________________________________
> Verifpal mailing list
> Verifpal@lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal