%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWW951+1 : TPTP v8.2.0. Released v7.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 18:10:36 EDT 2024 % Result : Theorem 9.56s 9.67s % Output : CNFRefutation 9.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SWW951+1 : TPTP v8.2.0. Released v7.4.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n022.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Jun 19 07:45:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.60/0.64 start to proof:theBenchmark % 9.56/9.65 %------------------------------------------- % 9.56/9.65 % File :CSE---1.7 % 9.56/9.65 % Problem :theBenchmark % 9.56/9.65 % Transform :cnf % 9.56/9.65 % Format :tptp:raw % 9.56/9.65 % Command :java -jar mcs_scs.jar %d %s % 9.56/9.66 % 9.56/9.66 % Result :Theorem 8.940000s % 9.56/9.66 % Output :CNFRefutation 8.940000s % 9.56/9.66 %------------------------------------------- % 9.56/9.66 %-------------------------------------------------------------------------- % 9.56/9.66 % File : SWW951+1 : TPTP v8.2.0. Released v7.4.0. % 9.56/9.66 % Domain : Software Verification % 9.56/9.66 % Problem : Attack on OTYT06 protocol % 9.56/9.66 % Version : [LT19] axioms : Especial. % 9.56/9.66 % English : Attack demonstrates violation of aliveness property of tag % 9.56/9.66 % : guaranteed to reader. % 9.56/9.66 % 9.56/9.66 % Refs : [BO97] Bull & Otway (1997), The Authentication Protocol % 9.56/9.66 % : [RS98] Ryan & Schneider (1998), An Attack on a Recursive Auth % 9.56/9.66 % : [LT19] Li & Tiu (2019), Combining ProVerif and Automated Theo % 9.56/9.66 % : [Li20] Li (2020), Email to Geoff Sutcliffe % 9.56/9.66 % Source : [Li20] % 9.56/9.66 % Names : OTYT06-reader-auth.p [LT20] % 9.56/9.66 % 9.56/9.66 % Status : Theorem % 9.56/9.66 % Rating : 0.17 v7.5.0, 0.19 v7.4.0 % 9.56/9.66 % Syntax : Number of formulae : 66 ( 52 unt; 0 def) % 9.56/9.66 % Number of atoms : 84 ( 40 equ) % 9.56/9.66 % Maximal formula atoms : 3 ( 1 avg) % 9.56/9.66 % Number of connectives : 54 ( 36 ~; 0 |; 4 &) % 9.56/9.66 % ( 0 <=>; 14 =>; 0 <=; 0 <~>) % 9.56/9.66 % Maximal formula depth : 5 ( 2 avg) % 9.56/9.66 % Maximal term depth : 4 ( 1 avg) % 9.56/9.66 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 9.56/9.66 % Number of functors : 18 ( 18 usr; 11 con; 0-2 aty) % 9.56/9.66 % Number of variables : 27 ( 27 !; 0 ?) % 9.56/9.66 % SPC : FOF_THM_RFO_SEQ % 9.56/9.66 % 9.56/9.66 % Comments : Generated by a modified version of ProVerif used in the % 9.56/9.66 % ProVerif-ATP project [LT19]. % 9.56/9.66 %-------------------------------------------------------------------------- % 9.56/9.66 fof(ax0,axiom, % 9.56/9.66 constr_CONST_0x30 != constr_CONST_1 ). % 9.56/9.66 % 9.56/9.66 fof(ax1,axiom, % 9.56/9.66 constr_CONST_0x30 != constr_CONST_2 ). % 9.56/9.66 % 9.56/9.66 fof(ax2,axiom, % 9.56/9.66 constr_CONST_0x30 != constr_CONST_3 ). % 9.56/9.66 % 9.56/9.66 fof(ax3,axiom, % 9.56/9.66 constr_CONST_0x30 != constr_CONST_4 ). % 9.56/9.66 % 9.56/9.66 fof(ax4,axiom, % 9.56/9.66 constr_CONST_0x30 != constr_ZERO ). % 9.56/9.66 % 9.56/9.66 fof(ax5,axiom, % 9.56/9.66 constr_CONST_0x30 != name_c ). % 9.56/9.66 % 9.56/9.66 fof(ax6,axiom, % 9.56/9.66 constr_CONST_0x30 != name_k ). % 9.56/9.66 % 9.56/9.66 fof(ax7,axiom, % 9.56/9.66 constr_CONST_0x30 != name_objective ). % 9.56/9.66 % 9.56/9.66 fof(ax8,axiom, % 9.56/9.66 constr_CONST_1 != constr_CONST_2 ). % 9.56/9.66 % 9.56/9.66 fof(ax9,axiom, % 9.56/9.66 constr_CONST_1 != constr_CONST_3 ). % 9.56/9.66 % 9.56/9.66 fof(ax10,axiom, % 9.56/9.66 constr_CONST_1 != constr_CONST_4 ). % 9.56/9.66 % 9.56/9.66 fof(ax11,axiom, % 9.56/9.66 constr_CONST_1 != constr_ZERO ). % 9.56/9.66 % 9.56/9.66 fof(ax12,axiom, % 9.56/9.66 constr_CONST_1 != name_c ). % 9.56/9.66 % 9.56/9.66 fof(ax13,axiom, % 9.56/9.66 constr_CONST_1 != name_k ). % 9.56/9.66 % 9.56/9.66 fof(ax14,axiom, % 9.56/9.66 constr_CONST_1 != name_objective ). % 9.56/9.66 % 9.56/9.66 fof(ax15,axiom, % 9.56/9.66 constr_CONST_2 != constr_CONST_3 ). % 9.56/9.66 % 9.56/9.66 fof(ax16,axiom, % 9.56/9.66 constr_CONST_2 != constr_CONST_4 ). % 9.56/9.66 % 9.56/9.66 fof(ax17,axiom, % 9.56/9.66 constr_CONST_2 != constr_ZERO ). % 9.56/9.66 % 9.56/9.66 fof(ax18,axiom, % 9.56/9.66 constr_CONST_2 != name_c ). % 9.56/9.66 % 9.56/9.66 fof(ax19,axiom, % 9.56/9.66 constr_CONST_2 != name_k ). % 9.56/9.66 % 9.56/9.66 fof(ax20,axiom, % 9.56/9.66 constr_CONST_2 != name_objective ). % 9.56/9.66 % 9.56/9.66 fof(ax21,axiom, % 9.56/9.66 constr_CONST_3 != constr_CONST_4 ). % 9.56/9.66 % 9.56/9.66 fof(ax22,axiom, % 9.56/9.66 constr_CONST_3 != constr_ZERO ). % 9.56/9.66 % 9.56/9.66 fof(ax23,axiom, % 9.56/9.67 constr_CONST_3 != name_c ). % 9.56/9.67 % 9.56/9.67 fof(ax24,axiom, % 9.56/9.67 constr_CONST_3 != name_k ). % 9.56/9.67 % 9.56/9.67 fof(ax25,axiom, % 9.56/9.67 constr_CONST_3 != name_objective ). % 9.56/9.67 % 9.56/9.67 fof(ax26,axiom, % 9.56/9.67 constr_CONST_4 != constr_ZERO ). % 9.56/9.67 % 9.56/9.67 fof(ax27,axiom, % 9.56/9.67 constr_CONST_4 != name_c ). % 9.56/9.67 % 9.56/9.67 fof(ax28,axiom, % 9.56/9.67 constr_CONST_4 != name_k ). % 9.56/9.67 % 9.56/9.67 fof(ax29,axiom, % 9.56/9.67 constr_CONST_4 != name_objective ). % 9.56/9.67 % 9.56/9.67 fof(ax30,axiom, % 9.56/9.67 constr_ZERO != name_c ). % 9.56/9.67 % 9.56/9.67 fof(ax31,axiom, % 9.56/9.67 constr_ZERO != name_k ). % 9.56/9.67 % 9.56/9.67 fof(ax32,axiom, % 9.56/9.67 constr_ZERO != name_objective ). % 9.56/9.67 % 9.56/9.67 fof(ax33,axiom, % 9.56/9.67 name_c != name_k ). % 9.56/9.67 % 9.56/9.67 fof(ax34,axiom, % 9.56/9.67 name_c != name_objective ). % 9.56/9.67 % 9.56/9.67 fof(ax35,axiom, % 9.56/9.67 name_k != name_objective ). % 9.56/9.67 % 9.56/9.67 fof(ax36,axiom, % 9.56/9.67 ! [VAR_X_10X30] : constr_xor(VAR_X_10X30,VAR_X_10X30) = constr_ZERO ). % 9.56/9.67 % 9.56/9.67 fof(ax37,axiom, % 9.56/9.67 ! [VAR_X_9] : constr_xor(VAR_X_9,constr_ZERO) = VAR_X_9 ). % 9.56/9.67 % 9.56/9.67 fof(ax38,axiom, % 9.56/9.67 ! [VAR_X_7,VAR_Y_8] : constr_xor(VAR_X_7,VAR_Y_8) = constr_xor(VAR_Y_8,VAR_X_7) ). % 9.56/9.67 % 9.56/9.67 fof(ax39,axiom, % 9.56/9.67 ! [VAR_X_0X30,VAR_Y_0X30,VAR_Z_0X30] : constr_xor(VAR_X_0X30,constr_xor(VAR_Y_0X30,VAR_Z_0X30)) = constr_xor(constr_xor(VAR_X_0X30,VAR_Y_0X30),VAR_Z_0X30) ). % 9.56/9.67 % 9.56/9.67 fof(ax40,axiom, % 9.56/9.67 ! [VAR_V_26,VAR_V_27] : % 9.56/9.67 ( ( pred_attacker(VAR_V_26) % 9.56/9.67 & pred_attacker(VAR_V_27) ) % 9.56/9.67 => pred_attacker(constr_xor(VAR_V_26,VAR_V_27)) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax41,axiom, % 9.56/9.67 pred_attacker(tuple_true) ). % 9.56/9.67 % 9.56/9.67 fof(ax42,axiom, % 9.56/9.67 ! [VAR_V_30X30] : % 9.56/9.67 ( pred_attacker(VAR_V_30X30) % 9.56/9.67 => pred_attacker(constr_h(VAR_V_30X30)) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax43,axiom, % 9.56/9.67 pred_attacker(tuple_false) ). % 9.56/9.67 % 9.56/9.67 fof(ax44,axiom, % 9.56/9.67 pred_attacker(constr_ZERO) ). % 9.56/9.67 % 9.56/9.67 fof(ax45,axiom, % 9.56/9.67 ! [VAR_V_32] : % 9.56/9.67 ( pred_attacker(VAR_V_32) % 9.56/9.67 => pred_attacker(tuple_T_out_4(VAR_V_32)) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax46,axiom, % 9.56/9.67 ! [VAR_V_35] : % 9.56/9.67 ( pred_attacker(tuple_T_out_4(VAR_V_35)) % 9.56/9.67 => pred_attacker(VAR_V_35) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax47,axiom, % 9.56/9.67 ! [VAR_V_38] : % 9.56/9.67 ( pred_attacker(VAR_V_38) % 9.56/9.67 => pred_attacker(tuple_T_out_2(VAR_V_38)) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax48,axiom, % 9.56/9.67 ! [VAR_V_41] : % 9.56/9.67 ( pred_attacker(tuple_T_out_2(VAR_V_41)) % 9.56/9.67 => pred_attacker(VAR_V_41) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax49,axiom, % 9.56/9.67 ! [VAR_V_44] : % 9.56/9.67 ( pred_attacker(VAR_V_44) % 9.56/9.67 => pred_attacker(tuple_T_in_3(VAR_V_44)) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax50,axiom, % 9.56/9.67 ! [VAR_V_47] : % 9.56/9.67 ( pred_attacker(tuple_T_in_3(VAR_V_47)) % 9.56/9.67 => pred_attacker(VAR_V_47) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax51,axiom, % 9.56/9.67 ! [VAR_V_50X30] : % 9.56/9.67 ( pred_attacker(VAR_V_50X30) % 9.56/9.67 => pred_attacker(tuple_T_in_1(VAR_V_50X30)) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax52,axiom, % 9.56/9.67 ! [VAR_V_53] : % 9.56/9.67 ( pred_attacker(tuple_T_in_1(VAR_V_53)) % 9.56/9.67 => pred_attacker(VAR_V_53) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax53,axiom, % 9.56/9.67 pred_attacker(constr_CONST_4) ). % 9.56/9.67 % 9.56/9.67 fof(ax54,axiom, % 9.56/9.67 pred_attacker(constr_CONST_3) ). % 9.56/9.67 % 9.56/9.67 fof(ax55,axiom, % 9.56/9.67 pred_attacker(constr_CONST_2) ). % 9.56/9.67 % 9.56/9.67 fof(ax56,axiom, % 9.56/9.67 pred_attacker(constr_CONST_1) ). % 9.56/9.67 % 9.56/9.67 fof(ax57,axiom, % 9.56/9.67 pred_attacker(constr_CONST_0x30) ). % 9.56/9.67 % 9.56/9.67 fof(ax58,axiom, % 9.56/9.67 ! [VAR_V_59,VAR_V_60X30] : % 9.56/9.67 ( ( pred_mess(VAR_V_60X30,VAR_V_59) % 9.56/9.67 & pred_attacker(VAR_V_60X30) ) % 9.56/9.67 => pred_attacker(VAR_V_59) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax59,axiom, % 9.56/9.67 ! [VAR_V_61,VAR_V_62] : % 9.56/9.67 ( ( pred_attacker(VAR_V_62) % 9.56/9.67 & pred_attacker(VAR_V_61) ) % 9.56/9.67 => pred_mess(VAR_V_62,VAR_V_61) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax60,axiom, % 9.56/9.67 pred_attacker(name_c) ). % 9.56/9.67 % 9.56/9.67 fof(ax61,axiom, % 9.56/9.67 ! [VAR_V_64] : pred_equal(VAR_V_64,VAR_V_64) ). % 9.56/9.67 % 9.56/9.67 fof(ax62,axiom, % 9.56/9.67 ! [VAR_V_65] : pred_attacker(name_new0x2Dname(VAR_V_65)) ). % 9.56/9.67 % 9.56/9.67 fof(ax63,axiom, % 9.56/9.67 ! [VAR_R1_85] : % 9.56/9.67 ( pred_attacker(tuple_T_in_1(VAR_R1_85)) % 9.56/9.67 => pred_attacker(tuple_T_out_2(constr_h(constr_xor(name_k,VAR_R1_85)))) ) ). % 9.56/9.67 % 9.56/9.67 fof(ax64,axiom, % 9.56/9.67 ! [VAR_K_XOR_K1_10X305,VAR_R1_10X306] : % 9.56/9.67 ( ( pred_attacker(tuple_T_in_3(VAR_K_XOR_K1_10X305)) % 9.56/9.67 & pred_attacker(tuple_T_in_1(VAR_R1_10X306)) ) % 9.56/9.67 => pred_attacker(tuple_T_out_4(name_objective)) ) ). % 9.56/9.67 % 9.56/9.67 fof(co0,conjecture, % 9.56/9.67 pred_attacker(name_objective) ). % 9.56/9.67 % 9.56/9.67 %-------------------------------------------------------------------------- % 9.56/9.67 %------------------------------------------- % 9.56/9.67 % Proof found % 9.56/9.67 % SZS status Theorem for theBenchmark % 9.56/9.67 % SZS output start Proof % 9.56/9.67 %ClaNum:82(EqnAxiom:16) % 9.56/9.67 %VarNum:51(SingletonVarNum:27) % 9.56/9.67 %MaxLitNum:3 % 9.56/9.67 %MaxfuncDepth:3 % 9.56/9.67 %SharedTerms:59 % 9.56/9.67 %goalClause: 68 % 9.56/9.67 %singleGoalClaCount:1 % 9.56/9.67 [17]P1(a1) % 9.56/9.67 [18]P1(a2) % 9.56/9.67 [19]P1(a3) % 9.56/9.67 [20]P1(a4) % 9.56/9.67 [21]P1(a5) % 9.56/9.67 [22]P1(a6) % 9.56/9.67 [23]P1(a7) % 9.56/9.67 [24]P1(a10) % 9.56/9.67 [25]P1(a11) % 9.56/9.67 [32]~E(a2,a1) % 9.56/9.67 [33]~E(a3,a1) % 9.56/9.67 [34]~E(a3,a2) % 9.56/9.67 [35]~E(a4,a1) % 9.56/9.67 [36]~E(a4,a2) % 9.56/9.67 [37]~E(a4,a3) % 9.56/9.67 [38]~E(a5,a1) % 9.56/9.67 [39]~E(a5,a2) % 9.56/9.67 [40]~E(a5,a3) % 9.56/9.67 [41]~E(a5,a4) % 9.56/9.67 [42]~E(a1,a6) % 9.56/9.67 [43]~E(a2,a6) % 9.56/9.67 [44]~E(a3,a6) % 9.56/9.67 [45]~E(a4,a6) % 9.56/9.67 [46]~E(a5,a6) % 9.56/9.67 [47]~E(a7,a1) % 9.56/9.67 [48]~E(a7,a2) % 9.56/9.67 [49]~E(a7,a3) % 9.56/9.67 [50]~E(a7,a4) % 9.56/9.67 [51]~E(a7,a5) % 9.56/9.67 [52]~E(a7,a6) % 9.56/9.67 [53]~E(a13,a1) % 9.56/9.67 [54]~E(a13,a2) % 9.56/9.67 [55]~E(a13,a3) % 9.56/9.67 [56]~E(a13,a4) % 9.56/9.67 [57]~E(a13,a5) % 9.56/9.67 [58]~E(a13,a6) % 9.56/9.67 [59]~E(a13,a7) % 9.56/9.67 [60]~E(a14,a1) % 9.56/9.67 [61]~E(a14,a2) % 9.56/9.67 [62]~E(a14,a3) % 9.56/9.67 [63]~E(a14,a4) % 9.56/9.67 [64]~E(a14,a5) % 9.56/9.67 [65]~E(a14,a6) % 9.56/9.67 [66]~E(a14,a7) % 9.56/9.67 [67]~E(a14,a13) % 9.56/9.67 [68]~P1(a14) % 9.56/9.67 [29]P2(x291,x291) % 9.56/9.67 [26]P1(f12(x261)) % 9.56/9.67 [27]E(f8(x271,a6),x271) % 9.56/9.67 [28]E(f8(x281,x281),a6) % 9.56/9.67 [30]E(f8(x301,x302),f8(x302,x301)) % 9.56/9.67 [31]E(f8(f8(x311,x312),x313),f8(x311,f8(x312,x313))) % 9.56/9.67 [69]~P1(x691)+P1(f9(x691)) % 9.56/9.67 [70]~P1(x701)+P1(f15(x701)) % 9.56/9.67 [71]~P1(x711)+P1(f16(x711)) % 9.56/9.67 [72]~P1(x721)+P1(f17(x721)) % 9.56/9.67 [73]~P1(x731)+P1(f18(x731)) % 9.56/9.67 [74]P1(x741)+~P1(f15(x741)) % 9.56/9.67 [75]P1(x751)+~P1(f16(x751)) % 9.56/9.67 [76]P1(x761)+~P1(f17(x761)) % 9.56/9.67 [77]P1(x771)+~P1(f18(x771)) % 9.56/9.67 [82]~P1(f18(x821))+P1(f16(f9(f8(a13,x821)))) % 9.56/9.67 [78]~P1(x782)+~P1(x781)+P3(x781,x782) % 9.56/9.67 [79]~P3(x792,x791)+P1(x791)+~P1(x792) % 9.56/9.67 [80]~P1(f17(x801))+~P1(f18(x802))+P1(f15(a14)) % 9.56/9.67 [81]~P1(x812)+~P1(x811)+P1(f8(x811,x812)) % 9.56/9.67 %EqnAxiom % 9.56/9.67 [1]E(x11,x11) % 9.56/9.67 [2]E(x22,x21)+~E(x21,x22) % 9.56/9.67 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 9.56/9.67 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 9.56/9.67 [5]~E(x51,x52)+E(f8(x51,x53),f8(x52,x53)) % 9.56/9.67 [6]~E(x61,x62)+E(f8(x63,x61),f8(x63,x62)) % 9.56/9.67 [7]~E(x71,x72)+E(f18(x71),f18(x72)) % 9.56/9.67 [8]~E(x81,x82)+E(f16(x81),f16(x82)) % 9.56/9.67 [9]~E(x91,x92)+E(f9(x91),f9(x92)) % 9.56/9.67 [10]~E(x101,x102)+E(f17(x101),f17(x102)) % 9.56/9.67 [11]~E(x111,x112)+E(f15(x111),f15(x112)) % 9.56/9.67 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 9.56/9.67 [13]P3(x132,x133)+~E(x131,x132)+~P3(x131,x133) % 9.56/9.67 [14]P3(x143,x142)+~E(x141,x142)+~P3(x143,x141) % 9.56/9.67 [15]P2(x152,x153)+~E(x151,x152)+~P2(x151,x153) % 9.56/9.67 [16]P2(x163,x162)+~E(x161,x162)+~P2(x163,x161) % 9.56/9.67 % 9.56/9.67 %------------------------------------------- % 9.56/9.67 cnf(1849,plain, % 9.56/9.67 (~P1(f18(x18491))+P1(f15(a14))), % 9.56/9.67 inference(scs_inference,[],[17,80,72])). % 9.56/9.67 cnf(1988,plain, % 9.56/9.67 (P1(f15(a14))), % 9.56/9.67 inference(scs_inference,[],[18,1849,73])). % 9.56/9.67 cnf(1989,plain, % 9.56/9.67 ($false), % 9.56/9.67 inference(scs_inference,[],[68,1988,74]), % 9.56/9.67 ['proof']). % 9.56/9.67 % SZS output end Proof % 9.56/9.68 % Total time :8.940000s %------------------------------------------------------------------------------