一种基于扩展Spi演算的类型系统

摘要

主要探讨了使用非形式化的原理和形式化的规则来获得密码协议安全属性的方法.这些原理和规则基于传统的等级和信息流的思想,通过将其扩展后用来处理密码协议中的并发进程.提出的规则是基于Spi演算扩展语法的一种类型规则.通过这些规则可以向用户担保,如果协议通过了类型检测,则该协议没有泄漏任何秘密的消息.