Automated type-based analysis of injective agreement in the presence of compromised principals

We present a type system to analyze authentication protocols in the presence of compromised principals. The main feature of our analysis method is that it relies on a minimal set of assumptions and checks protocols for a strong authentication requirement known as injective agreement. The set of compromised principals is allowed to grow dynamically and there is no restriction on the kind of nonce handshake employed in the protocol. We also present and implement a type reconstruction algorithm that automates the analysis in the sense that only a very high-level specification of the protocol and security requirements is required.