Universally Composable Formal Analysis of Sender Non-repudiation Protocol
Jie Yang · Jisuanji gongcheng · 2009
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.