Validating Security Protocols under the General Attacker

摘要: Security protocols have been analysed using a variety of tools and focusing on properties. Most findings assume the ever so popular Dolev-Yao threat model. A more recent model called Rational Attacker [1] sees each protocol participant decide whether or not to conform upon their own cost/benefit analysis. Each neither colludes nor shares knowledge with anyone, feature that rules out applicability existing equivalence results in Aiming at mechanical validation, we abstract away actual analysis obtain General model, which principal blindly act as attacker. The security under brings forward yet insights: retaliation attacks anticipation are our main findings, while tool support can scale up new negligible price. The general for based set-rewriting was adopted AVISPA [2] is leveraged express Attacker. state-of-the-art checker SATMC [3] then used automatically validate threats, be found.