Fault attacks consist in changing the program behavior by injecting faults at run-time, either at hardware or at software level. Their goal is to change the correct progress of the algorithm and hence, either to allow gaining some privilege access or to allow retrieving some secret information based on an analysis of the deviation of the corrupted behavior with respect to the original one. Countermeasures have been proposed to protect embedded systems by adding spatial, temporal or information redundancy at hardware or software level. First we define Countermeasures Check Point (CCP) and CCPs-based countermeasures as an important subclass of countermeasures. Then we propose a methodology to generate an optimal protection scheme for CCPs-based countermeasure. Finally we evaluate our work on a benchmark of code examples with respect to several Control Flow Integrity (CFI) oriented existing protection schemes.

Chosen-ciphertext security is by now a standard security property for asymmetric encryption. Many generic constructions for building secure cryptosystems from primitives with lower level of security have been proposed. Providing security proofs has also become standard practice. There is, however, a lack of automated verification procedures that analyze such cryptosystems and provide security proofs. This paper presents an automated procedure for analyzing generic asymmetric encryption schemes in the random oracle model. It has been applied to several examples of encryption schemes among which the construction of Bellare-Rogaway 1993, of Pointcheval at PKC'2000 and REACT.

This paper presents a process calculus for reconfig-urable communicating systems which has broadcast as ba-sic communication primitive, and we provide an opera-tional semantics for this calculus. We illustrate the calculus through some examples, and we propose three behavioural equivalences for reasoning about systems of broadcasting processes, namely, barbed equivalence, step-equivalence and labelled bisimilarity. An important result, is that all these relations coincide, providing different ways to study the equivalence/non-equivalence of two systems. Then, we provide a direct characterization for the strong congruence relation induced by these equivalences. Finally, we give a complete axiomatisation for strong congruence. 1.