const pk: Function; secret sk: Function; inversekeys (pk,sk); protocol nsl7(I,R) { role R { var ni; const nr; read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); read_3(I,R, {nr}pk(R) ); claim(I,nr,ni); } } const Alice,Bob; run nsl3.R(Alice,Bob); run nsl3.R(Alice,Bob);