(* ARINC 823 AMS protocol using a shared secret key described in Attachment 8 of the ARINC specification 823 Part I. CryptoVerif model. *) (**** 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). (* 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). (* 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). (* 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). (* Secrecy of keys The secrecy of KMAC_UV is not preserved in a computational sense, because this key is already used to MAC the second message of the key exchange. We do not test it here. These queries show that the keys KENC_UV are each indistinguishable from random keys, on the aircraft side (secretU_KENC_UV) and on the ground side (secretV_KENC_UV). They do not test whether the keys KENC_UV are independent of each other. *) query secret1 secretU_KENC_UV. query secret1 secretV_KENC_UV. (* These queries show that the keys KENC_UV are indistinguishable from independent random keys, on the aircraft side (secretU_KENC_UV) and on the ground side (secretV_KENC_UV). Independence holds on the ground side. It does not a priori holds on the aircraft side, but it holds if we assume that the aircraft never sends two AMS_Init_REQ messages with the same timestamp (variants SINGLE_TU and REPLAY_PROT). *) query secret secretU_KENC_UV. query secret secretV_KENC_UV. (* 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. (* 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); let secretU_KENC_UV: enc_key = KENC_UV in out(c_aircraft4, ()). 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 let secretV_KENC_UV: enc_key = KENC_UV in out(c_ground2, AMS_Init_RSP). (* 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 *)