Techniques for Security Checking Non-Interference vs Control Flow Analysis1 1Research partially supported by MURST Progetto Cofinanziato TOSCA.

AbstractWe model, in a process algebra framework, a variant of the well known Wide Mouthed Frog security protocol. Its relevant security properties are addressed both from a dynamic and static point of view, having operational semantics as a common starting point. In one case, we exploit techniques based on Non-Interference, while in the other one we rely on Control Flow Analysis. We then compare these techniques