Admissible Interference by Typing for Cryptographic Protocols

摘要

Many security properties of cryptographic protocols can be expressed by using information flow policies as non-interference. But, in general it is very difficult to design a system without interference. For that, many works try to weak the standard definition of the noninterference. For instance, in [21] Mullins defines the admissible interference as an interference that admits flow information only through a dowgrader. Thus, we present in this paper a type system that try to detect process that allow interference. Then, if we can type a process we can say that is free interference. Also, we extend the type system of process with another type system based on a standard message algebra used in the literature of cryptographic protocols. So, we define the theo-ric characterization, prove the correctness of our type system and present an illustration of our result.