Inferring authentication tags

摘要

We present PEAR (Protocol Extendable AnalyzeR), a tool automating the two static analyses for authentication protocols presented in [7, 8]. These analyses are based on a tagging scheme that describes how message components contribute in achieving authentication. The tool provides a tag inference procedure that allows users to analyze untagged protocol specifications. When a protocol is successfully validated, tags give users precise information on how and why authentication is guaranteed. Notably, the tool receives in input both the protocol specification and the validation rules. Both validation and tag inference are parametric with respect to the validation rules, thus allowing users to easily implement new rules/analyses with no need of modifying the underlying procedures.