%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV236+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n025.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 16:46:12 EDT 2024 % Result : Theorem 0.55s 0.62s % Output : CNFRefutation 0.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWV236+1 : TPTP v8.2.0. Released v3.2.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n025.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 15:10:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 0.55/0.61 %------------------------------------------- % 0.55/0.61 % File :CSE---1.7 % 0.55/0.61 % Problem :theBenchmark % 0.55/0.61 % Transform :cnf % 0.55/0.61 % Format :tptp:raw % 0.55/0.61 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.61 % 0.55/0.61 % Result :Theorem 0.020000s % 0.55/0.61 % Output :CNFRefutation 0.020000s % 0.55/0.61 %------------------------------------------- % 0.55/0.62 %------------------------------------------------------------------------------ % 0.55/0.62 % File : SWV236+1 : TPTP v8.2.0. Released v3.2.0. % 0.55/0.62 % Domain : Software Verification (Security) % 0.55/0.62 % Problem : IBM's known exporter attack on the 4758 CCA API % 0.55/0.62 % Version : Especial % 0.55/0.62 % English : This is a model of the key-management commands from the IBM CCA % 0.55/0.62 % API, which controls the 4758 hardware cryptoprocessor module. The % 0.55/0.62 % conjecture represents the security of a customer's PIN. This % 0.55/0.62 % variant is IBM's own known exporter attack they gave in response % 0.55/0.62 % to the attack discovery. % 0.55/0.62 % 0.55/0.62 % Refs : [BA01] Bond & Anderson (2001), API-Level Attacks on Embedded % 0.55/0.62 % : [Ste05] Steel (2005), Deduction with XOR Constraints in Securi % 0.55/0.62 % : [Ste06] Steel (2006), Email to G. Sutcliffe % 0.55/0.62 % Source : [Ste06] % 0.55/0.62 % Names : % 0.55/0.62 % 0.55/0.62 % Status : Theorem % 0.55/0.62 % Rating : 0.17 v8.2.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.13 v7.3.0, 0.14 v7.1.0, 0.09 v7.0.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.30 v5.4.0, 0.36 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.0, 0.21 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0, 0.37 v3.3.0, 0.21 v3.2.0 % 0.55/0.62 % Syntax : Number of formulae : 28 ( 15 unt; 0 def) % 0.55/0.62 % Number of atoms : 58 ( 5 equ) % 0.55/0.62 % Maximal formula atoms : 5 ( 2 avg) % 0.55/0.62 % Number of connectives : 30 ( 0 ~; 0 |; 18 &) % 0.55/0.62 % ( 0 <=>; 12 =>; 0 <=; 0 <~>) % 0.55/0.62 % Maximal formula depth : 11 ( 4 avg) % 0.55/0.62 % Maximal term depth : 5 ( 2 avg) % 0.55/0.62 % Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty) % 0.55/0.62 % Number of functors : 13 ( 13 usr; 10 con; 0-2 aty) % 0.55/0.62 % Number of variables : 44 ( 43 !; 1 ?) % 0.55/0.62 % SPC : FOF_THM_RFO_SEQ % 0.55/0.62 % 0.55/0.62 % Comments : Have added in AC-axioms for the xor operator (*) % 0.55/0.62 %------------------------------------------------------------------------------ % 0.55/0.62 fof(xor_commutative,axiom, % 0.55/0.62 ! [X1,X2] : xor(X1,X2) = xor(X2,X1) ). % 0.55/0.62 % 0.55/0.62 fof(xor_associative,axiom, % 0.55/0.62 ! [X1,X2,X3] : xor(X1,xor(X2,X3)) = xor(xor(X1,X2),X3) ). % 0.55/0.62 % 0.55/0.62 fof(encryption_decryption_cancellation,axiom, % 0.55/0.62 ! [X1,X2] : decrypt(X1,crypt(X1,X2)) = X2 ). % 0.55/0.62 % 0.55/0.62 fof(xor_rules_1,axiom, % 0.55/0.62 ! [X1] : xor(X1,id) = X1 ). % 0.55/0.62 % 0.55/0.62 fof(xor_rules_2,axiom, % 0.55/0.62 ! [X1] : xor(X1,X1) = id ). % 0.55/0.62 % 0.55/0.62 fof(key_import,axiom, % 0.55/0.62 ! [Xkek1,Xtype1,Xk1,Xtype2,Xkek2] : % 0.55/0.62 ( ( p(crypt(xor(Xkek1,Xtype1),Xk1)) % 0.55/0.62 & p(Xtype2) % 0.55/0.62 & p(crypt(xor(km,imp),Xkek2)) ) % 0.55/0.62 => p(crypt(xor(km,Xtype2),decrypt(xor(Xkek2,Xtype2),crypt(xor(Xkek1,Xtype1),Xk1)))) ) ). % 0.55/0.62 % 0.55/0.62 fof(key_export,axiom, % 0.55/0.62 ! [Xtype,Xk1,Xkek1] : % 0.55/0.62 ( ( p(crypt(xor(km,Xtype),Xk1)) % 0.55/0.62 & p(Xtype) % 0.55/0.62 & p(crypt(xor(km,exp),Xkek1)) ) % 0.55/0.62 => p(crypt(xor(Xkek1,Xtype),Xk1)) ) ). % 0.55/0.62 % 0.55/0.62 fof(key_part_import___part_1,axiom, % 0.55/0.62 ! [Xk,Xtype] : % 0.55/0.62 ( ( p(Xk) % 0.55/0.62 & p(Xtype) ) % 0.55/0.62 => p(crypt(xor(km,xor(kp,Xtype)),Xk)) ) ). % 0.55/0.62 % 0.55/0.62 fof(key_part_import___part_2,axiom, % 0.55/0.62 ! [Xk1,Xtype,Xk2] : % 0.55/0.62 ( ( p(Xk1) % 0.55/0.62 & p(crypt(xor(km,xor(kp,Xtype)),Xk2)) % 0.55/0.62 & p(Xtype) ) % 0.55/0.62 => p(crypt(xor(km,xor(Xtype,kp)),xor(Xk1,Xk2))) ) ). % 0.55/0.62 % 0.55/0.62 fof(key_part_import___part_3,axiom, % 0.55/0.62 ! [Xk1,Xtype,Xk2] : % 0.55/0.62 ( ( p(Xk1) % 0.55/0.62 & p(crypt(xor(km,xor(Xtype,kp)),Xk2)) % 0.55/0.62 & p(Xtype) ) % 0.55/0.62 => p(crypt(xor(km,Xtype),xor(Xk2,Xk1))) ) ). % 0.55/0.62 % 0.55/0.62 fof(encrypt_data,axiom, % 0.55/0.62 ! [X1,Xk1] : % 0.55/0.62 ( ( p(X1) % 0.55/0.62 & p(crypt(xor(km,data),Xk1)) ) % 0.55/0.62 => p(crypt(Xk1,X1)) ) ). % 0.55/0.62 % 0.55/0.62 fof(decrypt_data,axiom, % 0.55/0.62 ! [X1,Xk1] : % 0.55/0.62 ( ( p(X1) % 0.55/0.62 & p(crypt(xor(km,data),Xk1)) ) % 0.55/0.62 => p(decrypt(Xk1,X1)) ) ). % 0.55/0.62 % 0.55/0.62 fof(key_translate,axiom, % 0.55/0.62 ! [Xk,Xk1,Xtype2,Xkek1,Xkek2,Xtype] : % 0.55/0.62 ( ( p(crypt(Xk,Xk1)) % 0.55/0.62 & p(Xtype2) % 0.55/0.62 & p(crypt(xor(km,imp),Xkek1)) % 0.55/0.62 & p(crypt(xor(km,exp),Xkek2)) ) % 0.55/0.62 => p(crypt(xor(Xkek2,Xtype),decrypt(xor(Xtype2,Xkek1),crypt(Xk,Xk1)))) ) ). % 0.55/0.62 % 0.55/0.62 fof(combine_with_XOR,axiom, % 0.55/0.62 ! [X1,X2] : % 0.55/0.62 ( ( p(X1) % 0.55/0.62 & p(X2) ) % 0.55/0.62 => p(xor(X1,X2)) ) ). % 0.55/0.62 % 0.55/0.62 fof(decrypt_knowledge,axiom, % 0.55/0.62 ! [X1,X2] : % 0.55/0.62 ( ( p(crypt(X1,X2)) % 0.55/0.62 & p(X1) ) % 0.55/0.62 => p(X2) ) ). % 0.55/0.62 % 0.55/0.62 fof(encrypt_knowledge,axiom, % 0.55/0.62 ! [X1,X2] : % 0.55/0.62 ( ( p(X2) % 0.55/0.62 & p(X1) ) % 0.55/0.62 => p(crypt(X1,X2)) ) ). % 0.55/0.62 % 0.55/0.62 % for the IBM attack, we know the data cv is 0 % 0.55/0.62 % 0.55/0.62 fof(data_cv_is_known_to_be_zero,axiom, % 0.55/0.62 ! [X1,X2] : % 0.55/0.62 ( p(crypt(xor(X1,data),X2)) % 0.55/0.62 => p(crypt(X1,X2)) ) ). % 0.55/0.62 % 0.55/0.62 fof(initial_knowledge_of_intruder_1,axiom, % 0.55/0.62 p(kp) ). % 0.55/0.62 % 0.55/0.62 fof(initial_knowledge_of_intruder_2,axiom, % 0.55/0.62 p(imp) ). % 0.55/0.62 % 0.55/0.62 fof(initial_knowledge_of_intruder_3,axiom, % 0.55/0.62 p(data) ). % 0.55/0.62 % 0.55/0.62 fof(initial_knowledge_of_intruder_4,axiom, % 0.55/0.62 p(id) ). % 0.55/0.62 % 0.55/0.62 fof(initial_knowledge_of_intruder_5,axiom, % 0.55/0.62 p(pin) ). % 0.55/0.62 % 0.55/0.62 fof(initial_knowledge_of_intruder_6,axiom, % 0.55/0.62 p(crypt(xor(km,pin),pp)) ). % 0.55/0.62 % 0.55/0.62 %----EURK stands for 'encrypted unknown random key' % 0.55/0.62 fof(initial_knowledge_of_intruder_7,axiom, % 0.55/0.62 p(crypt(xor(km,exp),eurk)) ). % 0.55/0.62 % 0.55/0.62 fof(initial_knowledge_of_intruder_8,axiom, % 0.55/0.62 p(crypt(xor(km,data),eurk)) ). % 0.55/0.62 % 0.55/0.62 fof(initial_knowledge_of_intruder_9,axiom, % 0.55/0.62 p(exp) ). % 0.55/0.62 % 0.55/0.62 fof(an_account_number,axiom, % 0.55/0.62 p(a) ). % 0.55/0.62 % 0.55/0.62 fof(find_known_exporter,conjecture, % 0.55/0.62 ? [X] : % 0.55/0.62 ( p(crypt(xor(km,exp),X)) % 0.55/0.62 & p(X) ) ). % 0.55/0.62 % 0.55/0.62 %------------------------------------------------------------------------------ % 0.55/0.62 %------------------------------------------- % 0.55/0.62 % Proof found % 0.55/0.62 % SZS status Theorem for theBenchmark % 0.55/0.62 % SZS output start Proof % 0.55/0.62 %ClaNum:38(EqnAxiom:10) % 0.55/0.62 %VarNum:91(SingletonVarNum:44) % 0.55/0.62 %MaxLitNum:5 % 0.55/0.62 %MaxfuncDepth:4 % 0.55/0.62 %SharedTerms:27 % 0.55/0.62 %goalClause: 29 % 0.55/0.62 [11]P1(a1) % 0.55/0.62 [12]P1(a8) % 0.55/0.62 [13]P1(a2) % 0.55/0.62 [14]P1(a9) % 0.55/0.62 [15]P1(a3) % 0.55/0.62 [16]P1(a11) % 0.55/0.62 [17]P1(a4) % 0.55/0.62 [22]P1(f5(f12(a10,a2),a7)) % 0.55/0.62 [23]P1(f5(f12(a10,a3),a7)) % 0.55/0.62 [24]P1(f5(f12(a10,a11),a13)) % 0.55/0.62 [18]E(f12(x181,a1),x181) % 0.55/0.62 [19]E(f12(x191,x191),a1) % 0.55/0.62 [20]E(f12(x201,x202),f12(x202,x201)) % 0.55/0.62 [21]E(f6(x211,f5(x211,x212)),x212) % 0.55/0.62 [25]E(f12(f12(x251,x252),x253),f12(x251,f12(x252,x253))) % 0.55/0.62 [29]~P1(x291)+~P1(f5(f12(a10,a2),x291)) % 0.55/0.62 [32]P1(f5(x321,x322))+~P1(f5(f12(x321,a3),x322)) % 0.55/0.62 [26]~P1(x262)+~P1(x261)+P1(f12(x261,x262)) % 0.55/0.62 [27]~P1(x271)+~P1(x272)+P1(f5(x271,x272)) % 0.55/0.62 [28]P1(x281)+~P1(x282)+~P1(f5(x282,x281)) % 0.55/0.62 [30]~P1(x302)+P1(f5(x301,x302))+~P1(f5(f12(a10,a3),x301)) % 0.55/0.62 [31]~P1(x312)+P1(f6(x311,x312))+~P1(f5(f12(a10,a3),x311)) % 0.55/0.62 [33]~P1(x331)+~P1(x332)+P1(f5(f12(a10,f12(a9,x331)),x332)) % 0.55/0.62 [34]~P1(x342)+P1(f5(f12(x341,x342),x343))+~P1(f5(f12(a10,a2),x341))+~P1(f5(f12(a10,x342),x343)) % 0.55/0.62 [35]~P1(x351)+~P1(x353)+P1(f5(f12(a10,x351),f12(x352,x353)))+~P1(f5(f12(a10,f12(x351,a9)),x352)) % 0.55/0.62 [36]~P1(x361)+~P1(x362)+P1(f5(f12(a10,f12(x361,a9)),f12(x362,x363)))+~P1(f5(f12(a10,f12(a9,x361)),x363)) % 0.55/0.62 [38]~P1(x381)+~P1(f5(f12(x383,x384),x385))+~P1(f5(f12(a10,a8),x382))+P1(f5(f12(a10,x381),f6(f12(x382,x381),f5(f12(x383,x384),x385)))) % 0.55/0.62 [37]~P1(x373)+~P1(f5(x375,x376))+~P1(f5(f12(a10,a2),x371))+~P1(f5(f12(a10,a8),x374))+P1(f5(f12(x371,x372),f6(f12(x373,x374),f5(x375,x376)))) % 0.55/0.62 %EqnAxiom % 0.55/0.62 [1]E(x11,x11) % 0.55/0.62 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.62 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.62 [4]~E(x41,x42)+E(f12(x41,x43),f12(x42,x43)) % 0.55/0.62 [5]~E(x51,x52)+E(f12(x53,x51),f12(x53,x52)) % 0.55/0.62 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63)) % 0.55/0.62 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72)) % 0.55/0.62 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83)) % 0.55/0.62 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92)) % 0.55/0.62 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 0.55/0.62 % 0.55/0.62 %------------------------------------------- % 0.55/0.62 cnf(39,plain, % 0.55/0.62 (~P1(a7)), % 0.55/0.62 inference(scs_inference,[],[22,29])). % 0.55/0.62 cnf(51,plain, % 0.55/0.62 (E(f12(x511,a1),x511)), % 0.55/0.62 inference(rename_variables,[],[18])). % 0.55/0.62 cnf(52,plain, % 0.55/0.62 (E(f12(a1,x521),x521)), % 0.55/0.62 inference(scs_inference,[],[18,51,22,23,20,29,32,2,28,30,31,10,3])). % 0.55/0.62 cnf(55,plain, % 0.55/0.62 (P1(f5(f12(a7,a2),a7))), % 0.55/0.62 inference(scs_inference,[],[18,51,13,22,23,20,29,32,2,28,30,31,10,3,34])). % 0.55/0.62 cnf(62,plain, % 0.55/0.62 (E(f12(f12(a1,x621),a1),x621)), % 0.55/0.62 inference(scs_inference,[],[39,55,18,52,2,28,3])). % 0.55/0.62 cnf(68,plain, % 0.55/0.62 (E(x681,f12(f12(a1,x681),a1))), % 0.55/0.62 inference(scs_inference,[],[62,2])). % 0.55/0.62 cnf(71,plain, % 0.55/0.62 (E(f12(f12(f12(a1,x711),a1),a1),x711)), % 0.55/0.62 inference(scs_inference,[],[39,18,23,62,2,28,3])). % 0.55/0.62 cnf(75,plain, % 0.55/0.62 (P1(f5(f12(a7,a3),a7))), % 0.55/0.62 inference(scs_inference,[],[39,15,18,23,22,62,2,28,3,10,34])). % 0.55/0.62 cnf(77,plain, % 0.55/0.62 (P1(f5(a7,a7))), % 0.55/0.62 inference(scs_inference,[],[39,15,18,23,22,62,2,28,3,10,34,32])). % 0.55/0.62 cnf(81,plain, % 0.55/0.62 (E(x811,f12(f12(f12(a1,x811),a1),a1))), % 0.55/0.62 inference(scs_inference,[],[71,2])). % 0.55/0.62 cnf(84,plain, % 0.55/0.62 (E(f12(x841,a1),f12(f12(a1,x841),a1))), % 0.55/0.62 inference(scs_inference,[],[39,75,18,68,71,2,28,3])). % 0.55/0.62 cnf(89,plain, % 0.55/0.62 (E(f12(x891,a1),f12(f12(f12(a1,x891),a1),a1))), % 0.55/0.62 inference(scs_inference,[],[18,81,84,2,3])). % 0.55/0.62 cnf(95,plain, % 0.55/0.62 (E(f12(f12(f12(a1,x951),a1),a1),f12(x951,a1))), % 0.55/0.62 inference(scs_inference,[],[89,2])). % 0.55/0.62 cnf(96,plain, % 0.55/0.62 (E(f12(f12(x961,a1),a1),f12(f12(f12(a1,x961),a1),a1))), % 0.55/0.62 inference(scs_inference,[],[18,89,2,3])). % 0.55/0.62 cnf(107,plain, % 0.55/0.62 ($false), % 0.55/0.62 inference(scs_inference,[],[39,23,77,18,95,96,21,2,3,10,31]), % 0.55/0.62 ['proof']). % 0.60/0.63 % SZS output end Proof % 0.60/0.63 % Total time :0.020000s %------------------------------------------------------------------------------