SHARED KEY PROTOCOL

PROTOCOL shared-key PV AUTHENTICATION.ENC_SUPPORTED.FAST
RESULT event(recv_Init_IND(U,V,x_691,tV_692,tU_693)) ==> (check_time(tV_692,tU_693) && event(send_Init_IND(V,U,x_691,tV_692))) is true.
RESULT event(recv_Init_RSP(U,V,x_801342,RandV_801343,tU_801344,KMAC_UV_801346,KENC_UV_801347)) ==> (check_time(tU_801344,tV_801345) && event(send_Init_RSP(V,U,x_801342,RandV_801343,tU_801344,tV_801345,KMAC_UV_801346,KENC_UV_801347))) is true.
RESULT event(recv_Init_REQ(V,U,x_2698992,tU_2698993,tV_2698994)) ==> (check_time(tU_2698993,tV_2698994) && event(send_Init_REQ(U,V,x_2698992,tU_2698993))) is true.
RESULT event(recv_msg(x_3516399,y_3516400,tU_3516401,randV,policy_id_3516402,policy,enc,count_3516403,msg_3516404)) ==> (policy_ok(policy_id_3516402,policy,msg_3516404) && policy_ok(policy_id_3516402,policy2,msg_3516404) && event(send_msg(y_3516400,x_3516399,tU_3516401,randV,policy_id_3516402,policy2,enc,count_3516403,msg_3516404))) || (policy_ok(policy_id_3516402,policy,msg_3516404) && policy_ok(policy_id_3516402,policy2,msg_3516404) && policy = NONE) is true.
207.473s (user 207.353s + system 0.120s), max rss 948512K
PROTOCOL shared-key PV AUTHENTICATION.ENC_NOTSUPPORTED.FAST
RESULT event(recv_Init_IND(U,V,x_691,tV_692,tU_693)) ==> (check_time(tV_692,tU_693) && event(send_Init_IND(V,U,x_691,tV_692))) is true.
RESULT event(recv_Init_RSP(U,V,x_715578,RandV_715579,tU_715580,KMAC_UV_715582,KENC_UV_715583)) ==> (check_time(tU_715580,tV_715581) && event(send_Init_RSP(V,U,x_715578,RandV_715579,tU_715580,tV_715581,KMAC_UV_715582,KENC_UV_715583))) is true.
RESULT event(recv_Init_REQ(V,U,x_1969935,tU_1969936,tV_1969937)) ==> (check_time(tU_1969936,tV_1969937) && event(send_Init_REQ(U,V,x_1969935,tU_1969936))) is true.
RESULT event(recv_msg(x_2707767,y_2707768,tU_2707769,randV,policy_id_2707770,policy,enc,count_2707771,msg_2707772)) ==> (policy_ok(policy_id_2707770,policy,msg_2707772) && policy_ok(policy_id_2707770,policy2,msg_2707772) && event(send_msg(y_2707768,x_2707767,tU_2707769,randV,policy_id_2707770,policy2,enc,count_2707771,msg_2707772))) || (policy_ok(policy_id_2707770,policy,msg_2707772) && policy_ok(policy_id_2707770,policy2,msg_2707772) && policy = NONE) is true.
159.838s (user 159.766s + system 0.072s), max rss 792416K
PROTOCOL shared-key PV SECRECY.ENC_SUPPORTED.FAST
RESULT attacker(payload_message(s,r,policy_id_696,x_697)) ==> policy_ok(policy_id_696,AUTH,payload_message(s,r,policy_id_696,x_697)) || policy_ok(policy_id_696,NONE,payload_message(s,r,policy_id_696,x_697)) is true.
20.321s (user 20.301s + system 0.020s), max rss 252640K
PROTOCOL shared-key PV SECRECY.ENC_NOTSUPPORTED.FAST
RESULT attacker(payload_message(s,r,policy_id_696,x_697)) ==> policy_ok(policy_id_696,AUTH,payload_message(s,r,policy_id_696,x_697)) || policy_ok(policy_id_696,NONE,payload_message(s,r,policy_id_696,x_697)) cannot be proved.
14.849s (user 14.825s + system 0.024s), max rss 233104K
PROTOCOL shared-key PV KEY_SECRECY.ENC_SUPPORTED.FAST
RESULT not attacker(secretU_KENC[]) is true.
RESULT not attacker(secretU_KMAC[]) is true.
RESULT not attacker(secretV_KENC[]) is true.
RESULT not attacker(secretV_KMAC[]) is true.
2.684s (user 2.668s + system 0.016s), max rss 120224K
PROTOCOL shared-key PV KEY_SECRECY.ENC_NOTSUPPORTED.FAST
RESULT not attacker(secretU_KENC[]) is true.
RESULT not attacker(secretU_KMAC[]) is true.
RESULT not attacker(secretV_KENC[]) is true.
RESULT not attacker(secretV_KMAC[]) is true.
2.664s (user 2.648s + system 0.016s), max rss 120224K
PROTOCOL shared-key PV UKS.ENC_SUPPORTED.FAST
RESULT event(send_and_recv_Init_RSP(Vx_707,Ux_706,x_708,RandV_709,tU_710,tV_711,KMAC_UV_712,KENC_UV_713,Ux2,Vx2,x2,RandV2,tU2,KMAC_UV2,KENC_UV_713)) ==> (Ux_706 = Ux2 && Vx_707 = Vx2) is true.
RESULT event(send_and_recv_Init_RSP(Vx_707,Ux_706,x_708,RandV_709,tU_710,tV_711,KMAC_UV_712,KENC_UV_713,Ux2,Vx2,x2,RandV2,tU2,KMAC_UV_712,KENC_UV2)) ==> (Ux_706 = Ux2 && Vx_707 = Vx2) is true.
13.505s (user 13.477s + system 0.028s), max rss 208784K
PROTOCOL shared-key PV UKS.ENC_NOTSUPPORTED.FAST
RESULT event(send_and_recv_Init_RSP(Vx_707,Ux_706,x_708,RandV_709,tU_710,tV_711,KMAC_UV_712,KENC_UV_713,Ux2,Vx2,x2,RandV2,tU2,KMAC_UV2,KENC_UV_713)) ==> (Ux_706 = Ux2 && Vx_707 = Vx2) is true.
RESULT event(send_and_recv_Init_RSP(Vx_707,Ux_706,x_708,RandV_709,tU_710,tV_711,KMAC_UV_712,KENC_UV_713,Ux2,Vx2,x2,RandV2,tU2,KMAC_UV_712,KENC_UV2)) ==> (Ux_706 = Ux2 && Vx_707 = Vx2) is true.
12.629s (user 12.609s + system 0.020s), max rss 208784K

