位置：成果数据库 > 期刊 > 期刊详情页
SET证书申请协议在SPV下的自动化验证及改进
  • 期刊名称：计算机学报, 31(6):1035-1045, 2008
  • 时间：0
  • 分类：TP309[自动化与计算机技术—计算机系统结构;自动化与计算机技术—计算机科学与技术]
  • 作者机构：[1]中山大学信息科学与技术学院广东省信息安全重点实验室,广州510275, [2]北京大学信息科学技术学院教育部高可信软件技术重点实验室,北京100871, [3]暨南大学计算机科学系,广州510632, [4]北京工业大学计算机学院,北京100022, [5]华南师范大学计算机学院,广州510631
  • 相关基金：本课题得到国家“九七三”重点基础研究发展规划项目基金（2005CB321902）、国家自然科学基金（60496327,10410638,60473004）、广东省自然科学基金（06023195）和广东省自然科学基金团队项目（04205407）资助.
  • 相关项目：非规范知识交叉领域研究
关键词： SET证书申请协议, 自动化验证, SPV, 认证性, 秘密性, SET certificate registration protocols, automatic verification, SPV, authentication, secrecy
中文摘要：

基于实例化空间逻辑理论，使用知识推理方法，在SPV（Security Protocol Verifier）下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明，并对协议进行了改进。SPV调用工业级SAT求解器，能够高效验证安全协议是否满足CAPSL（Common Authentication Protocol Specification Language）协议规范及单层、多层认知规范。应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化，而SET协议作为当前最复杂的工业级协议，其原始文档有上千页，因此简化过程相当困难，相关研究较少，已有的一些简化模型也不够完整。因此，文章针对SET证书申请协议，给出了比以往更贴近原协议的简化模型，并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果，分析了由于协议不满足某些认知规范所带来的安全隐患，从而对协议进行改进，最后证明了改进后协议的有效性。该工作也充分说明了SPV足以处理复杂的工业级协议。

英文摘要：

Based on the Instantiation Space Logic theory and knowledge reasoning, the authors implement the totally automatic verification on the complete SET certificate registration protocols＇ authentication and secrecy properties using SPV, and improve the protocols. SPV can efficiently verify whether the security protocol satisfies the goals in CAPSL（Common Authentication Protocol Specification Language） as well as multi-level epistemic specifications using modern SAT solvers. All protocols should be simplified before being verified by logics or tools. As to the SET protocols, it is the most complex industrial protocol at present, which has the document of over 1000 pages. Therefore, it is very difficult to simplify and there are few research works about it. Besides, some existent simplified models are not complete enough. Consequently, the paper gives a simplified model which is more close to the original SET certificate registration protocols, and introduces the model＇s formal description in SPV with the verification process and results. More over, according to the hidden danger of the protocols brought by the unsatisfied epistemic specification, the authors improve the protocols and show the effectiveness. The work also justifies that SPV has the ability to deal with complex industrial protocols.

