摘要： UCSA(Universally Composable Symbolic Analysis)框架结合了形式化分析方法和UC框架。在前人的基础上继续扩展UCSA框架的适用范围。为了使该框架能够分析发送者非否认协议，提出发送者非否认性的理想功能和形式化定义，利用分析执行序列和构造模拟进程的方法分析两者在UCSA框架下的可靠性和完备性。结果表明两者在UCSA框架下是等价的。
关键词:
非否认协议,
发送者非否认性,
形式化分析,
UCSA框架
Abstract: Universally Composable Symbolic Analysis(UCSA) framework is a new method based on formal analysis and UC framework to analyze security protocols. This paper extends UCSA framework based on predecessors’ contribution, defines the ideal functionality and formal definition of sender’s non-repudiation protocols and analyzes whether the two are identical under the UCSA framework by simulation and execution trace analysis. The result shows that the ideal functionality and formal definition are identical under UCSA.
Key words:
non-repudiation protocol,
sender non-repudiation,
formal analysis,
Universally Composable Symbolic Analysis(UCSA) framework
中图分类号:
杨 杰. 发送者非否认协议的UC形式化分析[J]. 计算机工程, 2009, 35(20): 128-130.
YANG Jie. Universally Composable Formal Analysis of Sender Non-repudiation Protocol[J]. Computer Engineering, 2009, 35(20): 128-130.