PROTOCOL shared-key CV SECRECY.ORIGINAL
RESULT Could not prove secrecy of b.
267.953s (user 267.841s + system 0.112s), max rss 726240K
PROTOCOL shared-key CV SECRECY.SINGLE_TU
All queries proved.
37.530s (user 37.478s + system 0.052s), max rss 511184K
PROTOCOL shared-key CV SECRECY.REPLAY_PROT
All queries proved.
56.604s (user 56.496s + system 0.108s), max rss 516304K
PROTOCOL shared-key CV AUTHENTICATION.ORIGINAL
All queries proved.
66.548s (user 66.472s + system 0.076s), max rss 642608K
PROTOCOL shared-key CV AUTHENTICATION.SINGLE_TU
All queries proved.
33.014s (user 32.954s + system 0.060s), max rss 436784K
PROTOCOL shared-key CV AUTHENTICATION.REPLAY_PROT
All queries proved.
42.275s (user 42.235s + system 0.040s), max rss 432880K
PROTOCOL shared-key CV UKS.ORIGINAL
All queries proved.
28.370s (user 28.342s + system 0.028s), max rss 262912K
PROTOCOL shared-key CV UKS.SINGLE_TU
All queries proved.
40.407s (user 40.391s + system 0.016s), max rss 267328K
PROTOCOL shared-key CV UKS.REPLAY_PROT
All queries proved.
42.851s (user 42.811s + system 0.040s), max rss 267008K
PROTOCOL shared-key CV KEY_SECRECY.ORIGINAL
RESULT Could not prove secrecy of secretU_KENC_UV.
9.173s (user 9.145s + system 0.028s), max rss 162832K
PROTOCOL shared-key CV KEY_SECRECY.SINGLE_TU
All queries proved.
2.056s (user 2.036s + system 0.020s), max rss 94000K
PROTOCOL shared-key CV KEY_SECRECY.REPLAY_PROT
All queries proved.
6.796s (user 6.788s + system 0.008s), max rss 98160K

PUBLIC KEY PROTOCOL

