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
]