A method for securing a first program with a second program, a third program and a fourth program, each program comprising constitutive elements having a finite number of program points and evolution rules associated with the program points and defining the passage from one program point to another program point, and each program comprising a definition of a set of properties each property being associated with one or more of the constitutive elements of the program. The fourth program constructed by defining at least one relation between at least one constitutive element of the second program and at least one constitutive element of the third program, said relation being named a correspondence relation, and at least one property of the third program being proven, propagate the proof of said property to at least one property of the first program by exploitation of the correspondence relation.