PROTOCOL public-key PV SECRECY.NO_COMPROMISE.ENC_SUPPORTED.FAST
RESULT attacker(payload_message(U,V,policy_id_1038,x_1039)) ==> policy_ok(policy_id_1038,AUTH,payload_message(U,V,policy_id_1038,x_1039)) || policy_ok(policy_id_1038,NONE,payload_message(U,V,policy_id_1038,x_1039)) is true.
RESULT attacker(payload_message(V,U,policy_id_1038,x_1039)) ==> policy_ok(policy_id_1038,AUTH,payload_message(V,U,policy_id_1038,x_1039)) || policy_ok(policy_id_1038,NONE,payload_message(V,U,policy_id_1038,x_1039)) is true.
843.249s (user 843.021s + system 0.228s), max rss 1407696K
PROTOCOL public-key PV SECRECY.NO_COMPROMISE.ENC_NOTSUPPORTED.FAST
RESULT attacker(payload_message(U,V,policy_id_1038,x_1039)) ==> policy_ok(policy_id_1038,AUTH,payload_message(U,V,policy_id_1038,x_1039)) || policy_ok(policy_id_1038,NONE,payload_message(U,V,policy_id_1038,x_1039)) cannot be proved.
RESULT attacker(payload_message(V,U,policy_id_1038,x_1039)) ==> policy_ok(policy_id_1038,AUTH,payload_message(V,U,policy_id_1038,x_1039)) || policy_ok(policy_id_1038,NONE,payload_message(V,U,policy_id_1038,x_1039)) cannot be proved.
744.663s (user 744.487s + system 0.176s), max rss 1344336K
PROTOCOL public-key PV AUTHENTICATION.NO_COMPROMISE.ENC_SUPPORTED.FAST
RESULT event(recv_Init_IND(U,V,x_1030,sV_1031,tV_1032,tU_1033)) ==> (check_time(tV_1032,tU_1033) && event(send_Init_IND(V,U,x_1030,sV_1031,tV_1032))) is true.
RESULT event(send_and_recv_Init_RSP(Vx_3350740,Ux_3350739,x_3350741,sU_3350742,RandV_3350743,tU_3350744,tV_3350745,KMAC_UV_3350746,KENC_UV_3350747,Ux2,Vx2,x2,sU2,RandV2,tU2,KMAC_UV2,KENC_UV_3350747)) ==> (Ux_3350739 = Ux2 && Vx_3350740 = Vx2) is true.
RESULT event(send_and_recv_Init_RSP(Vx_3350740,Ux_3350739,x_3350741,sU_3350742,RandV_3350743,tU_3350744,tV_3350745,KMAC_UV_3350746,KENC_UV_3350747,Ux2,Vx2,x2,sU2,RandV2,tU2,KMAC_UV_3350746,KENC_UV2)) ==> (Ux_3350739 = Ux2 && Vx_3350740 = Vx2) is true.
RESULT inj-event(recv_Init_RSP(U,V,x_13068268,sU_13068269,RandV_13068270,tU_13068271,KMAC_UV_13068273,KENC_UV_13068274)) ==> (check_time(tU_13068271,tV_13068272) && inj-event(send_Init_RSP(V,U,x_13068268,sU_13068269,RandV_13068270,tU_13068271,tV_13068272,KMAC_UV_13068273,KENC_UV_13068274))) is true.
RESULT event(recv_Init_REQ(V,U,x_26752076,sU_26752077,tU_26752078,tV_26752079)) ==> (check_time(tU_26752078,tV_26752079) && event(send_Init_REQ(U,V,x_26752076,sU_26752077,tU_26752078))) is true.
RESULT event(recv_msg(U,V,tU_30187765,sU_30187766,randV,policy_id_30187767,policy,enc,count_30187768,msg_30187769)) ==> (policy_ok(policy_id_30187767,policy,msg_30187769) && policy_ok(policy_id_30187767,policy2,msg_30187769) && event(send_msg(V,U,tU_30187765,sU_30187766,randV,policy_id_30187767,policy2,enc,count_30187768,msg_30187769))) || (policy_ok(policy_id_30187767,policy,msg_30187769) && policy_ok(policy_id_30187767,policy2,msg_30187769) && policy = NONE) is true.
RESULT event(recv_msg(V,U,tU_30187765,sU_30187766,randV,policy_id_30187767,policy,enc,count_30187768,msg_30187769)) ==> (policy_ok(policy_id_30187767,policy,msg_30187769) && policy_ok(policy_id_30187767,policy2,msg_30187769) && event(send_msg(U,V,tU_30187765,sU_30187766,randV,policy_id_30187767,policy2,enc,count_30187768,msg_30187769))) || (policy_ok(policy_id_30187767,policy,msg_30187769) && policy_ok(policy_id_30187767,policy2,msg_30187769) && policy = NONE) is true.
8070.408s (user 8068.460s + system 1.948s), max rss 6902304K
PROTOCOL public-key PV AUTHENTICATION.NO_COMPROMISE.ENC_NOTSUPPORTED.FAST
RESULT event(recv_Init_IND(U,V,x_1030,sV_1031,tV_1032,tU_1033)) ==> (check_time(tV_1032,tU_1033) && event(send_Init_IND(V,U,x_1030,sV_1031,tV_1032))) is true.
RESULT event(send_and_recv_Init_RSP(Vx_3047220,Ux_3047219,x_3047221,sU_3047222,RandV_3047223,tU_3047224,tV_3047225,KMAC_UV_3047226,KENC_UV_3047227,Ux2,Vx2,x2,sU2,RandV2,tU2,KMAC_UV2,KENC_UV_3047227)) ==> (Ux_3047219 = Ux2 && Vx_3047220 = Vx2) is true.
RESULT event(send_and_recv_Init_RSP(Vx_3047220,Ux_3047219,x_3047221,sU_3047222,RandV_3047223,tU_3047224,tV_3047225,KMAC_UV_3047226,KENC_UV_3047227,Ux2,Vx2,x2,sU2,RandV2,tU2,KMAC_UV_3047226,KENC_UV2)) ==> (Ux_3047219 = Ux2 && Vx_3047220 = Vx2) is true.
RESULT inj-event(recv_Init_RSP(U,V,x_12459100,sU_12459101,RandV_12459102,tU_12459103,KMAC_UV_12459105,KENC_UV_12459106)) ==> (check_time(tU_12459103,tV_12459104) && inj-event(send_Init_RSP(V,U,x_12459100,sU_12459101,RandV_12459102,tU_12459103,tV_12459104,KMAC_UV_12459105,KENC_UV_12459106))) is true.
RESULT event(recv_Init_REQ(V,U,x_20621759,sU_20621760,tU_20621761,tV_20621762)) ==> (check_time(tU_20621761,tV_20621762) && event(send_Init_REQ(U,V,x_20621759,sU_20621760,tU_20621761))) is true.
RESULT event(recv_msg(U,V,tU_23771847,sU_23771848,randV,policy_id_23771849,policy,enc,count_23771850,msg_23771851)) ==> (policy_ok(policy_id_23771849,policy,msg_23771851) && policy_ok(policy_id_23771849,policy2,msg_23771851) && event(send_msg(V,U,tU_23771847,sU_23771848,randV,policy_id_23771849,policy2,enc,count_23771850,msg_23771851))) || (policy_ok(policy_id_23771849,policy,msg_23771851) && policy_ok(policy_id_23771849,policy2,msg_23771851) && policy = NONE) is true.
RESULT event(recv_msg(V,U,tU_23771847,sU_23771848,randV,policy_id_23771849,policy,enc,count_23771850,msg_23771851)) ==> (policy_ok(policy_id_23771849,policy,msg_23771851) && policy_ok(policy_id_23771849,policy2,msg_23771851) && event(send_msg(U,V,tU_23771847,sU_23771848,randV,policy_id_23771849,policy2,enc,count_23771850,msg_23771851))) || (policy_ok(policy_id_23771849,policy,msg_23771851) && policy_ok(policy_id_23771849,policy2,msg_23771851) && policy = NONE) is true.
7107.308s (user 7104.968s + system 2.340s), max rss 6834992K
PROTOCOL public-key PV KEY_SECRECY.NO_COMPROMISE.ENC_SUPPORTED.FAST
RESULT not attacker(secretU_KENC[]) is true.
RESULT not attacker(secretU_KMAC[]) is true.
RESULT not attacker(secretV_KENC[]) is true.
RESULT not attacker(secretV_KMAC[]) is true.
102.082s (user 101.942s + system 0.140s), max rss 661984K
PROTOCOL public-key PV KEY_SECRECY.NO_COMPROMISE.ENC_NOTSUPPORTED.FAST
RESULT not attacker(secretU_KENC[]) is true.
RESULT not attacker(secretU_KMAC[]) is true.
RESULT not attacker(secretV_KENC[]) is true.
RESULT not attacker(secretV_KMAC[]) is true.
101.062s (user 100.954s + system 0.108s), max rss 657984K
PROTOCOL public-key PV SECRECY.PFS.ENC_SUPPORTED.FAST
RESULT attacker_p1(payload_message(U,V,policy_id_1038,x_1039)) ==> policy_ok(policy_id_1038,AUTH,payload_message(U,V,policy_id_1038,x_1039)) || policy_ok(policy_id_1038,NONE,payload_message(U,V,policy_id_1038,x_1039)) cannot be proved.
RESULT attacker_p1(payload_message(V,U,policy_id_1038,x_1039)) ==> policy_ok(policy_id_1038,AUTH,payload_message(V,U,policy_id_1038,x_1039)) || policy_ok(policy_id_1038,NONE,payload_message(V,U,policy_id_1038,x_1039)) cannot be proved.
5306.040s (user 5305.424s + system 0.616s), max rss 1408112K
PROTOCOL public-key PV KEY_SECRECY.PFS.ENC_SUPPORTED.FAST
RESULT not attacker_p1(secretU_KENC[]) cannot be proved.
RESULT not attacker_p1(secretU_KMAC[]) cannot be proved.
RESULT not attacker_p1(secretV_KENC[]) cannot be proved.
RESULT not attacker_p1(secretV_KMAC[]) cannot be proved.
122.264s (user 122.188s + system 0.076s), max rss 662416K
PROTOCOL public-key PV AUTHENTICATION.COMPROMISE_U.ENC_SUPPORTED.FAST
RESULT event(recv_Init_IND(U,V,x_1030,sV_1031,tV_1032,tU_1033)) ==> (check_time(tV_1032,tU_1033) && event(send_Init_IND(V,U,x_1030,sV_1031,tV_1032))) is true.
RESULT event(send_and_recv_Init_RSP(Vx_3982505,Ux_3982504,x_3982506,sU_3982507,RandV_3982508,tU_3982509,tV_3982510,KMAC_UV_3982511,KENC_UV_3982512,Ux2,Vx2,x2,sU2,RandV2,tU2,KMAC_UV2,KENC_UV_3982512)) ==> (Ux_3982504 = Ux2 && Vx_3982505 = Vx2) is true.
RESULT event(send_and_recv_Init_RSP(Vx_3982505,Ux_3982504,x_3982506,sU_3982507,RandV_3982508,tU_3982509,tV_3982510,KMAC_UV_3982511,KENC_UV_3982512,Ux2,Vx2,x2,sU2,RandV2,tU2,KMAC_UV_3982511,KENC_UV2)) ==> (Ux_3982504 = Ux2 && Vx_3982505 = Vx2) is true.
RESULT inj-event(recv_Init_RSP(U,V,x_9319994,sU_9319995,RandV_9319996,tU_9319997,KMAC_UV_9319999,KENC_UV_9320000)) ==> (check_time(tU_9319997,tV_9319998) && inj-event(send_Init_RSP(V,U,x_9319994,sU_9319995,RandV_9319996,tU_9319997,tV_9319998,KMAC_UV_9319999,KENC_UV_9320000))) is false.
RESULT (even event(recv_Init_RSP(U,V,x_20192105,sU_20192106,RandV_20192107,tU_20192103,KMAC_UV_20192108,KENC_UV_20192109)) ==> event(send_Init_RSP(V,U,x_20192105,sU_20192106,RandV_20192107,tU_20192103,tV_20192104,KMAC_UV_20192108,KENC_UV_20192109)) is false.)
RESULT event(recv_Init_REQ(V,U,x_20201752,sU_20201753,tU_20201754,tV_20201755)) ==> (check_time(tU_20201754,tV_20201755) && event(send_Init_REQ(U,V,x_20201752,sU_20201753,tU_20201754))) cannot be proved.
RESULT (even event(recv_Init_REQ(V,U,x_24275570,sU_24275571,tU_24275568,tV_24275569)) ==> event(send_Init_REQ(U,V,x_24275570,sU_24275571,tU_24275568)) cannot be proved.)
RESULT event(recv_msg(U,V,tU_24288077,sU_24288078,randV,policy_id_24288079,policy,enc,count_24288080,msg_24288081)) ==> (policy_ok(policy_id_24288079,policy,msg_24288081) && policy_ok(policy_id_24288079,policy2,msg_24288081) && event(send_msg(V,U,tU_24288077,sU_24288078,randV,policy_id_24288079,policy2,enc,count_24288080,msg_24288081))) || (policy_ok(policy_id_24288079,policy,msg_24288081) && policy_ok(policy_id_24288079,policy2,msg_24288081) && policy = NONE) cannot be proved.
RESULT (even event(recv_msg(U,V,tU_29675157,sU_29675158,randV_29675159,policy_id_29675153,policy_29675154,enc_29675160,count_29675161,msg_29675155)) ==> event(send_msg(V,U,tU_29675157,sU_29675158,randV_29675159,policy_id_29675153,policy2_29675156,enc_29675160,count_29675161,msg_29675155)) || policy_29675154 = NONE cannot be proved.)
RESULT event(recv_msg(V,U,tU_24288077,sU_24288078,randV,policy_id_24288079,policy,enc,count_24288080,msg_24288081)) ==> (policy_ok(policy_id_24288079,policy,msg_24288081) && policy_ok(policy_id_24288079,policy2,msg_24288081) && event(send_msg(U,V,tU_24288077,sU_24288078,randV,policy_id_24288079,policy2,enc,count_24288080,msg_24288081))) || (policy_ok(policy_id_24288079,policy,msg_24288081) && policy_ok(policy_id_24288079,policy2,msg_24288081) && policy = NONE) cannot be proved.
RESULT (even event(recv_msg(V,U,tU_29711222,sU_29711223,randV_29711224,policy_id_29711218,policy_29711219,enc_29711225,count_29711226,msg_29711220)) ==> event(send_msg(U,V,tU_29711222,sU_29711223,randV_29711224,policy_id_29711218,policy2_29711221,enc_29711225,count_29711226,msg_29711220)) || policy_29711219 = NONE cannot be proved.)
8819.647s (user 8818.087s + system 1.560s), max rss 6918944K
PROTOCOL public-key PV AUTHENTICATION.COMPROMISE_V.ENC_SUPPORTED.FAST
RESULT event(recv_Init_IND(U,V,x_1030,sV_1031,tV_1032,tU_1033)) ==> (check_time(tV_1032,tU_1033) && event(send_Init_IND(V,U,x_1030,sV_1031,tV_1032))) cannot be proved.
RESULT (even event(recv_Init_IND(U,V,x_3453067,sV_3453068,tV_3453065,tU_3453066)) ==> event(send_Init_IND(V,U,x_3453067,sV_3453068,tV_3453065)) cannot be proved.)
RESULT event(send_and_recv_Init_RSP(Vx_3457606,Ux_3457605,x_3457607,sU_3457608,RandV_3457609,tU_3457610,tV_3457611,KMAC_UV_3457612,KENC_UV_3457613,Ux2,Vx2,x2,sU2,RandV2,tU2,KMAC_UV2,KENC_UV_3457613)) ==> (Ux_3457605 = Ux2 && Vx_3457606 = Vx2) is true.
RESULT event(send_and_recv_Init_RSP(Vx_3457606,Ux_3457605,x_3457607,sU_3457608,RandV_3457609,tU_3457610,tV_3457611,KMAC_UV_3457612,KENC_UV_3457613,Ux2,Vx2,x2,sU2,RandV2,tU2,KMAC_UV_3457612,KENC_UV2)) ==> (Ux_3457605 = Ux2 && Vx_3457606 = Vx2) is true.
RESULT inj-event(recv_Init_RSP(U,V,x_7645500,sU_7645501,RandV_7645502,tU_7645503,KMAC_UV_7645505,KENC_UV_7645506)) ==> (check_time(tU_7645503,tV_7645504) && inj-event(send_Init_RSP(V,U,x_7645500,sU_7645501,RandV_7645502,tU_7645503,tV_7645504,KMAC_UV_7645505,KENC_UV_7645506))) is false.
RESULT (even event(recv_Init_RSP(U,V,x_15731022,sU_15731023,RandV_15731024,tU_15731020,KMAC_UV_15731025,KENC_UV_15731026)) ==> event(send_Init_RSP(V,U,x_15731022,sU_15731023,RandV_15731024,tU_15731020,tV_15731021,KMAC_UV_15731025,KENC_UV_15731026)) is false.)
RESULT event(recv_Init_REQ(V,U,x_15740701,sU_15740702,tU_15740703,tV_15740704)) ==> (check_time(tU_15740703,tV_15740704) && event(send_Init_REQ(U,V,x_15740701,sU_15740702,tU_15740703))) is true.
RESULT event(recv_msg(U,V,tU_19269275,sU_19269276,randV,policy_id_19269277,policy,enc,count_19269278,msg_19269279)) ==> (policy_ok(policy_id_19269277,policy,msg_19269279) && policy_ok(policy_id_19269277,policy2,msg_19269279) && event(send_msg(V,U,tU_19269275,sU_19269276,randV,policy_id_19269277,policy2,enc,count_19269278,msg_19269279))) || (policy_ok(policy_id_19269277,policy,msg_19269279) && policy_ok(policy_id_19269277,policy2,msg_19269279) && policy = NONE) cannot be proved.
RESULT (even event(recv_msg(U,V,tU_24037706,sU_24037707,randV_24037708,policy_id_24037702,policy_24037703,enc_24037709,count_24037710,msg_24037704)) ==> event(send_msg(V,U,tU_24037706,sU_24037707,randV_24037708,policy_id_24037702,policy2_24037705,enc_24037709,count_24037710,msg_24037704)) || policy_24037703 = NONE cannot be proved.)
RESULT event(recv_msg(V,U,tU_19269275,sU_19269276,randV,policy_id_19269277,policy,enc,count_19269278,msg_19269279)) ==> (policy_ok(policy_id_19269277,policy,msg_19269279) && policy_ok(policy_id_19269277,policy2,msg_19269279) && event(send_msg(U,V,tU_19269275,sU_19269276,randV,policy_id_19269277,policy2,enc,count_19269278,msg_19269279))) || (policy_ok(policy_id_19269277,policy,msg_19269279) && policy_ok(policy_id_19269277,policy2,msg_19269279) && policy = NONE) cannot be proved.
RESULT (even event(recv_msg(V,U,tU_24055047,sU_24055048,randV_24055049,policy_id_24055043,policy_24055044,enc_24055050,count_24055051,msg_24055045)) ==> event(send_msg(U,V,tU_24055047,sU_24055048,randV_24055049,policy_id_24055043,policy2_24055046,enc_24055050,count_24055051,msg_24055045)) || policy_24055044 = NONE cannot be proved.)
7584.538s (user 7582.298s + system 2.240s), max rss 6903536K

