(* GSM-R connection protocol *) (* Open communication channel *) free c. (* Private channel used to provide ids to RBCs and trains *) private free id. (* Support for relative time *) data inc/1. pred greater/2. clauses greater: inc(x),x; greater: x,y -> greater: inc(x),y. (* MAC function *) fun mac/2. (* Symmetric encryption *) fun encrypt/2. reduc decrypt(encrypt(x,k),k) = x. (* Generate the session key using Ra, Rb and Ks as parameters *) fun genSessionKey/3. (* Retrieve the symmetric key shared between an RBC and train *) private fun getKey/2. (* Message types from SUBSET-037 *) data AU1/0. data AU2/0. data AU3/0. data AR/0. data DT/0. (* Defininition for directions *) data DF_SEND/0. data DF_RESP/0. (* PDUs have SaF set to 0000 0001 for 'Single DES with modified MAC algorithm 3 *) data SAF/0. (* Zeros for use in the '000' flag either as an ETY or part of the standard... *) data ZEROS/0. (* Defining the ETCS ID types *) data TRAIN_ETCS_ID_TYPE/0. data RBC_ETCS_ID_TYPE/0. (* Use a static data value for the length *) data PAYLOAD_LENGTH/0. (* Add some generic messages, which can represent any valid set of ERTMS messages as per the specification to enable validation of deletion of messages *) data MESSAGE_1/0. data MESSAGE_2/0. data MESSAGE_3/0. private free SECRET. (* Check whether the long-term and session keys are kept secret *) query attacker:SECRET. (* Check authentication of the RBC to the train *) query evinj:trainFinishSession(rbc_id, train_id, train_nonce, saf, rbc_nonce, ks) ==> evinj:rbcStartSession(rbc_id, train_id, rbc_nonce, saf, train_nonce). (* Check authentication of the train to the RBC *) query evinj:rbcFinishSession(rbc_id, train_id, rbc_nonce, saf, train_nonce, ks) ==> evinj:trainStartSession(rbc_id, train_id, train_nonce, saf). (* Same check but allowing the session to use a different RBC ID and SaF *) query evinj:rbcFinishSession(rbc_id, train_id, rbc_nonce, saf, train_nonce, ks) ==> evinj:trainStartSession(rbc_id2, train_id, train_nonce, saf2). (* Check whether all messages can be received *) query ev:MessagesReceived3(m1, m2, m3). (* Check whether messages can be inserted by the attacker. If a message is accepted by the RBC is must have been sent by a train before. *) query ev:DataReceived1(m) ==> (ev:DataSent1(s2, m) | ev:DataSent2(s2, m) | ev:DataSent3(s2, m)). query ev:DataReceived2(m) ==> (ev:DataSent1(s2, m) | ev:DataSent2(s2, m) | ev:DataSent3(s2, m)). query ev:DataReceived3(m) ==> (ev:DataSent1(s2, m) | ev:DataSent2(s2, m) | ev:DataSent3(s2, m)). (* Check whether messages can be replayed by the attacker. Every message sent by a train should be accepted by a RBC at most once. *) query evinj:DataReceived1(m) ==> (evinj:DataSent1(s, m) | evinj:DataSent2(s, m) | evinj:DataSent3(s, m)). query evinj:DataReceived2(m) ==> (evinj:DataSent1(s, m) | evinj:DataSent2(s, m) | evinj:DataSent3(s, m)). query evinj:DataReceived3(m) ==> (evinj:DataSent1(s, m) | evinj:DataSent2(s, m) | evinj:DataSent3(s, m)). (* Check whether messages can be deleted *) query evinj:DataReceived1(m) ==> evinj:DataSent1(s, m). query evinj:DataReceived2(m) ==> evinj:DataSent2(s, m). query evinj:DataReceived3(m) ==> evinj:DataSent3(s, m). (* Check whether messages can be reordered. When messages are received, check if they are received in the same order as they were sent. *) query evinj:MessagesReceived2(m1, m2) ==> ((evinj:DataSent1(s, m1) & evinj:DataSent2(s, m2)) | (evinj:DataSent1(s, m1) & evinj:DataSent3(s, m2)) | (evinj:DataSent2(s, m1) & evinj:DataSent3(s, m2))). query evinj:MessagesReceived3(m1, m2, m3) ==> (evinj:DataSent1(s, m1) & evinj:DataSent2(s, m2) & evinj:DataSent3(s, m3)). let Train = new session; (* Receive an RBC id to communicate with *) in(id, rbc_etcs_id); (* T-CONN.request -- Au1 SaPDU *) new trainNonce; event trainStartSession(rbc_etcs_id, train_etcs_id, trainNonce, SAF); out(c, (TRAIN_ETCS_ID_TYPE, AU1, DF_SEND, train_etcs_id, SAF, trainNonce)); (* T-CONN.confirmation -- Au2 SaPDU *) in(c, (=RBC_ETCS_ID_TYPE, =AU2, =DF_RESP, in_rbc_etcs_id, rbcSaF, rbcNonce, inMAC)); (* Generate the session key *) let trainKS = genSessionKey(trainNonce, rbcNonce, getKey(in_rbc_etcs_id, train_etcs_id)) in (* Output encrypted secret to check secrecy of keys *) out(c, encrypt(SECRET, trainKS)); out(c, encrypt(SECRET, getKey(in_rbc_etcs_id, train_etcs_id))); if inMAC = mac(trainKS, ((PAYLOAD_LENGTH, train_etcs_id, RBC_ETCS_ID_TYPE, AU2, DF_RESP, in_rbc_etcs_id, rbcSaF), rbcNonce, trainNonce, train_etcs_id)) then (* T-DATA.request -- Au3 SaPDU *) event trainFinishSession(in_rbc_etcs_id, train_etcs_id, trainNonce, rbcSaF, rbcNonce, trainKS); out(c,(ZEROS, AU3, DF_SEND, mac(trainKS, (PAYLOAD_LENGTH, train_etcs_id, ZEROS, AU3, DF_SEND, trainNonce, rbcNonce)))); (* Send three messages from the train to the RBC *) new time; let msg1 = (DT, time, MESSAGE_1) in event DataSent1(session, msg1); out(c, msg1); let msg2 = (DT, inc(time), MESSAGE_2) in event DataSent2(session, msg2); out(c, msg2); let msg3 = (DT, inc(inc(time)), MESSAGE_3) in event DataSent3(session, msg3); out(c, msg3); 0. let RBC = (* Get an RBC identiy *) in(id, rbc_etcs_id); (* T-CONN.indication -- Au1 SaPDU *) new rbcNonce; in(c, (sent_ETCS_ID_TYPE, =AU1, =DF_SEND, in_train_etcs_id, trainSaF, trainNonce)); event rbcStartSession(rbc_etcs_id, in_train_etcs_id, rbcNonce, trainSaF, trainNonce); (* Generate the session key *) let rbcKS = genSessionKey(trainNonce, rbcNonce, getKey(rbc_etcs_id, in_train_etcs_id)) in (* Output encrypted secret to check secrecy of keys *) out(c, encrypt(SECRET, rbcKS)); out(c, encrypt(SECRET, getKey(rbc_etcs_id, in_train_etcs_id))); (* T-CONN.response -- Au2 SaPDU *) out(c, (RBC_ETCS_ID_TYPE, AU2, DF_RESP, rbc_etcs_id, trainSaF, rbcNonce, mac(rbcKS, ((PAYLOAD_LENGTH, in_train_etcs_id, RBC_ETCS_ID_TYPE, AU2, DF_RESP, rbc_etcs_id, trainSaF), rbcNonce, trainNonce, in_train_etcs_id)))); (* AU3 SaPDU *) in(c,(=ZEROS, =AU3, =DF_SEND, inMAC)); if inMAC = mac(rbcKS, (PAYLOAD_LENGTH, in_train_etcs_id, ZEROS, AU3, DF_SEND , trainNonce, rbcNonce)) then event rbcFinishSession(rbc_etcs_id, in_train_etcs_id, rbcNonce, trainSaF, trainNonce, rbcKS); (* Receive messages from the train *) in(c, (=DT, timeA, msgA)); event DataReceived1((DT, timeA, msgA)); in(c, (=DT, timeB, msgB)); event DataReceived2((DT, timeB, msgB)); event MessagesReceived2((DT, timeA, msgA), (DT, timeB, msgB)); in(c, (=DT, timeC, msgC)); event DataReceived3((DT, timeC, msgC)); event MessagesReceived3((DT, timeA, msgA), (DT, timeB, msgB), (DT, timeC, msgC)); 0. process !(new new_rbc_id; !out(id, new_rbc_id)) | !(new train_etcs_id; !Train) | !RBC