基于Abadi-Rowgaway的形式化加密的计算合理性定理，提出和证明了密码协议形式化分析的计算合理性定理。通过对群密钥分配协议安全性的分析，说明定理对协议的可选择攻击具有较强的分析能力，提出了群密钥分配协议的形式化方法与计算方法下安全性的形式化定义，并证明了其合理性。