------------------------SDT2 B' GSM----------------------------------------------------ObjectName----------------------------------------ObjectType----------------------------------------!%&()LinkEndpoints--------------------------------1------------------------------------------------- (˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙GSM------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------˙˙˙˙11-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------˙˙˙˙()[8(!x package GSM /* SDL MODEL OVERVIEW ----------------- This model represents a simplified GSM network. WHAT HAS BEEN MODELED --------------------- - user PIN code verification, - mobile IMEI checking in the EIR database (prevents using a stolen mobile), - user authentication: the AUC sends a random number to the mobile, who encrypts it and sends it back to the AUC who checks the result. - when a mobile moves from one cell to another, the HLR and VLR databases are updated. - when a mobile is called, the routing information is given by the HLR and VLR databases. - during simulation, any mobile can move to any cell. Remark: 'init' signals have been used because for the moment the SDL context parameters are not supported in the SDL simulator. WHAT HAS NOT BEEN MODELED ------------------------ - low-level protocols (physical, link, network etc. layers), - connection to the switched or ISDN telephone network, - the numerous logical channels used between a mobile phone and the base stations: Traffic CHannel, Synchronization CHannel, Broadcast Control CHannel, Standalone Dedicated Control CHannel, Access Grant CHannel, Random Access CHannel, Pagina CHannel, - supplementary services, - power management on the mobile phone, - speech and data encryption, - SIM card creation and unlocking, - called ringer heared in the caller phone. */ /* GLOSSARY -------- - AuthentC enter (AUC): AUthentication Center. - BaseStationCtlr (BSC): Base Station Controller.ter. - BaseTxStation (BTS): Base Transceiver Station. - EquipIdRegister (EIR): Equipment Identity Register. - GSM: Global System for Mobile communi cations. - HomeLocRegister (HLR): Home Location Register. - IMEI: International Mobile Equipment Identity. - MobileSwitchCtr (MSC): Mobile Switching Center. - PIN: Personnal Identification Number. - VisitLocRegister (VLR): Vis itor Location Register. BIBLIOGRAPHY ------------ Le radiotelephone cellulaire GSM, J.Tisal, Masson, Paris, 1995. */)]}): AUthentication Center. - BaseStationCtlr (BSC): Base Station Controller.ter. - BaseTxStation (BTS):Ž˙˙˙˙ Base Transceiver Station. - EquipIdRegister (EIR): Equipment Identity Register. - GSM: Global System for Mobile communications. - HomeLocRegister (HLR): Home Location Register. - IMEI: International Mobile Equipment Identity.  - MobileSwitchCtr (MSC): Mobile Switching Center. - PIN: Personnal Identification Number. - VisitLocRegister (VLR): Visitor Location Register. BIBLIOGRAPHY ------------ Le radiotelephone cellulaire GSM, J.Tisal, Masson, Paris, 1995. */ /* CIF End Text */ /* CIF CurrentPage 2 */ /* CIF TEXT (34, 74), (1097, 1788) */ /* CIF Keep Specific Geode TextMode 4 */ /* CIF Keep Specific Geode Modified */ /* PIN user code: */)]}------------------------------------------------------ĘB()[()[h()[k()[n()]][Bq()][ t()][9w()[8(!V newtype PIN_t literals unknown, pin_a, pin_b, pin_c, pin_d; endnewtype; /* Mobile Switch ID: */ newtype MSC_ID_t literals Paris, Lyon; endnewtype; /* Base Station Controller ID: */ newtype BSC_ID_t literals Paris1, Lyon1; endnewtype; /* Base Transceiver Station ID: */ newtype BTS_ID_t literals Paris11, Paris12, Lyon11, Lyon12; endnewtype; /* Mobile users ID: */ newtype Mobile_ID_t  literals Nobody, Marie, John, pizza, parispizza, lyonpizza; endnewtype; /* Mobile phone identity: */ newtype IMEI_t literals IMEI1, IMEI2, IMEI3, IMEI4; endnewtype; /* Call rejection reason: */ newtype reason_t literals ok, not_allowed, invalid_ph_nr, abnormal; endnewtype; /* call failure reason */ newtype called_state_t literals called_ok, called_busy, called_unreachable; endnewtype; newtype billing_storage struct called Mobile_ID_t; duration NATURAL; price REAL; endnewtype; syntype indice = NATURAL default 0 constants 0 : 15 endsyntype; newtype billing_report_elt ARRAY( indice, billing_storage); endnewtype; newtype billing_report_t struct nb_com indice; bil billing_report_elt; endnewtype; /* CIF End Text */ /* CIF TEXT (1158, 69), (1741, 1775) */ /* CIF Keep Specific Geode TextMode 4 */ /* CIF Keep Specific Geode Modified */ signal initMSC(MSC_ID_t), initBSC(BSC_ID_t), initBTS(BTS_ID_t), initMS(BTS_ID_t, Mobile_ID_t, IMEI_t); /* init signals to replace by context parameters when available in the tool: */ signal answer_call, askReport, authentResp(BOOLEAN), badPIN, BTSchanging(BTS_ID_t), BTSresp(BOOLEAN, BTS_ID_t), busy, call_conf(called_state_t /* status */, Mobile_ID_t /* called */, BTS_ID_t) /* to a mobile */, call_ind(Mobile_ID_t, Mobile_ID_t /* called */, BTS_ID_t) /* to a mobile */, call_reject(reason_t, Mobile_ID_t, BTS_ID_T) /* to a mobile */, call_req(Mobile_ID_t /* calling */, Mobile_ID_t) /* called *//* from a mobile */, call_resp(called_state_t /* status */, Mobile_ID_t /* calling */, Mobile_ID_t) /* called *//* from a mobile */, checkIMEI(IMEI_t), com_start(Mobile_ID_t), com_finish(Mobile_ID_t, Mobile_id_t), convers, dialing(Mobile_ID_t), disable,  encryptedNr(NATURAL), endUpdHLR, endUpdVLR, getBTS(Mobile_ID_t), getPhoneNumber(Mobile_ID_t), getMSC(Mobile_ID_t), getReport(Mobile_ID_t), giveReport(billing_report_t, Mobile_ID_t, BTS_ID_t), DBgiveReport(billing_report_t, Mobile_ID_t), IMEI_OK(BOOLEAN), initGUI(Mobile_ID_t), initSCM(BSC_ID_t), initSM(MSC_ID_t), logOn(Mobile_ID_t, BTS_ID_t, IMEI_t), mobileLocation(MSC_ID_t, BTS_ID_t, reason_t), MSCresp(BOOLEAN, MSC_ID_t), offKey, on_hook, onKey, PIN(PIN_t), randomNr(NATURAL), rejected, report(Mobile_ID_t /* caller */, NATURAL) /* time */, ring, searchMobile(Mobile_ID_t), sendShortcut(Mobile_ID_t), startAuthent, unlock, unreachable, updateHLR(Mobile_ID_t, MSC_ID_t, BOOLEAN), updateVLR(Mobile_ID_t, BTS_ID_t); /* CIF End Text */ /* CIF CurrentPage 3 */ /* CIF TEXT (1324, 59), (1203, 2115) */ /* CIF Keep Specific Geode TextMode 4 */ /* CIF Keep Specific Geode Modified */ /* alphabetical order: */ signallist keys = answer_call, askReport, BTSchanging, dialing, offKey, on_hook, onKey, PIN; signallist MSCtoAUC = encryptedNr, startAuthent; signallist MSCtoBilling = com_start, com_finish, getReport; signallist MSCtoBC = call_conf, call_ind, call_reject, giveReport, initBSC, randomNr; signallist MSCtoDB = checkIMEI, com_start, com_finish, encryptedNr, getMSC, getReport, startAuthent, updateHLR; signallist MSCtoEIR = checkIMEI; signallist MSCtoHLR = getMSC, updateHLR; signallist MSCtoVLR = getBTS, updateVLR; signallist MStoMS = BTSresp, call_conf, call_ind, getBTS, giveReport; signallist MtoB = encryptedNr, call_req, call_resp, com_start, com_finish, getReport, logOn; signallist VLRtoMSC = BTSresp, endUpdVLR, getBTS; /* CIF End Text */ /* CIF TEXT (37, 49), (1256, 2110) */ /* CIF Keep Specific Geode TextMode 4 */ /* CIF Keep Specific Geode Modified */ /* Alphabetical order. */ signallist AUCtoMSC = authentResp, randomNr; signallist BCtoBTS = call_conf, call_ind, call_reject, giveReport, initBTS, randomNr; signallist BCtoMSC = encryptedNr, call_re q, call_resp, com_start, com_finish, getReport, logOn; signallist BtoM = call_conf, call_ind, call_reject, giveReport, initMS, randomNr; signallist BTStoBC = encryptedNr, call_req, call_resp, com_start, com_finish, getReport, logOn, randomNr; signal!list DBtoMSC = authentResp, initMSC, IMEI_OK, endUpdHLR, DBgiveReport, MSCresp, randomNr; signallist DBtoMSCtrl = authentResp, initMSC, IMEI_OK, endUpdHLR, DBgiveReport, randomNr; signallist displ = badPIN, disable, initGUI, rejected, ring, unlock, c"onvers, busy, unreachable, giveReport; signallist EIRtoMSC = initMSC, IMEI_OK; signallist HLRtoMSC = endUpdHLR, MSCresp; /* CIF End Text */ /* CIF CurrentPage 1 */ /* CIF BlockType (907, 87), (257, 152) */ /* CIF Keep Specific Geode TextMode 4 */ /* C#IF Keep Specific Geode Modified */ /* CIF Page DefaultPartition (2970, 2100) */ /* CIF Frame (32, 150), (2453, 1336) */ /* CIF Keep Specific Geode TextMode 0 */ /* CIF Keep Specific Geode Modified */ )]][=z()[(! DataBases)]][=}$()[(! MobileSwitchCtr)]][=€()[(! BaseStationCtlr)]][=ƒ()[(! BaseTxStation)]][=†()[(! MobileStation)]]]]}------------------------------------------------------------------ž˙˙˙˙(!4Œ!5!7)[!(! DefinitionPage! )]}------------------------------------------------------------------------------------------------------------------------------------------------------------------------------R˙˙˙˙!%()PageOrder-------------------------------------1-------------------------------------------------DefinitionPage--------------------------------------------------------------------------------------- ----%)----˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙˙----˙˙˙˙!%()HeadingText-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ------------------------&------------˙˙˙˙()[w(!GSDL)]}-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------˙˙˙˙()[(! Ě! 22!(d)[h(! 6––!  ç)[k(! 6ŻŻ)[n(! 6Żz ! )]][Bq(! 6Ż! )][ t(! 6ÖŻ)][9w*(! 6žČ! !S)[8(!š newtype PIN_t literals unknown, pin_a, pin_b, pin_c, pin_d; endnewtype; /* Mobile Switch ID: */ newtype MSC_ID_t literals Paris, Lyon; endnewtype; /* Base Station Controller ID: */ newtype BSC+_ID_t literals Paris1, Lyon1; endnewtype; /* Base Transceiver Station ID: */ newtype BTS_ID_t literals Paris11, Paris12, Lyon11, Lyon12; endnewtype; /* Mobile users ID: */ newtype Mobile_ID_t literals Nobody, Marie, John, pizza, parispizza, lyonpiz,za; endnewtype; /* Mobile phone identity: */ newtype IMEI_t literals IMEI1, IMEI2, IMEI3, IMEI4; endnewtype; /* Call rejection reason: */ newtype reason_t literals ok, not_allowed, invalid_ph_nr, abnormal; endnewtype; /* call failure reason */ newty-pe called_state_t literals called_ok, called_busy, called_unreachable; endnewtype; newtype billing_storage struct called Mobile_ID_t; duration NATURAL; price REAL; endnewtype; syntype indice = NATURAL default 0 constants 0 : 15 endsyntype.; newtype billing_report_elt ARRAY( indice, billing_storage); endnewtype; newtype billing_report_t struct nb_com indice; bil billing_report_elt; endnewtype; signal initMSC(MSC_ID_t), initBSC(BSC_ID_t), initBTS(BTS_ID_t), initMS(BTS_ID_t,/ Mobile_ID_t, IMEI_t); signal answer_call, askReport, authentResp(BOOLEAN), badPIN, BTSchanging(BTS_ID_t), BTSresp(BOOLEAN, BTS_ID_t), BTSreply(BOOLEAN, BTS_ID_t), busy, call_conf(called_state_t /* status */, Mobile_ID_t /* 0called */, BTS_ID_t) /* to a mobile */, call_confirm(called_state_t /* status */, Mobile_ID_t /* called */, BTS_ID_t) /* to a mobile */, call_ind(Mobile_ID_t, Mobile_ID_t /* called */, BTS1_ID_t) /* to a mobile */, call_inquire(Mobile_ID_t, Mobile_ID_t /* called */, BTS_ID_t) /* to a mobile */, call_reject(reason_t, Mobile_ID_t, BTS_ID_T) /* to a mobile */, call_req(Mobile_ID_t /* c2alling */, Mobile_ID_t, /* called *//* from a mobile */ BTS_ID_t /* Proxy addition */), call_resp(called_state_t /* status */, Mobile_ID_t /* calling */, Mobile_ID_t, /* called *//* from a mobile */ 3 BTS_ID_t), /* Proxy addition */ checkIMEI(IMEI_t), com_start(Mobile_ID_t, BTS_ID_t), /* Proxy addition */ com_finish(Mobile_ID_t, Mobile_id_t, BTS_ID_t), /* Proxy addition */ convers, dialing(Mobile_ID4_t), disable, encryptedNr(NATURAL, BTS_ID_t /* Proxy addition */), endUpdHLR, endUpdVLR, getBTS(Mobile_ID_t), fetchBTS(Mobile_ID_t), getPhoneNumber(Mobile_ID_t), getMSC(Mobile_ID_t), getReport(Mobile_ID_t, BTS_I5D_t), /* Proxy addition */ giveReport(billing_report_t, Mobile_ID_t, BTS_ID_t), returnReport(billing_report_t, Mobile_ID_t, BTS_ID_t), DBgiveReport(billing_report_t, Mobile_ID_t), IMEI_OK(BOOLEAN), initGUI(Mobile_ID_t), initSCM(BSC_ID_t), ini6tSM(MSC_ID_t), logOn(Mobile_ID_t, BTS_ID_t, IMEI_t), mobileLocation(MSC_ID_t, BTS_ID_t, reason_t, PID), MSCresp(BOOLEAN, MSC_ID_t), offKey, on_hook, onKey, PIN(PIN_t), randomNr(NATURAL, Mobile_ID_t), /* Proxy ad7dition */ rejected, report(Mobile_ID_t /* caller */, NATURAL) /* time */, ring, searchMobile(Mobile_ID_t), sendShortcut(Mobile_ID_t), startAuthent, unlock, unreachable, updateHLR(Mobile_ID_t, MSC_ID_t, BOOLEAN), updateVLR(Mobile_ID_t, B8TS_ID_t); signallist keys = answer_call, askReport, BTSchanging, dialing, offKey, on_hook, onKey, PIN; signallist MSCtoAUC = encryptedNr, startAuthent; signallist MSCtoBilling = com_start, com_finish, getReport; signallist MSCtoBC = call_conf, call_in9d, call_reject, giveReport, initBSC, randomNr; signallist MSCtoDB = checkIMEI, com_start, com_finish, encryptedNr, getMSC, getReport, startAuthent, updateHLR; signallist MSCtoEIR = checkIMEI; signallist MSCtoHLR = getMSC, updateHLR; signallist MSCtoVL:R = fetchBTS, updateVLR; /* signallist MSCtoVLR = getBTS, updateVLR; */ /* signallist MStoMS = BTSresp, call_conf, call_ind, getBTS, giveReport; */ signallist MStoMS = BTSresp, call_confirm, call_inquire, getBTS, returnReport; signallist MtoB = encrypted;Nr, call_req, call_resp, com_start, com_finish, getReport, logOn; signallist VLRtoMSC = BTSreply, endUpdVLR; /* signallist VLRtoMSC = BTSresp, endUpdVLR, getBTS; */ signallist AUCtoMSC = authentResp, randomNr; signallist BCtoBTS = call_conf, call_ind, crt, randomNr; signallist displ = badPIN, disable, initGUI, rejected, ring, unlock, convers, busy, unreachable, giveReport; signallist EIRtoMSC = initMSC, IMEI_OK; signallist HLRtoMSC = endUpdHLR, MSCresp; )]][=z(! 6€ ,! ,Č!?S)[(! 6™ w! DataBases)]][=}(! 6€ &! wČ!S)[(! 6™ q! MobileSwitchCtr)]][=€(! 6€ ! ^Č!S)[(! 6™ k! BaseStationCtlr)]@][=ƒ(! 6€ ! EČ!S)[(! 6™ e! BaseTxStation)]][=†(! 6€ ! EČ!S)[(! 6™ _! MobileStation)]][=Œ(! 6€ ! ,Č!S)[A(! 6™ Y! MSBTSProxy)]]]]}6€ ! ,Č!S)[(! 6™ Y! MSBTSProxy)]]]]}roxy)]]]]}]]]]}[(! 6™ _! MobileStation)]][=Œ(! 6€ ! ,Č!S)[(!-˙˙˙˙ 6™ Y! MSBTSProxy)]]]]}! 6™ Y! MSBTSProxy)]]]]} 6€ ! ,Č!S)[(! 6™ Y! MSBTSProxy)]]]]}----------------------------------------------------------------------------------------------%˙˙˙˙