(* public communication channel *) free c. (* constant values *) fun imsiReq/0. let ID_MS = in(c, req); if req = imsiReq then ( out(c, imsi)). let ID_SN = out(c, imsiReq); in(c, ximsi). let MS = (ID_MS). let SN = (ID_SN). process (! (new sk1; new imsi1; (! (new sk2; new imsi2; let sk = choice[sk1, sk2] in ( let imsi = choice[imsi1, imsi2] in ( (MS) | (SN)))))))