(* public communication channel *) free c. (* public identity of MS *) free imsi_wtn. (* 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 k; new imsi; (! ((MS) | (SN))))) | (new k; new id; let imsi = choice[id, imsi_wtn] in ( (! ((MS) | (SN)))))