Protocol Analysis of Modal Logic Combined with Strand Space with Variables
Xiang Li · Jisuanji gongcheng · 2007
A strand space model with variables is provided based on traditional strand space,the undermined terms and subterms are expressed with variables,and the variable occurs in the message term and its calculus.The protocol consists of strands with variables belonging to different participants in the protocol running.Based on the concrete traces,the logic designed for reasoning about the principal action,consists of syntax,atoms and inference rules.The basic modal formula [ P] Aφ means that the action P is finished with the result of φ.By associating sequence of actions and attaching the formulas,it can prove the security properties of protocols such as secrecy and authentication.It analyzes Helsinki protocol through the method,and the logic leads directly to rediscovery of Horng-Hsu’s attack.