TPTP Problem File: SWX241_1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX241_1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Find a security leak in a faulty security type system
% Version : Especial.
% English :
% Refs : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source : [CST26]
% Names : Sec_prop.p [CST26]
% Status : Theorem
% Rating : 0.74 v9.3.0
% Syntax : Number of formulae : 65 ( 49 unt; 0 def)
% Number of atoms : 88 ( 53 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 55 ( 32 ~; 3 |; 2 &)
% ( 9 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 0 prp; 1-2 aty)
% Number of functors : 36 ( 36 usr; 7 con; 0-3 aty)
% Number of variables : 140 ( 138 !; 2 ?)
% SPC : FOF_THM_RFO_SEQ
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [X,X2] : head(cons(X,X2)) = X ).
fof(axiom_002,axiom,
! [X,X2] : tail(cons(X,X2)) = X2 ).
fof(axiom_003,axiom,
! [X,X2] : nil != cons(X,X2) ).
fof(axiom_004,axiom,
! [X] : proj1Suc(suc(X)) = X ).
fof(axiom_005,axiom,
! [X] : zero != suc(X) ).
fof(axiom_006,axiom,
! [X] : proj1High(high(X)) = X ).
fof(axiom_007,axiom,
! [X] : proj1Low(low(X)) = X ).
fof(axiom_008,axiom,
! [X,X2] : high(X) != low(X2) ).
fof(axiom_009,axiom,
! [X,X2] : proj1Nand(nand(X,X2)) = X ).
fof(axiom_010,axiom,
! [X,X2] : proj2Nand(nand(X,X2)) = X2 ).
fof(axiom_011,axiom,
! [X] : proj1Var(var(X)) = X ).
fof(axiom_012,axiom,
! [X,X2] : nand(X,X2) != tT ).
fof(axiom_013,axiom,
! [X,X2] : nand(X,X2) != fF ).
fof(axiom_014,axiom,
! [X,X2,X3] : nand(X,X2) != var(X3) ).
fof(axiom_015,axiom,
tT != fF ).
fof(axiom_016,axiom,
! [X] : tT != var(X) ).
fof(axiom_017,axiom,
! [X] : fF != var(X) ).
fof(axiom_018,axiom,
! [X,X2] : proj1Assign(assign(X,X2)) = X ).
fof(axiom_019,axiom,
! [X,X2] : proj2Assign(assign(X,X2)) = X2 ).
fof(axiom_020,axiom,
! [X,X2] : proj1Seq(seq(X,X2)) = X ).
fof(axiom_021,axiom,
! [X,X2] : proj2Seq(seq(X,X2)) = X2 ).
fof(axiom_022,axiom,
! [X,X2,X3] : proj1IfThenElse(ifThenElse(X,X2,X3)) = X ).
fof(axiom_023,axiom,
! [X,X2,X3] : proj2IfThenElse(ifThenElse(X,X2,X3)) = X2 ).
fof(axiom_024,axiom,
! [X,X2,X3] : proj3IfThenElse(ifThenElse(X,X2,X3)) = X3 ).
fof(axiom_025,axiom,
! [X,X2] : proj1While(while(X,X2)) = X ).
fof(axiom_026,axiom,
! [X,X2] : proj2While(while(X,X2)) = X2 ).
fof(axiom_027,axiom,
! [X,X2] : skip != assign(X,X2) ).
fof(axiom_028,axiom,
! [X,X2] : skip != seq(X,X2) ).
fof(axiom_029,axiom,
! [X,X2,X3] : skip != ifThenElse(X,X2,X3) ).
fof(axiom_030,axiom,
! [X,X2] : skip != while(X,X2) ).
fof(axiom_031,axiom,
! [X,X2,X3,X4] : assign(X,X2) != seq(X3,X4) ).
fof(axiom_032,axiom,
! [X,X2,X3,X4,X5] : assign(X,X2) != ifThenElse(X3,X4,X5) ).
fof(axiom_033,axiom,
! [X,X2,X3,X4] : assign(X,X2) != while(X3,X4) ).
fof(axiom_034,axiom,
! [X,X2,X3,X4,X5] : seq(X,X2) != ifThenElse(X3,X4,X5) ).
fof(axiom_035,axiom,
! [X,X2,X3,X4] : seq(X,X2) != while(X3,X4) ).
fof(axiom_036,axiom,
! [X,X2,X3,X4,X5] : ifThenElse(X,X2,X3) != while(X4,X5) ).
fof(axiom_037,axiom,
! [X] :
( X != nand(proj1Nand(X),proj2Nand(X))
=> ( X != var(proj1Var(X))
=> ~ secret(X) ) ) ).
fof(axiom_038,axiom,
! [A,B] :
( secret(nand(A,B))
<=> ( secret(A)
| secret(B) ) ) ).
fof(axiom_039,axiom,
! [Z] : secret(var(high(Z))) ).
fof(axiom_040,axiom,
! [X2] : ~ secret(var(low(X2))) ).
fof(axiom_041,axiom,
typeCorrect(skip) ).
fof(axiom_042,axiom,
! [E,Z] : typeCorrect(assign(high(Z),E)) ).
fof(axiom_043,axiom,
! [E,X2] :
( typeCorrect(assign(low(X2),E))
<=> ~ secret(E) ) ).
fof(axiom_044,axiom,
! [P,Q] :
( typeCorrect(seq(P,Q))
<=> ( typeCorrect(P)
& typeCorrect(Q) ) ) ).
fof(axiom_045,axiom,
! [C,R,Q2] :
( typeCorrect(ifThenElse(C,R,Q2))
<=> ( typeCorrect(R)
& typeCorrect(Q2) ) ) ).
fof(axiom_046,axiom,
! [E2,P2] :
( typeCorrect(while(E2,P2))
<=> typeCorrect(P2) ) ).
fof(axiom_047,axiom,
l = low(zero) ).
fof(axiom_048,axiom,
h = high(zero) ).
fof(axiom_049,axiom,
! [X] : ~ elem(X,nil) ).
fof(axiom_050,axiom,
! [X,Z,Xs] :
( elem(X,cons(Z,Xs))
<=> ( Z = X
| elem(X,Xs) ) ) ).
fof(axiom_051,axiom,
! [X,A,B] :
( eval(X,nand(A,B))
<=> ( ~ eval(X,A)
| ~ eval(X,B) ) ) ).
fof(axiom_052,axiom,
! [X] : eval(X,tT) ).
fof(axiom_053,axiom,
! [X] : ~ eval(X,fF) ).
fof(axiom_054,axiom,
! [X,Z] :
( eval(X,var(Z))
<=> elem(Z,X) ) ).
fof(axiom_055,axiom,
! [X] : del(X,nil) = nil ).
fof(axiom_056,axiom,
! [X,Z,Ys] :
( X = Z
=> del(X,cons(Z,Ys)) = del(X,Ys) ) ).
fof(axiom_057,axiom,
! [X,Z,Ys] :
( X != Z
=> del(X,cons(Z,Ys)) = cons(Z,del(X,Ys)) ) ).
fof(axiom_058,axiom,
! [X] : run(X,skip) = X ).
fof(axiom_059,axiom,
! [X,Z,E] :
( eval(X,E)
=> run(X,assign(Z,E)) = cons(Z,X) ) ).
fof(axiom_060,axiom,
! [X,Z,E] :
( ~ eval(X,E)
=> run(X,assign(Z,E)) = del(Z,X) ) ).
fof(axiom_061,axiom,
! [X,P,Q] : run(X,seq(P,Q)) = run(run(X,P),Q) ).
fof(axiom_062,axiom,
! [X,E2,R,Q2] :
( eval(X,E2)
=> run(X,ifThenElse(E2,R,Q2)) = run(X,R) ) ).
fof(axiom_063,axiom,
! [X,E2,R,Q2] :
( ~ eval(X,E2)
=> run(X,ifThenElse(E2,R,Q2)) = run(X,Q2) ) ).
fof(axiom_064,axiom,
! [X,E3,P2] : run(X,while(E3,P2)) = run(X,ifThenElse(E3,seq(P2,while(E3,P2)),skip)) ).
fof(goal_065,conjecture,
? [P,S] :
~ ( typeCorrect(P)
=> ( elem(l,run(S,P))
<=> elem(l,run(cons(h,S),P)) ) ) ).
%------------------------------------------------------------------------------