PROTOCOL public-key CV SECRECY.NOREPLAY_PROT
All queries proved.
190.772s (user 190.608s + system 0.164s), max rss 1832720K
PROTOCOL public-key CV AUTHENTICATION.NOREPLAY_PROT
All queries proved.
335.321s (user 335.129s + system 0.192s), max rss 2443520K
PROTOCOL public-key CV KEY_SECRECY.NOREPLAY_PROT
All queries proved.
11.333s (user 11.293s + system 0.040s), max rss 276432K
PROTOCOL public-key CV SECRECY.REPLAY_PROT
All queries proved.
213.541s (user 213.365s + system 0.176s), max rss 1832352K
PROTOCOL public-key CV AUTHENTICATION.REPLAY_PROT
All queries proved.
222.322s (user 222.090s + system 0.232s), max rss 1796240K
PROTOCOL public-key CV KEY_SECRECY.REPLAY_PROT
All queries proved.
12.297s (user 12.281s + system 0.016s), max rss 286832K
PROTOCOL public-key CV fixed.KEY_SECRECY.REPLAY_PROT
All queries proved.
32.066s (user 32.034s + system 0.032s), max rss 291232K
PROTOCOL public-key CV fixed.SECRECY.REPLAY_PROT
All queries proved.
3305.887s (user 3305.119s + system 0.768s), max rss 4957968K
PROTOCOL public-key CV fixed.AUTHENTICATION.COMPROMISE_U.REPLAY_PROT
All queries proved.
536.834s (user 536.682s + system 0.152s), max rss 1903632K
PROTOCOL public-key CV fixed.AUTHENTICATION.COMPROMISE_V.REPLAY_PROT
All queries proved.
279.325s (user 279.173s + system 0.152s), max rss 1305904K
PROTOCOL public-key CV fixed.AUTHENTICATION.NO_COMPROMISE.REPLAY_PROT
All queries proved.
363.555s (user 363.427s + system 0.128s), max rss 1369424K