(* ARINC 823 AMS protocol using a shared secret key described in Attachment 8 of the ARINC specification 823 Part I. CryptoVerif model. *) (**** Proof indications ****) set autoMove = false. (* Do not move "let received_count_table_960" under "event recv_MsgU". That would prevent proving the injective correspondence recv_msgU ==> sen d_msgV *) (**** Declarations of types, constants, and function symbols ****) (* Type for session ids, used internally in the model to distinguish each session of the protocol. *) type session_ids [large, fixed]. (* Type of 32 bits numbers *) type t_Rand32 [large, fixed]. (* Ids U = aircraft V = ground entity *) type t_id [fixed]. (* 8 bytes = 64 bits entity type, AMS_EntityType *) const U, V: t_id. (* AMS Message elements *) type t_AMS_elem. type t_software_part_number. type t_policy_id. type t_algo_bits [fixed]. fun buildAMS10_s_init_info(t_software_part_number, t_policy_id, t_id, t_id): t_AMS_elem [compos]. fun buildAMS40_entity_id(t_id, t_id): t_AMS_elem [compos]. fun buildAMS41_comp_algo_id(t_algo_bits): t_AMS_elem [compos]. fun buildAMS42_comp_algo_sel(t_algo_bits): t_AMS_elem [compos]. (* The first bit is 1 when DMC level 0 is supported. The second bit is 1 when DMC level 1 is supported. The third bit is 1 when DEFLATE is supported. We ignore algorithms reserved for future use. *) fun payload_with_1_element(t_AMS_elem): bitstring [compos]. fun concat_AMS_element(t_AMS_elem, bitstring): bitstring [compos]. (* Encoding algorithms *) type t_encode_algo [fixed]. (* 2 bits *) const encode_OFF, encode_B64, encode_B64PAD, encode_B128: t_encode_algo. fun encode(t_encode_algo, bitstring): bitstring. fun decode(t_encode_algo, bitstring): bitstring. forall encode_algo: t_encode_algo, payload:bitstring; decode(encode_algo, encode(encode_algo, payload)) = payload. (* encode is injective *) forall encode_algo: t_encode_algo, payload1:bitstring, payload2:bitstring; (encode(encode_algo, payload1) = encode(encode_algo, payload2)) = (payload1 = payload2). (* Compression *) type t_comp_algo [fixed]. (* 4 bits, Value of the CompMode field *) const comp_OFF, comp_DMC0, comp_DMC1, comp_DEFLATE: t_comp_algo. fun compress(t_comp_algo, bitstring): bitstring. fun decompress(t_comp_algo, bitstring): bitstring. forall comp_algo: t_comp_algo, payload:bitstring; decompress(comp_algo, compress(comp_algo, payload)) = payload. fun bool_and(t_algo_bits, t_algo_bits): t_algo_bits. fun select_common_compression(t_AMS_elem, t_comp_algo): t_comp_algo. (* Algorithms *) type t_AMS_AlgID [bounded]. (* 16 bits *) type t_MAClen [bounded]. (* 4 bits *) type t_AuthAlgo [bounded]. (* 4 bits *) type t_EncAlgo [bounded]. (* 8 bits *) fun algo(t_MAClen, t_AuthAlgo, t_EncAlgo): t_AMS_AlgID [compos]. const MAClen32, MAClen64, MAClen128: t_MAClen. const HMAC_SHA256: t_AuthAlgo. const NULL_enc, AES128_CFB128: t_EncAlgo. fun get_common_enc_algo(t_EncAlgo): t_EncAlgo. (* The protocol satisfies authentication independently of the definition of this function. letfun get_common_enc_algo(enc_algo: t_EncAlgo) = if enc_algo = AES128_CFB128 then AES128_CFB128 else NULL_enc. *) (* Policy types *) type t_AMS_Policy [fixed]. (* 2 bits *) const NONE, AUTH, BOTH: t_AMS_Policy. fun get_policy(t_policy_id, bitstring): t_AMS_Policy. (* The definition of the policy is left implicit in this model. get_policy(policy_id, msg) is supposed to determine the expected policy to apply to the message msg from the message msg itself and the policy identifier policy_id. *) fun get_protect_mode(t_AMS_Policy, t_EncAlgo): t_AMS_Policy. (* The protocol satisfies authentication independently of the definition of this function. letfun get_protect_mode(policy: t_AMS_Policy, enc_algo: t_EncAlgo) = if enc_algo = NULL_enc && policy = BOTH then AUTH else policy. If the security policy specifies the BOTH protection mode and the selected encryption is NULL, then ProtectMode is set to AUTH. In all other cases, ProtectMode is the protection mode specified in the security policy. *) (* Protocol ids *) type t_AMS_PID [bounded]. (* 1 byte, "1" or "2" *) const ams_pid1 (* public-key protocol *), ams_pid2 (* shared-key protocol *): t_AMS_PID. (* Commands *) type t_Cmd [fixed]. (* 4 bits *) const Data_IND, Info_IND, DataCnf_IND, Release_REQ, Release_RSP_Minus, Release_RSP_Plus, Init_IND, Init_REQ, Init_RSP_Minus, Init_RSP_Plus, Abort_IND: t_Cmd. fun ok_tunnel(t_Cmd): bool. forall; ok_tunnel(Init_IND) = false. forall; ok_tunnel(Init_REQ) = false. forall; ok_tunnel(Init_RSP_Minus) = false. forall; ok_tunnel(Init_RSP_Plus) = false. (* Counter *) type t_Count [fixed]. const Count1: t_Count. const Count_unspecified: t_Count. (* Used as a dummy value to fill the count argument of event recv_msg when the message is sent unprotected. *) (* MAC *) type mac_key [large, fixed]. proba PPRF. (* PPRF(t, qMAC, l, qKDF256, qKDF128) is the probability of distinguishing MAC, KDF256, and KDF128 from independent pseudo-random functions in time t, with qMAC, qKDF256, qKDF128 queries to MAC, KDF256, and KDF128 respectively, with MAC queries of length at most l. *) (* sessionMAC is SUF-CMA for each of the 3 lengths *) expand SUF_CMA_MAC_3lengths(t_MAClen, MAClen32, MAClen64, MAClen128, mac_key, sessionMAC, PPRF). (* Encryption *) type enc_key [large, fixed]. (* 128 bits *) type t_IVdata [fixed]. type byte [fixed]. (* 1 byte = 8 bits *) const CstDN: byte. (* 0x00 *) const CstUP: byte. (* 0x01 *) fun buildIVdata(byte, t_Count): t_IVdata [compos]. expand encryption_IV_no_hyp(enc_key, t_IVdata, E', D'). (* encryption is IND-CPA provided IVdata is distinct for each encryption --- This property is needed only for secrecy. *) (* Hash function HASH is collision resistant *) type t_SHA256_out [large, fixed]. (* 256 bits, output of SHA256 *) type hash_key [large,fixed]. proba Phash. expand CollisionResistant_hash(hash_key, bitstring, t_SHA256_out, HASH, Phash). type t_AMS_Appendix. fun concat_hash(t_AMS_Appendix, t_Rand32): bitstring [compos]. (* MAC is HMAC_SHA256, it is SUF-CMA and collision-resistant; KDF256, KDF128 are PRFs, even when they share the same key as the MAC *) expand MAC_KDF(mac_key, enc_key, t_SHA256_out, t_id, MAC, KDF256, KDF128, PPRF). (* Time *) type t_AMS_Time [fixed]. fun check_time(t_AMS_Time, t_AMS_Time): bool. (* check_time(tU, tV) is supposed to check that tV - 60 seconds <= tU <= tV + 120 seconds. *) table table_timesU(t_id, t_AMS_Time). (* table used to remember all times tU at which the aircraft started a session, to prevent it from starting two sessions with the same tU. *) table table_timesV(t_id, t_AMS_Time). (* table used to remember all times tV at which the ground entity sent a trigger, to prevent it from sending two triggers with the same tV. *) (* Tables for replay protection for Init_IND and Init_REQ messages *) table received_Init_IND_table(t_id, t_AMS_Time). table received_Init_REQ_table(t_id, t_AMS_Time). (* Supplementary address type *) type t_AMS_SuppAddr. (* Session identifiers *) type t_SID [fixed]. (* 3 bits *) const SID0, SID1, SID2, SID3, SID4, SID5: t_SID. (* Building AMS messages *) type t_AMS_IMI. (* empty or "PM1." *) type t_AMS_ID. (* t_AMS_SuppAddr has variable length, but starts with / and ends with . so it can be distinguished from the PID, and its length can be determined. *) fun buildAMS_id1(t_AMS_SuppAddr, t_AMS_IMI, t_AMS_PID): t_AMS_ID [compos]. fun buildAMS_id2(t_AMS_PID): t_AMS_ID [compos]. type t_AMS_Header. (* 2 bytes = 16 bits *) fun buildAMS_Header(bool (*R1 parameter, ignored*), t_AMS_Policy, t_encode_algo, t_SID, t_comp_algo, t_Cmd): t_AMS_Header [compos]. fun buildAMS_msg_prefix1(t_AMS_ID, t_AMS_Header, bitstring): bitstring [compos]. fun buildAMS_msg_prefix_Init(bitstring, t_AMS_AlgID, t_AMS_Time): bitstring [compos]. fun buildAMS_msg_prefix_RSP(bitstring, t_AMS_AlgID, t_AMS_Time, t_Rand32, t_Count): bitstring [compos]. fun buildAMS_msg_prefix_TBP_RSP(bitstring, t_AMS_AlgID, t_AMS_Time, t_Rand32, t_Count, t_AMS_Appendix): bitstring [compos]. fun buildAMS_msg_prefix_Rest(bitstring, t_Count): bitstring [compos]. fun buildMAC_arg(t_id, t_id, bitstring): bitstring [compos]. fun build_msg_Init(bitstring, t_SHA256_out): bitstring [compos]. fun buildAMS_appendix_Init(t_AMS_AlgID, t_AMS_Time, t_SHA256_out): t_AMS_Appendix [compos]. fun concat(bitstring, bitstring): bitstring. (* concatenation; it is NOT compos, because the lengths of the two concatenated bitstrings is not known. *) fun split_message(t_MAClen, bitstring): bitstring. (* split_message(l, m) returns a pair (m1, m2) such that m is the concatenation of m1 and m2, and m2 has length l. In this protocol, m2 is the MAC, m1 is the rest of the message. *) (* Tables of message counters We simulate a distinct table for each session by adding a unique session identifier as first argument. *) table received_count_table(session_ids, t_Count). table sent_count_table(session_ids, t_Count). (**** Security properties ****) (* Authenticity of the payload messages, when the policy is not NONE *) event send_msgU(t_id, t_id, t_AMS_Time, t_Rand32, t_policy_id, t_AMS_Policy, t_EncAlgo, t_Count, bitstring). event send_msgV(t_id, t_id, t_AMS_Time, t_Rand32, t_policy_id, t_AMS_Policy, t_EncAlgo, t_Count, bitstring). event recv_msgU(t_id, t_id, t_AMS_Time, t_Rand32, t_policy_id, t_AMS_Policy, t_EncAlgo, t_Count, bitstring). event recv_msgV(t_id, t_id, t_AMS_Time, t_Rand32, t_policy_id, t_AMS_Policy, t_EncAlgo, t_Count, bitstring). ifdef(`ORIGINAL',` query x:t_id, y:t_id, tU: t_AMS_Time, randV: t_Rand32, policy_id: t_policy_id, policy: t_AMS_Policy, enc: t_EncAlgo, count: t_Count, msg: bitstring; event recv_msgU(x, y, tU, randV, policy_id, policy, enc, count, msg) ==> policy = get_policy(policy_id, msg) && (send_msgV(y, x, tU, randV, policy_id, policy, enc, count, msg) || policy = NONE). query x:t_id, y:t_id, tU: t_AMS_Time, randV: t_Rand32, policy_id: t_policy_id, policy: t_AMS_Policy, enc: t_EncAlgo, count: t_Count, msg: bitstring; event recv_msgV(x, y, tU, randV, policy_id, policy, enc, count, msg) ==> policy = get_policy(policy_id, msg) && (send_msgU(y, x, tU, randV, policy_id, policy, enc, count, msg) || policy = NONE). ',` (* We have injectivity both in the SINGLE_TU and REPLAY_PROT variants *) query x:t_id, y:t_id, tU: t_AMS_Time, randV: t_Rand32, policy_id: t_policy_id, policy: t_AMS_Policy, enc: t_EncAlgo, count: t_Count, msg: bitstring; event inj:recv_msgU(x, y, tU, randV, policy_id, policy, enc, count, msg) ==> policy = get_policy(policy_id, msg) && (inj:send_msgV(y, x, tU, randV, policy_id, policy, enc, count, msg) || policy = NONE). query x:t_id, y:t_id, tU: t_AMS_Time, randV: t_Rand32, policy_id: t_policy_id, policy: t_AMS_Policy, enc: t_EncAlgo, count: t_Count, msg: bitstring; event inj:recv_msgV(x, y, tU, randV, policy_id, policy, enc, count, msg) ==> policy = get_policy(policy_id, msg) && (inj:send_msgU(y, x, tU, randV, policy_id, policy, enc, count, msg) || policy = NONE). ') (* Freshness of the AMS_Init_REQ message; authentication of the aircraft to the ground entity *) event send_Init_REQ(t_id, t_id, bitstring, t_AMS_Time). event recv_Init_REQ(t_id, t_id, bitstring, t_AMS_Time, t_AMS_Time). ifdef(`REPLAY_PROT',` query x: bitstring, tU: t_AMS_Time, tV: t_AMS_Time; event inj:recv_Init_REQ(V, U, x, tU, tV) ==> check_time(tU, tV) && inj:send_Init_REQ(U, V, x, tU). ',` query x: bitstring, tU: t_AMS_Time, tV: t_AMS_Time; event recv_Init_REQ(V, U, x, tU, tV) ==> check_time(tU, tV) && send_Init_REQ(U, V, x, tU). ') (* Authentication of the ground entity to the aircraft *) event send_Init_RSP(t_id, t_id, bitstring, bitstring, t_Rand32, t_AMS_Time, t_AMS_Time, mac_key, enc_key). event recv_Init_RSP(t_id, t_id, bitstring, bitstring, t_Rand32, t_AMS_Time, mac_key, enc_key). ifdef(`ORIGINAL', ` query x: bitstring, mac: bitstring, RandV: t_Rand32, tU: t_AMS_Time, tV: t_AMS_Time, KMAC_UV: mac_key, KENC_UV: enc_key; event recv_Init_RSP(U, V, x, mac, RandV, tU, KMAC_UV, KENC_UV) ==> check_time(tU, tV) && send_Init_RSP(V, U, x, mac, RandV, tU, tV, KMAC_UV, KENC_UV). ',` query x: bitstring, mac: bitstring, RandV: t_Rand32, tU: t_AMS_Time, tV: t_AMS_Time, KMAC_UV: mac_key, KENC_UV: enc_key; event inj:recv_Init_RSP(U, V, x, mac, RandV, tU, KMAC_UV, KENC_UV) ==> check_time(tU, tV) && inj:send_Init_RSP(V, U, x, mac, RandV, tU, tV, KMAC_UV, KENC_UV). ') (* NOTE: In the correspondence above, the Init_RSP message is split into two arguments: the message prefix (message without its MAC), x, and the MAC, m. This change facilitates the modeling in CryptoVerif because we do not need to express that the concatenation of the prefix and the MAC is injective once the length of the MAC is known. *) (* Freshness of the AMS_Init_IND message (ground-initiated trigger) *) event send_Init_IND(t_id, t_id, bitstring, t_AMS_Time). event recv_Init_IND(t_id, t_id, bitstring, t_AMS_Time, t_AMS_Time). ifdef(`REPLAY_PROT',` query x: bitstring, tV: t_AMS_Time, tU: t_AMS_Time; event inj:recv_Init_IND(U, V, x, tV, tU) ==> check_time(tV, tU) && inj:send_Init_IND(V, U, x, tV). ',` query x: bitstring, tV: t_AMS_Time, tU: t_AMS_Time; event recv_Init_IND(U, V, x, tV, tU) ==> check_time(tV, tU) && send_Init_IND(V, U, x, tV). ') (* Secrecy -- see arinc823-secret-key.SECRECY.cv *) (**** The protocol ****) param Naircraft, Nground, Nground_init, Nground_init_react, Nmessage. channel c_gen1, c_gen2, c_aircraft0, c_aircraft0', c_aircraft1, c_aircraft2, c_aircraft3, c_aircraft4, c_ground1, c_ground2, c_ground_initiated_trigger1, c_ground_initiated_trigger2, c_aircraft_react_ground_initiated_trigger1, c_aircraft_react_ground_initiated_trigger2, choicechannel, pub. (* The process tunnel_protocol models the secure session data exchange (Attachment 8, Section 8.3) *) let tunnel_protocolU = ( (* Sender side *) ! Nmessage in(choicechannel, (AMS_payload: bitstring, encode_alg: t_encode_algo, comp_algo: t_comp_algo, ams_dstaddr: t_AMS_SuppAddr, ams_imi: t_AMS_IMI, count: t_Count, cmd: t_Cmd)); (* cmd can be - Data_IND / DataCnf_IND in case D04 - Info_IND in case X04 - Release_REQ in case R03 (Confirmed release) - Release_RSP+ / Release_RSP- in case R12 (reply to a confirmed release request) - Abort_IND in case A03 (Abort) *) if ok_tunnel(cmd) then (* We never send two messages with the same count, in the same session. *) get sent_count_table(=current_session_id, =count) in yield else let policy_req = get_policy(policy_id, AMS_payload) in event send_msgU(my_id, other_id, tU, RandV, policy_id, policy_req, common_enc_algo, count, AMS_payload); (* D01 *) if policy_req = NONE then out(pub, AMS_payload) else (* D/X02 *) let encoded_payload = encode(encode_alg, AMS_payload) in let actual_comp_algo = select_common_compression(common_comp_algo_id, comp_algo) in let compressed_payload = compress(actual_comp_algo, encoded_payload) in insert sent_count_table(current_session_id, count); (* D/X03 *) let protect_mode = get_protect_mode(policy_req, common_enc_algo) in let encrypted_AMS_payload = if protect_mode = AUTH then compressed_payload else E'(KENC_UV, buildIVdata(dir_send, count), compressed_payload) in (* D/X04 *) let ams_id = buildAMS_id1(ams_dstaddr, ams_imi, ams_pid) in let ams_header = buildAMS_Header(false, protect_mode, encode_alg, sid, actual_comp_algo, cmd) in let AMS_Data_IND_prefix = buildAMS_msg_prefix1(ams_id, ams_header, buildAMS_msg_prefix_Rest(encrypted_AMS_payload, count)) in let TBP_AMS_Data_IND = buildMAC_arg(my_id, other_id, AMS_Data_IND_prefix) in let mac = sessionMAC(MAClen, KMAC_UV, TBP_AMS_Data_IND) in let AMS_Data_IND = concat(AMS_Data_IND_prefix, mac) in (* D/X05 *) out(pub, AMS_Data_IND) ) | ( (* Receiver side *) ! Nmessage in(pub, (clear:bool, AMS_Data_IND: bitstring)); (* clear is true when the received message is not AMS-protected. This is determined using the ACARS label: there are specific Px ACARS labels for AMS protected messages (cf p. 58) *) if clear then ( (* Policy check not explicit in the description of the protocol p 135, but mentioned p 29-30, and essential for security *) if get_policy(policy_id, AMS_Data_IND) = NONE then event recv_msgU(my_id, other_id, tU, RandV, policy_id, NONE, common_enc_algo, Count_unspecified, AMS_Data_IND) ) else (* D/X06 *) let (AMS_Data_IND_prefix: bitstring, mac: bitstring) = split_message(MAClen, AMS_Data_IND) in (* The MAC checking of step D/X08 is moved here to facilitate verification *) let TBP_AMS_Data_IND = buildMAC_arg(other_id, my_id, AMS_Data_IND_prefix) in if mac = sessionMAC(MAClen, KMAC_UV, TBP_AMS_Data_IND) then let buildAMS_msg_prefix1(ams_id, ams_header, buildAMS_msg_prefix_Rest(encrypted_AMS_payload, MsgCount)) = AMS_Data_IND_prefix in let buildAMS_Header(R1, protect_mode, encode_alg, sid, compression, cmd) = ams_header in if ok_tunnel(cmd) then (* D/X07 *) (* D/X08 *) (* Check on the message count is slightly weaker than the check given in the specification: we just discard the message if a message with the same count has already been received in the same session. *) get received_count_table(=current_session_id, =MsgCount) in yield else insert received_count_table(current_session_id, MsgCount); (* Message accepted *) (* D/X09 *) let compressed_payload = if protect_mode = AUTH then encrypted_AMS_payload else D'(KENC_UV, buildIVdata(dir_recv, MsgCount), encrypted_AMS_payload) in (* D/X10 *) let encoded_payload = decompress(compression, compressed_payload) in let AMS_payload = decode(encode_alg, encoded_payload) in (* Policy check not explicit in the description of the protocol p 137, but mentioned p 29-30 *) let policy_req = get_policy(policy_id, AMS_payload) in if protect_mode = get_protect_mode(policy_req, common_enc_algo) then event recv_msgU(my_id, other_id, tU, RandV, policy_id, policy_req, common_enc_algo, MsgCount, AMS_payload) ). let tunnel_protocolV = ( (* Sender side *) ! Nmessage in(choicechannel, (AMS_payload: bitstring, encode_alg: t_encode_algo, comp_algo: t_comp_algo, ams_dstaddr: t_AMS_SuppAddr, ams_imi: t_AMS_IMI, count: t_Count, cmd: t_Cmd)); (* cmd can be - Data_IND / DataCnf_IND in case D04 - Info_IND in case X04 - Release_REQ in case R03 (Confirmed release) - Release_RSP+ / Release_RSP- in case R12 (reply to a confirmed release request) - Abort_IND in case A03 (Abort) *) if ok_tunnel(cmd) then (* We never send two messages with the same count, in the same session. *) get sent_count_table(=current_session_id, =count) in yield else let policy_req = get_policy(policy_id, AMS_payload) in event send_msgV(my_id, other_id, tU, RandV, policy_id, policy_req, common_enc_algo, count, AMS_payload); (* D01 *) if policy_req = NONE then out(pub, AMS_payload) else (* D/X02 *) let encoded_payload = encode(encode_alg, AMS_payload) in let actual_comp_algo = select_common_compression(common_comp_algo_id, comp_algo) in let compressed_payload = compress(actual_comp_algo, encoded_payload) in insert sent_count_table(current_session_id, count); (* D/X03 *) let protect_mode = get_protect_mode(policy_req, common_enc_algo) in let encrypted_AMS_payload = if protect_mode = AUTH then compressed_payload else E'(KENC_UV, buildIVdata(dir_send, count), compressed_payload) in (* D/X04 *) let ams_id = buildAMS_id1(ams_dstaddr, ams_imi, ams_pid) in let ams_header = buildAMS_Header(false, protect_mode, encode_alg, sid, actual_comp_algo, cmd) in let AMS_Data_IND_prefix = buildAMS_msg_prefix1(ams_id, ams_header, buildAMS_msg_prefix_Rest(encrypted_AMS_payload, count)) in let TBP_AMS_Data_IND = buildMAC_arg(my_id, other_id, AMS_Data_IND_prefix) in let mac = sessionMAC(MAClen, KMAC_UV, TBP_AMS_Data_IND) in let AMS_Data_IND = concat(AMS_Data_IND_prefix, mac) in (* D/X05 *) out(pub, AMS_Data_IND) ) | ( (* Receiver side *) ! Nmessage in(pub, (clear:bool, AMS_Data_IND: bitstring)); (* clear is true when the received message is not AMS-protected. This is determined using the ACARS label: there are specific Px ACARS labels for AMS protected messages (cf p. 58) *) if clear then ( (* Policy check not explicit in the description of the protocol p 135, but mentioned p 29-30, and essential for security *) if get_policy(policy_id, AMS_Data_IND) = NONE then event recv_msgV(my_id, other_id, tU, RandV, policy_id, NONE, common_enc_algo, Count_unspecified, AMS_Data_IND) ) else (* D/X06 *) let (AMS_Data_IND_prefix: bitstring, mac: bitstring) = split_message(MAClen, AMS_Data_IND) in (* The MAC checking of step D/X08 is moved here to facilitate verification *) let TBP_AMS_Data_IND = buildMAC_arg(other_id, my_id, AMS_Data_IND_prefix) in if mac = sessionMAC(MAClen, KMAC_UV, TBP_AMS_Data_IND) then let buildAMS_msg_prefix1(ams_id, ams_header, buildAMS_msg_prefix_Rest(encrypted_AMS_payload, MsgCount)) = AMS_Data_IND_prefix in let buildAMS_Header(R1, protect_mode, encode_alg, sid, compression, cmd) = ams_header in if ok_tunnel(cmd) then (* D/X07 *) (* D/X08 *) (* Check on the message count is slightly weaker than the check given in the specification: we just discard the message if a message with the same count has already been received in the same session. *) get received_count_table(=current_session_id, =MsgCount) in yield else insert received_count_table(current_session_id, MsgCount); (* Message accepted *) (* D/X09 *) let compressed_payload = if protect_mode = AUTH then encrypted_AMS_payload else D'(KENC_UV, buildIVdata(dir_recv, MsgCount), encrypted_AMS_payload) in (* D/X10 *) let encoded_payload = decompress(compression, compressed_payload) in let AMS_payload = decode(encode_alg, encoded_payload) in (* Policy check not explicit in the description of the protocol p 137, but mentioned p 29-30 *) let policy_req = get_policy(policy_id, AMS_payload) in if protect_mode = get_protect_mode(policy_req, common_enc_algo) then event recv_msgV(my_id, other_id, tU, RandV, policy_id, policy_req, common_enc_algo, MsgCount, AMS_payload) ). (* Secure session initiation, aircraft-initiated (Attachement 8, Section 8.2.1) *) let aircraft_fixed_MAClen = in(c_aircraft1, (software_part_number: t_software_part_number, policy_id: t_policy_id, algo_bits: t_algo_bits, encode_alg: t_encode_algo, ams_dstaddr: t_AMS_SuppAddr, ams_imi: t_AMS_IMI, sid: t_SID, tU: t_AMS_Time, enc_algo: t_EncAlgo (* either NULL_enc or AES128_CFB128, depending on whether the aircraft supports encryption *))); ifdef(`ORIGINAL',`',` (* Refuse to run the aircraft session twice with the same tU. This is necessary to prove secrecy. It models the recommendation that the aircraft should never run two sessions with the same tU. *) get table_timesU(=V, =tU) in yield else insert table_timesU(V, tU); ') (* Choose a session id *) new current_session_id: session_ids; (* Message 1, N01 *) let s_init_info = buildAMS10_s_init_info(software_part_number, policy_id, U, V) in let comp_algo_id = buildAMS41_comp_algo_id(algo_bits) in let ams_payload = concat_AMS_element(s_init_info, payload_with_1_element(comp_algo_id)) in let encoded_payload = encode(encode_alg, ams_payload) in (* N02 *) let ams_id = buildAMS_id1(ams_dstaddr, ams_imi, ams_pid2) in let ams_header = buildAMS_Header(false, AUTH, encode_alg, sid, comp_OFF, Init_REQ) in let alg_ID_U = algo(MAClen, HMAC_SHA256, enc_algo) in let AMS_Init_REQ_prefix = buildAMS_msg_prefix1(ams_id, ams_header, buildAMS_msg_prefix_Init(encoded_payload, alg_ID_U, tU)) in let TBP_AMS_Init_REQ = buildMAC_arg(U, V, AMS_Init_REQ_prefix) in let MAC0_U = MAC(K_UV, TBP_AMS_Init_REQ) in let AMS_Appendix = buildAMS_appendix_Init(alg_ID_U, tU, MAC0_U) in let AMS_Init_REQ = build_msg_Init(AMS_Init_REQ_prefix, MAC0_U) in (* N03 *) event send_Init_REQ(U, V, AMS_Init_REQ, tU); out(c_aircraft2, AMS_Init_REQ); (* Message 2, N12 *) in(c_aircraft3, AMS_Init_RSP: bitstring); let (AMS_Init_RSP_prefix: bitstring, mac2: bitstring) = split_message(MAClen, AMS_Init_RSP) in let buildAMS_msg_prefix1(ams_id2, ams_header2, buildAMS_msg_prefix_RSP(compressed_payload2, AlgSel, =tU, RandV, MsgCount)) = AMS_Init_RSP_prefix in let buildAMS_Header(R1, =AUTH, encode_alg2, sid2, compression2, cmd2) = ams_header2 in let encoded_payload2 = decompress(compression2, compressed_payload2) in let AMS_payload2 = decode(encode_alg2, encoded_payload2) in let concat_AMS_element(common_comp_algo_id, app_data2) = AMS_payload2 in (* N13 *) let X_UV = HASH(hk, concat_hash(AMS_Appendix, RandV)) in (* N14 *) let algo(MAClen', =HMAC_SHA256, common_enc_algo) = AlgSel in (* We use the MAC length initially chosen by the aircraft, and ignore the MAC length included in AlgSel. *) let KMAC_UV = KDF256(K_UV, X_UV, U, V) in (* N15 - This should be done only if the encryption is not NULL, but doing it anyway does not hurt. *) let KENC_UV = KDF128(K_UV, X_UV, U, V) in (* N16 *) let TBP_AMS_Init_RSP = buildMAC_arg(V, U, buildAMS_msg_prefix1(ams_id2, ams_header2, buildAMS_msg_prefix_TBP_RSP(compressed_payload2, AlgSel, tU, RandV, MsgCount, AMS_Appendix))) in (* N17 *) if MsgCount = Count1 then if mac2 = sessionMAC(MAClen, KMAC_UV, TBP_AMS_Init_RSP) then if cmd2 = Init_RSP_Plus then insert received_count_table(current_session_id, Count1); (* When the command is Init_RSP- instead of Init_RSP_Plus, the aircraft entity executes an airline configurable unavailable action, which is ignored here. *) (* Message accepted, secure session established *) (* Parameters for the process tunnel_protocol *) let ams_pid = ams_pid2 in let dir_send = CstDN in let dir_recv = CstUP in let my_id = U in let other_id = V in event recv_Init_RSP(U, V, AMS_Init_RSP_prefix, mac2, RandV, tU, KMAC_UV, KENC_UV); out(c_aircraft4, ()); tunnel_protocolU. (*tunnel_protocol(ams_pid2, common_comp_algo_id, policy_id, KMAC_UV, KENC_UV, MAClen, common_enc_algo, sid, CstDN, CstUP, U, V)*) let aircraft = (in(c_aircraft0, MAClen: t_MAClen); if MAClen = MAClen32 || MAClen = MAClen64 || MAClen = MAClen128 then out(c_aircraft0', ()); aircraft_fixed_MAClen). let ground = in(c_ground1, (gd_algo_bits: t_algo_bits, tV: t_AMS_Time, app_data: bitstring, encode_alg: t_encode_algo, comp_algo: t_comp_algo, AMS_Init_REQ: bitstring)); (* Choose a session id *) new current_session_id: session_ids; (* Message 1, N04 *) let build_msg_Init(AMS_Init_REQ_prefix, MAC0_U) = AMS_Init_REQ in (* The MAC checking of step N05 is moved here to facilitate verification *) let TBP_AMS_Init_REQ = buildMAC_arg(U, V, AMS_Init_REQ_prefix) in if MAC0_U = MAC(K_UV, TBP_AMS_Init_REQ) then let buildAMS_msg_prefix1(ams_id, ams_header, buildAMS_msg_prefix_Init(encoded_payload, alg_ID_U, tU)) = AMS_Init_REQ_prefix in let AMS_Appendix = buildAMS_appendix_Init(alg_ID_U, tU, MAC0_U) in if check_time(tU, tV) then let buildAMS_Header(R1, =AUTH, encode_alg: t_encode_algo, sid: t_SID, compression: t_comp_algo, =Init_REQ) = ams_header in let ams_payload = decode(encode_alg, encoded_payload) in let algo(MAClen, =HMAC_SHA256, enc_algo) = alg_ID_U in let common_enc_algo = get_common_enc_algo(enc_algo) in let concat_AMS_element(s_init_info, payload_with_1_element(comp_algo_id)) = ams_payload in let buildAMS10_s_init_info(software_part_number, policy_id, =U, =V) = s_init_info in let buildAMS41_comp_algo_id(algo_bits) = comp_algo_id in let gd_comp_algo_id = buildAMS41_comp_algo_id(gd_algo_bits) in let common_comp_algo_id = buildAMS42_comp_algo_sel(bool_and(algo_bits, gd_algo_bits)) in (* N05 *) ifdef(`REPLAY_PROT',` (* Replay protection. This check is stronger than the one in the specification! *) get received_Init_REQ_table(=U, =tU) in yield else insert received_Init_REQ_table(U, tU); ',` (* Uniqueness check of AMS_Appendix not modeled *) ') (* N06 - Message 1 accepted *) (* Termination of another session with the same peer aircraft not modeled *) new RandV: t_Rand32; let X_UV = HASH(hk, concat_hash(AMS_Appendix, RandV)) in (* event recv_Init_REQ put after some variable definitions to help prove injectivity *) event recv_Init_REQ(V, U, AMS_Init_REQ, tU, tV); (* N07 *) let KMAC_UV = KDF256(K_UV, X_UV, U, V) in (* N08 - This should be done only if the encryption is not NULL, but doing it anyway does not hurt. *) let KENC_UV = KDF128(K_UV, X_UV, U, V) in (* Message 2, N09 *) (* I consider the optional Query and Ping as application data, whose content does not need to be detailed. *) let AMS_payload = concat_AMS_element(common_comp_algo_id, app_data) in let encoded_payload = encode(encode_alg, AMS_payload) in let actual_comp_algo = select_common_compression(common_comp_algo_id, comp_algo) in let compressed_payload = compress(actual_comp_algo, encoded_payload) in insert sent_count_table(current_session_id, Count1); (* N10 *) let ams_id = buildAMS_id2(ams_pid2) in let ams_header = buildAMS_Header(false, AUTH, encode_alg, sid, actual_comp_algo, Init_RSP_Plus) in let AlgSel = algo(MAClen, HMAC_SHA256, common_enc_algo) in let AMS_Init_RSP_prefix = buildAMS_msg_prefix1(ams_id, ams_header, buildAMS_msg_prefix_RSP(compressed_payload, AlgSel, tU, RandV, Count1)) in let TBP_AMS_Init_RSP = buildMAC_arg(V, U, buildAMS_msg_prefix1(ams_id, ams_header, buildAMS_msg_prefix_TBP_RSP(compressed_payload, AlgSel, tU, RandV, Count1, AMS_Appendix))) in let mac = sessionMAC(MAClen, KMAC_UV, TBP_AMS_Init_RSP) in let AMS_Init_RSP = concat(AMS_Init_RSP_prefix, mac) in (* N11 *) event send_Init_RSP(V, U, AMS_Init_RSP_prefix, mac, RandV, tU, tV, KMAC_UV, KENC_UV); (* Parameters for the process tunnel_protocol *) let ams_pid = ams_pid2 in let dir_send = CstUP in let dir_recv = CstDN in let my_id = V in let other_id = U in out(c_ground2, AMS_Init_RSP); tunnel_protocolV. (* tunnel_protocol(ams_pid2, common_comp_algo_id, policy_id, KMAC_UV, KENC_UV, MAClen, common_enc_algo, sid, CstUP, CstDN, V, U)*) (* Ground-initiated trigger (Attachment 8, Section 8.2.2). *) let ground_initiated_trigger = in(c_ground_initiated_trigger1, (encode_alg: t_encode_algo, MAClen: t_MAClen, tV: t_AMS_Time)); ifdef(`REPLAY_PROT',` (* Refuse to run the ground initiated trigger twice with the same tV. To protect against replays. *) get table_timesV(=U, =tV) in yield else insert table_timesV(U, tV); ') (* G01 *) let ams_payload = payload_with_1_element(buildAMS40_entity_id(U,V)) in let encoded_payload = encode(encode_alg, ams_payload) in (* G02 *) let ams_id = buildAMS_id2(ams_pid2) in let ams_header = buildAMS_Header(false, AUTH, encode_alg, SID0, comp_OFF, Init_IND) in let alg_ID_V = algo(MAClen, HMAC_SHA256, AES128_CFB128) in let AMS_Init_IND_prefix = buildAMS_msg_prefix1(ams_id, ams_header, buildAMS_msg_prefix_Init(encoded_payload, alg_ID_V, tV)) in let TBP_AMS_Init_IND = buildMAC_arg(V, U, AMS_Init_IND_prefix) in let MAC0_V = MAC(K_UV, TBP_AMS_Init_IND) in let AMS_Init_IND = build_msg_Init(AMS_Init_IND_prefix, MAC0_V) in (* G03 *) event send_Init_IND(V, U, AMS_Init_IND, tV); out(c_ground_initiated_trigger2, AMS_Init_IND). let aircraft_react_ground_initiated_trigger = (* G04 *) in(c_aircraft_react_ground_initiated_trigger1, (tU: t_AMS_Time, AMS_Init_IND: bitstring)); let build_msg_Init(AMS_Init_IND_prefix, MAC0_V) = AMS_Init_IND in let buildAMS_msg_prefix1(ams_id, ams_header, buildAMS_msg_prefix_Init(encoded_payload, alg_ID_V, tV)) = AMS_Init_IND_prefix in if check_time(tV, tU) then let buildAMS_Header(R1, =AUTH, encode_alg: t_encode_algo, sid: t_SID, compression: t_comp_algo, =Init_IND) = ams_header in let ams_payload = decode(encode_alg, encoded_payload) in let payload_with_1_element(buildAMS40_entity_id(=U,=V)) = ams_payload in (* G05 *) let TBP_AMS_Init_IND = buildMAC_arg(V, U, AMS_Init_IND_prefix) in if MAC0_V = MAC(K_UV, TBP_AMS_Init_IND) then ifdef(`REPLAY_PROT',` (* Replay protection. This check is not present in the specification! *) get received_Init_IND_table(=V, =tV) in yield else insert received_Init_IND_table(V, tV); ') (* G06 - Message accepted *) event recv_Init_IND(U, V, AMS_Init_IND, tV, tU); out(c_aircraft_react_ground_initiated_trigger1, ()). (* We let the adversary schedule the aircraft; no need to put it explicitly here. *) (* Putting the whole system together *) process in(c_gen1, ()); new K_UV: mac_key; new hk: hash_key; out(c_gen2, hk); ((! Naircraft aircraft) | (! Nground ground) | (! Nground_init ground_initiated_trigger) | (! Nground_init_react aircraft_react_ground_initiated_trigger)) (* EXPECTED All queries proved. 47.471s (user 46.743s + system 0.728s), max rss 1390400K END *)