TLS 1.3 Tamarin Model

[Nik Stuckenbrock]

Hi,

I'm currently working on the formal verification of TLS 1.3 build in Tamarin I found on [GitHub](https://github.com/tls13tamarin/TLS13Tamarin).
After processing the files with `m4` and executing the proofs I received the following syntax/type mismatch error:

tamarin-prover: shapeTerm: the term (p_sg.3) does not have enough pairs.
Occured in fact: (ProtoFact Linear "F_State_C1" 31) with behavior [[=],[=],[=],[<],[=],[.],[=],[.],[=,=],[.],[.],[=],[.],[=],[=],[.],[.],[.],[.],[=],[=],[=],[=],[=],[=],[=],[.],[=],[=],[=]]
CallStack (from HasCallStack):
  error, called at src/Theory/Constraint/Solver/Simplify.hs:615:33 in tamarin-prover-theory-1.10.0-L6vcrIqDzilJv2Os1O8TEh:Theory.Constraint.Solver.Simplify

Removing the all assignments for `p_sg` removes the error but probably isn't the best solution.
Does anyone know how to fix this, or where the problem is coming from? I can't find the mismatch in the pairs.

Here is an excerpt of the theory.

rule recv_hello_retry_request:
let
    g1 = $g1
    g2 = $g2
    p_sg = <g1, g2>
    [...]

sg = p_sg

[...]
in
    [ F_State_C1(tid,C,S, p_res_psk,p_messages,p_nc,p_ns,p_g,p_sg,p_hrr,p_x,p_y,p_gx,p_gy,p_gxy,p_psk_ke_mode,p_psk_id,p_edi,p_es,p_hs,p_ms,p_cats,p_sats,p_hs_keyc,p_hs_keys,p_auth_status,p_ems,p_rms,p_cert_req ),
    [...]
 
Thanks in advance,
Nik