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

计算机工程与应用 ›› 2007, Vol. 43 ›› Issue (3): 131-131.

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

袁霖王亚弟韩继红

郑州解放军信息工程大学电子技术学院102教研室信息工程大学电子技术学院信息工程大学电子技术学院

收稿日期:2006-02-14 修回日期:1900-01-01 出版日期:2007-01-21 发布日期:2007-01-21
通讯作者: 袁霖

A Type System Based on Extended Spi Calculus

Received:2006-02-14 Revised:1900-01-01 Online:2007-01-21 Published:2007-01-21

摘要/Abstract

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

关键词: 类型系统, 密码协议, 保密性, 类型规则

Abstract: The way wich uses informal principles and formal rules to cryptographic protocols is probed in this paper. These principles and rules stem from traditional concepts of classification and information flow. The rules presented in this paper is a kind of typing rules based on extended Spi Calculus. These rules guarantee that if a protocol typechecks ,then it does not leak its secret inputs.

Key words: type system, cryptographic protocols, secrecy properties, typing rules

袁霖王亚弟韩继红. 一种基于扩展Spi演算的类型系统[J]. 计算机工程与应用, 2007, 43(3): 131-131.

[1]	祝义1，2，黄志球1，周航1，刘林源1，3. 函数式程序模板元编程的元建模实现方法[J]. 计算机工程与应用, 2018, 54(7): 1-10.
[2]	米军利1，谢淑翠2，张建中3. 有条件容忍入侵的数字签名协议[J]. 计算机工程与应用, 2013, 49(1): 82-85.
[3]	余磊，魏仕民. 网络管理中一种互认证密码协议的安全性分析[J]. 计算机工程与应用, 2012, 48(4): 94-96.
[4]	孙培勇，刘忆宁，延吉红，曹建宇. 一种安全的多候选人电子投票方案[J]. 计算机工程与应用, 2012, 48(25): 217-219.
[5]	陈莉，王唯贤. 改进的可认证邮件传递协议及其安全属性分析[J]. 计算机工程与应用, 2011, 47(21): 112-114.
[6]	陈虎，宋如顺，张福泰. 无证书并行签密方案[J]. 计算机工程与应用, 2009, 45(21): 85-87.
[7]	赖欣,喻秀英,何大可. 基于ECDLP的高效承诺方案[J]. 计算机工程与应用, 2008, 44(3): 136-138.
[8]	丁萌伟,周清雷,赵东明. Yahalom-Paulson协议的串空间模型与分析[J]. 计算机工程与应用, 2008, 44(22): 97-99.
[9]	刘荣胜黄邵高春鸣. 基于类型化Pi-演算的Web服务组合相容性检测[J]. 计算机工程与应用, 2007, 43(7): 120-124.
[10]	周正^1,刘毅²,沈昌祥². 一种新的保密性与完整性统一安全策略[J]. 计算机工程与应用, 2007, 43(34): 1-2.
[11]	王全来^1,2，王亚弟¹，韩继红¹. 密码协议形式化分析的计算合理性[J]. 计算机工程与应用, 2007, 43(21): 8-11.