同期刊论文项目
非规范知识交叉领域研究
期刊论文 134 会议论文 68 著作 2
系统规范表示与验证的认识逻辑途径
期刊论文 64 会议论文 33 著作 2
同项目期刊论文
Missing is Useful": Missing Values in Cost-sensitive Decision Trees
Computation of Arbitrage in Frictional Bond Markets
Optimal Dynamic Portfolio Selection with Earnings-at-Risk
Compensatory ability to null mutation in metabolic networks
An Effective GML Documents Compressor
Random Sierpinski network with scale-free small world and modular structure
Rigorous solution of average distance for Sierpinski network
A Characterization Theorem for Injective Model Classes Axiomatized by General Rules
Similarity between preferential models
Some Representation Theorems for recovering contraction relations
A Simplicial Approach for Discrete Fixed Point Theorems
Computation of Arbitrage in a Financial Market with Various Types of Frictions
An ontology-theme-based method of acquiring knowledge from Chinese natural language documents
A Survey on Description Logic
Prediction of protein-protein interactions from primary sequences
一个基于智能的MAS模型及其方法论
多主体系统时态认知规范的"On the fly"模型检测算法研究
有界模型检测同步多智能体系统的时态认知逻辑
有缺指派下的信念修正逻辑
Analog-Cell：一种新的电子细胞图形模型
LIGHT: A Query-Efficient yet Low-Maintenance Indexing Scheme over DHTs
Effects of accelerating growth on the evolution of weighted complex networks
“理解”论：信息内容认知机理的假说
机制主义方法与人工智能统一理论
基于分形技术的数据流突变检测算法
Semantic interpretation of Compositional Logic in Instantiation Space
Mining Multiple Data Sources: Local Pattern Analysis
Detecting Differences between Contrast Groups
Missing Data Analysis: A Kernel-Based Multi-imputation Approach
Cognitive Approach to Artificial Intelligence
Forward Looking Nash Equilibrium for Keyword Auction
Knowledge structure approach to verification of authentication protocols
To build a Blocklist Based on the Cost of Spam
Detecting Inconsistency in Biological Molecular Databases using Ontology
Domain-Driven Data Mining, a Practical Methodology
基于约束的自然语言问题到OWL的语义映射方法研究
Two Representation Theorems for Nonmonotonic Inference Relations
A modal characterization of Lambda-bisimilarity
An algebraic Characterization of equivalent preferential models
符号化模型检测CTL*
论“信息-知识-智能转换规律”
Evolving pseudofractal networks
From regular to growing small-world networks
Computing the Minimum-Support for Mining Frequent Patterns
Identifying Follow Correlation Itemset-Pairs
Estimating Confidence Intervals for Structural Differences between Contrast Groups with Missing Data
Mining Class-bridge Rules Based on Rough Sets
Strategies for Complex Data Cube Queries
Rule-based Dependency Models for Security Protocol Analysis
POP Algorithm: Kernel-Based Imputation to Treat Missing Values in Knowledge Discovery from Databases
Empirical Likelihood Confidence Intervals for Differences between Two Datasets with Missing Data
Activity Mining: from Activities to Actions
Structuralism? Functionalism? Behaviorism? Or Mechanism? - - Looking Backward and Forward for Bett
An Investigation on The Theory of Information-Knowledge-Intelligence Transforms
SAT问题中局部搜索法的改进
Verification of Authentication Protocols for Epistemic Goals via SAT Compilation
Primitive Recursiveness of Real Numbers under Different Representations
Observation-Based Logic of Knowledge, Belief, Desire and Intention.
Primitive recursive real numbers.
Customer Retention: Identifying Actionable Information from Web-Logs
Generalized Dimension-Reduction Framework for Recent-Biased Time Series Analysis
EDUA: An Efficient Algorithm for Dynamic Database Mining
A Behavioural Pseudometric based on lambda—Bisimilarity
On Default Correlation and Pricing of Collateralized Debt Obligation by Copula Functions
Genetic-algorithm-based Strategy for Identifying Association Rules without Specifying Actual Minimum
Self-similarity, small-world, scale-free scaling, disassortativity, and robustness in hierarchical l
A geometric growth model interpolating between regular and small-world networks
Advanced Intelligence and Mechanism Approach
Adaptive indexing for content-based search in P2P systems
Identifying quality knowledge from different data sources
Model Checking Temporal Logics of Knowledge Via OBDDs
知识的内涵与度量
人工智能理论：从分立到统一的奥秘
人工智能：由分立走向和谐
An efficient peer-to-peer indexing tree structure for multidimensional data
Association-Based Segmentation for Chinese-Crossed Query Expansion
On Data Structures for Association Rule Discovery
Tracking clusters in evolving data streams over sliding windows
多智能体系统时态认知规范高效符号模型检测的算法研究
Recursive weighted treelike networks
一种支持多维数据范围查询的对等计算索引框架
Characterize branching distance in terms of ()-bisimilarity
非结构化对等计算系统中多维范围搜索
信息转换原理：信息、知识、智能的一体化理论
一种多特征方查询的有效算法
一种有效的信息检索模型
完全加权关联规则挖掘及其在查询扩展中的应用
多数据库中例外模式挖掘方法研究
关系数据库中基于区域聚类的多区域查询优化
复杂网络研究进展：模型与应用
使用SVMs进行汉语浅层分析
注意-情绪协调的个性化信息推荐模型
目的地选择服务系统中的智能逻辑推理
语言认知与主题内容识别
移动个性化信息服务中的用户兴趣模型
鲁棒局部保持投影的表情识别
基于全信息自然语言理解的语音识别后文本处理
基于实例的机器辅助写作翻译系统
信任感知的组合服务动态选择方法
基于高维空间的在线高效子空间Skyline算法——CSky
用CLP技术解决动画自动生成中的布局规划问题
谱聚类算法对输入数据顺序的敏感性
短信过滤系统设计分析
数据流中概念漂移检测的集成分类器设计
实例化空间：一种新的安全协议验证逻辑的语义模型
多主体系统时态认知规范的“On the Fly”模型检测算法研究
智能目的地选择服务系统的设计与实现
有界模型检测同步多智体系统的时态认知逻辑
基于图形处理器的数据流快速聚类
基于滑动窗口的进化数据流聚类
SAT 问题中局部搜索法的改进
A logical framework for Identifying quality knowledge from different data sources
多主体系统时态认知规范的"On the fly"模型检测算法研究
实例化空间: 一种新的安全协议验证逻辑的语义模型
有界模型检测的优化
SET证书申请协议在SPV下的自动化
多智能体系统时态认知规范高效符
多主体系统时态认知规范的"On th
Bounded model Checking knowled
Computationally grounded model
Improving Encoding Efficiency
MCTK（认识逻辑模型检测工具）
SPV（安全协议分析器）
Verification of Multi-agent Sy
Exploiting Inference Rules to
Within-problem Learning for Ef
BDDRPA*: An Efficient BDD-base
An Extended Interpreted System
一个基于智能的 MAS 模型及其方法论
Primitive Recursive Real Numbers under different Representations
Primitive Recursive Real Numbers
SET 证书申请协议在 SPV 下的自动化验证及改进
一个基于智能的MAS模型及其方法论
Verification of Authentication Protocols for Epistemic Goals via SAT Compilation
Knowledge structure approach t
实例化空间: 一种新的安全协议验
基于知识结构的认证协议验证
符号化模型检测CTL
多智能体系统时态认知规范的"On
Identifying quality knowledge
一个基于智能的MAS模型及其方法
Model Checking Temporal Logics
Semantic interpretation of Com
有界模型检测同步多智能体系统的
Verification of Authentication
Primitive Recursive Real Numbe
实例化空间：一种新的安全协议验证逻辑的语义模型
多主体系统时态认知规范的“On the Fly”模型检测算法研究
有界模型检测同步多智体系统的时态认知逻辑
一种基于多模式加密算法的文件保护方案
网络课程中基于Web的在线测试系统的研究与实现
New Retrieval Method Based on Relative Entropy for Language Modeling with Different Smoothing Methods