| Lately, a surge of interest has been expressed in computer security. This could be explained by the dazzling proliferation of computer networks and the extensive use of distributed systems, World Wide Web, e-commerce, etc. This gave rise to plenty of cryptographic protocols. The main goal underlying these protocols is to enforce critical security properties such as authentication, secrecy, integrity, atomicity, etc. Nevertheless, the absence of well-established and dedicated formal methods for the specification and verification of security protocols has induced undesirable consequences. Actually, many protocols have been shown flawed many years after their use. Hence, there is a desideratum that consists in elaborating formal frameworks for the formal automatic design and validation of security protocols. This thesis is a contribution in this respect with the following items. (1) The proposition of a taxonomy of cryptographic protocol, flaws. (2) The proposition of a taxonomy of methods used to specify and analyze cryptographic protocols. (3) The proposition of a formal, sound and complete typing system to analyze cryptographic protocols. (4) The development of an algorithm, based on the typing system, to automatically discover flaws in security protocols. (5) The development of DYMNA, an environment implemented in Java, based on the aforementioned algorithm, and devoted to specify and analyze security protocols. (6) The correctness of some cryptographic protocols with respect to the secrecy property. (7) The proposition of a new dynamic, linear and modal logic endowed with a tableau-based system to specify security properties and specially e-commerce properties. |
