可证明安全性是密码协议安全性评估的重要依据，但手写安全性证明容易出错且正确性难以判定，利用计算机辅助构造游戏序列进而实现自动化证明是当前一种可行的方法。为此提出一种基于进程演算的密码协议形式化描述模型，定义了描述密码协议安全性证明中攻击游戏的语法规则，并借助工具LEX和YACC，设计出解析器程序，将密码协议及其安全性的形式化描述解析为自动化安全性证明系统的初始数据结构，并用实例来说明这种方法的可行性。