TPTP Problem File: SWX216+1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX216+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 : Sec2_prop.p [CST26]
% Status : Theorem
% Rating : 1.00 v9.3.0
% Syntax : Number of formulae : 87 ( 63 unt; 2 typ; 0 def)
% Number of atoms : 333 ( 80 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 88 ( 49 ~; 6 |; 4 &)
% ( 11 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 232 ( 214 fml; 18 var)
% Number of types : 2 ( 0 usr)
% Number of type conns : 4 ( 2 >; 2 *; 0 +; 0 <<)
% Number of predicates : 49 ( 46 usr; 10 prp; 0-3 aty)
% Number of functors : 1 ( 1 usr; 0 con; 2-2 aty)
% Number of variables : 202 ( 200 !; 2 ?; 9 :)
% SPC : TX0_THM_EQU_NAR
% Comments :
%------------------------------------------------------------------------------
tff(type_001,type,
pair2: ( $i * $o ) > $i ).
tff(type_002,type,
typeCorrect: ( $o * $i ) > $o ).
tff(axiom_003,axiom,
! [X,X2: $o] : ( proj1pair(pair2(X,(X2))) = X ) ).
tff(axiom_004,axiom,
! [X,X2: $o] :
( proj2pair(pair2(X,(X2)))
<=> (X2) ) ).
tff(axiom_005,axiom,
! [X,X2] : ( head(cons(X,X2)) = X ) ).
tff(axiom_006,axiom,
! [X,X2] : ( tail(cons(X,X2)) = X2 ) ).
tff(axiom_007,axiom,
! [X,X2] : ( nil != cons(X,X2) ) ).
tff(axiom_008,axiom,
! [X] : ( proj1Suc(suc(X)) = X ) ).
tff(axiom_009,axiom,
! [X] : ( zero != suc(X) ) ).
tff(axiom_010,axiom,
! [X] : ( proj1High(high(X)) = X ) ).
tff(axiom_011,axiom,
! [X] : ( proj1Low(low(X)) = X ) ).
tff(axiom_012,axiom,
! [X,X2] : ( high(X) != low(X2) ) ).
tff(axiom_013,axiom,
! [X,X2] : ( proj1Nand(nand(X,X2)) = X ) ).
tff(axiom_014,axiom,
! [X,X2] : ( proj2Nand(nand(X,X2)) = X2 ) ).
tff(axiom_015,axiom,
! [X] : ( proj1Var(var(X)) = X ) ).
tff(axiom_016,axiom,
! [X,X2] : ( nand(X,X2) != tT ) ).
tff(axiom_017,axiom,
! [X,X2] : ( nand(X,X2) != fF ) ).
tff(axiom_018,axiom,
! [X,X2,X3] : ( nand(X,X2) != var(X3) ) ).
tff(axiom_019,axiom,
tT != fF ).
tff(axiom_020,axiom,
! [X] : ( tT != var(X) ) ).
tff(axiom_021,axiom,
! [X] : ( fF != var(X) ) ).
tff(axiom_022,axiom,
! [X,X2] : ( proj1Assign(assign(X,X2)) = X ) ).
tff(axiom_023,axiom,
! [X,X2] : ( proj2Assign(assign(X,X2)) = X2 ) ).
tff(axiom_024,axiom,
! [X,X2] : ( proj1Seq(seq(X,X2)) = X ) ).
tff(axiom_025,axiom,
! [X,X2] : ( proj2Seq(seq(X,X2)) = X2 ) ).
tff(axiom_026,axiom,
! [X,X2,X3] : ( proj1IfThenElse(ifThenElse(X,X2,X3)) = X ) ).
tff(axiom_027,axiom,
! [X,X2,X3] : ( proj2IfThenElse(ifThenElse(X,X2,X3)) = X2 ) ).
tff(axiom_028,axiom,
! [X,X2,X3] : ( proj3IfThenElse(ifThenElse(X,X2,X3)) = X3 ) ).
tff(axiom_029,axiom,
! [X,X2] : ( proj1Catch(catch(X,X2)) = X ) ).
tff(axiom_030,axiom,
! [X,X2] : ( proj2Catch(catch(X,X2)) = X2 ) ).
tff(axiom_031,axiom,
! [X,X2] : ( proj1While(while(X,X2)) = X ) ).
tff(axiom_032,axiom,
! [X,X2] : ( proj2While(while(X,X2)) = X2 ) ).
tff(axiom_033,axiom,
! [X,X2] : ( skip != assign(X,X2) ) ).
tff(axiom_034,axiom,
! [X,X2] : ( skip != seq(X,X2) ) ).
tff(axiom_035,axiom,
! [X,X2,X3] : ( skip != ifThenElse(X,X2,X3) ) ).
tff(axiom_036,axiom,
! [X,X2] : ( skip != catch(X,X2) ) ).
tff(axiom_037,axiom,
skip != throw ).
tff(axiom_038,axiom,
! [X,X2] : ( skip != while(X,X2) ) ).
tff(axiom_039,axiom,
! [X,X2,X3,X4] : ( assign(X,X2) != seq(X3,X4) ) ).
tff(axiom_040,axiom,
! [X,X2,X3,X4,X5] : ( assign(X,X2) != ifThenElse(X3,X4,X5) ) ).
tff(axiom_041,axiom,
! [X,X2,X3,X4] : ( assign(X,X2) != catch(X3,X4) ) ).
tff(axiom_042,axiom,
! [X,X2] : ( assign(X,X2) != throw ) ).
tff(axiom_043,axiom,
! [X,X2,X3,X4] : ( assign(X,X2) != while(X3,X4) ) ).
tff(axiom_044,axiom,
! [X,X2,X3,X4,X5] : ( seq(X,X2) != ifThenElse(X3,X4,X5) ) ).
tff(axiom_045,axiom,
! [X,X2,X3,X4] : ( seq(X,X2) != catch(X3,X4) ) ).
tff(axiom_046,axiom,
! [X,X2] : ( seq(X,X2) != throw ) ).
tff(axiom_047,axiom,
! [X,X2,X3,X4] : ( seq(X,X2) != while(X3,X4) ) ).
tff(axiom_048,axiom,
! [X,X2,X3,X4,X5] : ( ifThenElse(X,X2,X3) != catch(X4,X5) ) ).
tff(axiom_049,axiom,
! [X,X2,X3] : ( ifThenElse(X,X2,X3) != throw ) ).
tff(axiom_050,axiom,
! [X,X2,X3,X4,X5] : ( ifThenElse(X,X2,X3) != while(X4,X5) ) ).
tff(axiom_051,axiom,
! [X,X2] : ( catch(X,X2) != throw ) ).
tff(axiom_052,axiom,
! [X,X2,X3,X4] : ( catch(X,X2) != while(X3,X4) ) ).
tff(axiom_053,axiom,
! [X,X2] : ( throw != while(X,X2) ) ).
tff(axiom_054,axiom,
! [X] :
( ( X != nand(proj1Nand(X),proj2Nand(X)) )
=> ( ( X != var(proj1Var(X)) )
=> ~ secret(X) ) ) ).
tff(axiom_055,axiom,
! [A,B] :
( secret(nand(A,B))
<=> ( secret(A)
| secret(B) ) ) ).
tff(axiom_056,axiom,
! [Z] : secret(var(high(Z))) ).
tff(axiom_057,axiom,
! [X2] : ~ secret(var(low(X2))) ).
tff(axiom_058,axiom,
! [X: $o,Y] :
( ( Y != assign(proj1Assign(Y),proj2Assign(Y)) )
=> ( ( Y != seq(proj1Seq(Y),proj2Seq(Y)) )
=> ( ( Y != ifThenElse(proj1IfThenElse(Y),proj2IfThenElse(Y),proj3IfThenElse(Y)) )
=> ( ( Y != catch(proj1Catch(Y),proj2Catch(Y)) )
=> ( ( Y != while(proj1While(Y),proj2While(Y)) )
=> typeCorrect((X),Y) ) ) ) ) ) ).
tff(axiom_059,axiom,
! [X: $o,E,X2] : typeCorrect((X),assign(high(X2),E)) ).
tff(axiom_060,axiom,
! [X: $o,E,X3] :
( typeCorrect((X),assign(low(X3),E))
<=> ( ~ (X)
& ~ secret(E) ) ) ).
tff(axiom_061,axiom,
! [X: $o,P,Q] :
( typeCorrect((X),seq(P,Q))
<=> ( typeCorrect((X),P)
& typeCorrect((X),Q) ) ) ).
tff(axiom_062,axiom,
! [X: $o,C,R,Q2] :
( typeCorrect((X),ifThenElse(C,R,Q2))
<=> ( typeCorrect(( secret(C)
| (X) ),R)
& typeCorrect(( secret(C)
| (X) ),Q2) ) ) ).
tff(axiom_063,axiom,
! [X: $o,P2,Q3] :
( typeCorrect((X),catch(P2,Q3))
<=> ( typeCorrect((X),P2)
& typeCorrect((X),Q3) ) ) ).
tff(axiom_064,axiom,
! [X: $o,E2,P3] :
( typeCorrect((X),while(E2,P3))
<=> typeCorrect(( secret(E2)
| (X) ),P3) ) ).
tff(axiom_065,axiom,
l = low(zero) ).
tff(axiom_066,axiom,
h = high(zero) ).
tff(axiom_067,axiom,
! [X] : ~ elem(X,nil) ).
tff(axiom_068,axiom,
! [X,Z,Xs] :
( elem(X,cons(Z,Xs))
<=> ( ( Z = X )
| elem(X,Xs) ) ) ).
tff(axiom_069,axiom,
! [X,A,B] :
( eval(X,nand(A,B))
<=> ( ~ eval(X,A)
| ~ eval(X,B) ) ) ).
tff(axiom_070,axiom,
! [X] : eval(X,tT) ).
tff(axiom_071,axiom,
! [X] : ~ eval(X,fF) ).
tff(axiom_072,axiom,
! [X,Z] :
( eval(X,var(Z))
<=> elem(Z,X) ) ).
tff(axiom_073,axiom,
! [X] : ( del(X,nil) = nil ) ).
tff(axiom_074,axiom,
! [X,Z,Ys] :
( ( X = Z )
=> ( del(X,cons(Z,Ys)) = del(X,Ys) ) ) ).
tff(axiom_075,axiom,
! [X,Z,Ys] :
( ( X != Z )
=> ( del(X,cons(Z,Ys)) = cons(Z,del(X,Ys)) ) ) ).
tff(axiom_076,axiom,
! [X] : ( run(X,skip) = pair2(X,$false) ) ).
tff(axiom_077,axiom,
! [X,Z,E] :
( eval(X,E)
=> ( run(X,assign(Z,E)) = pair2(cons(Z,X),$false) ) ) ).
tff(axiom_078,axiom,
! [X,Z,E] :
( ~ eval(X,E)
=> ( run(X,assign(Z,E)) = pair2(del(Z,X),$false) ) ) ).
tff(axiom_079,axiom,
! [X,P,Q,S1] :
( ( run(X,P) = pair2(S1,$true) )
=> ( run(X,seq(P,Q)) = pair2(S1,$true) ) ) ).
tff(axiom_080,axiom,
! [X,P,Q,S1] :
( ( run(X,P) = pair2(S1,$false) )
=> ( run(X,seq(P,Q)) = run(S1,Q) ) ) ).
tff(axiom_081,axiom,
! [X,E2,R,Q2] :
( eval(X,E2)
=> ( run(X,ifThenElse(E2,R,Q2)) = run(X,R) ) ) ).
tff(axiom_082,axiom,
! [X,E2,R,Q2] :
( ~ eval(X,E2)
=> ( run(X,ifThenElse(E2,R,Q2)) = run(X,Q2) ) ) ).
tff(axiom_083,axiom,
! [X,P2,Q3,S] :
( ( run(X,P2) = pair2(S,$true) )
=> ( run(X,catch(P2,Q3)) = run(S,Q3) ) ) ).
tff(axiom_084,axiom,
! [X,P2,Q3,S] :
( ( run(X,P2) = pair2(S,$false) )
=> ( run(X,catch(P2,Q3)) = pair2(S,$false) ) ) ).
tff(axiom_085,axiom,
! [X] : ( run(X,throw) = pair2(X,$true) ) ).
tff(axiom_086,axiom,
! [X,E3,P3] : ( run(X,while(E3,P3)) = run(X,ifThenElse(E3,seq(P3,while(E3,P3)),skip)) ) ).
tff(goal_087,conjecture,
? [P,S] :
~ ( typeCorrect($false,P)
=> ( elem(l,proj1pair(run(S,P)))
<=> elem(l,proj1pair(run(cons(h,S),P))) ) ) ).
%------------------------------------------------------------------------------