樂(lè)觀合同簽訂協(xié)議的分析和驗(yàn)證.pdf

1、在目前提出的電子合同簽訂協(xié)議中，樂(lè)觀合同簽訂協(xié)議由于運(yùn)行效率高而具有應(yīng)用前景。對(duì)于樂(lè)觀簽訂協(xié)議的設(shè)計(jì)和驗(yàn)證是一個(gè)研究熱點(diǎn)，除了常用的理論和方法，人們還提出了一些新的手段。一些典型的協(xié)議已經(jīng)成為各種分析驗(yàn)證方法和工具的試驗(yàn)臺(tái)。
　　 樂(lè)觀合同簽訂協(xié)議通常包括主協(xié)議和子協(xié)議，由于主協(xié)議消息交換輪次和子協(xié)議設(shè)計(jì)的區(qū)別，表現(xiàn)為不同的結(jié)構(gòu)。本文從結(jié)構(gòu)上對(duì)協(xié)議的各種安全屬性進(jìn)行了分析。提出了一種協(xié)議結(jié)構(gòu)的圖形表示，直觀表現(xiàn)了協(xié)議動(dòng)作之間的關(guān)

2、系，以此推出了協(xié)議滿足安全屬性的條件，給出了可能滿足安全屬性的協(xié)議結(jié)構(gòu)，證明了一個(gè)可行的樂(lè)觀合同簽訂協(xié)議至少需要四輪消息交換。
　　 由于結(jié)構(gòu)分析忽略了消息的具體內(nèi)容，而且只能檢驗(yàn)一次協(xié)議運(yùn)行的情況，所以在進(jìn)行協(xié)議分析時(shí)需要與其它工具相結(jié)合。根據(jù)結(jié)構(gòu)分析的結(jié)果，本文用模型檢測(cè)工具SPIN對(duì)不滿足公平性的協(xié)議進(jìn)行了驗(yàn)證，一方面證明了結(jié)構(gòu)分析的正確性，一方面用反例得到了攻擊軌跡。對(duì)結(jié)構(gòu)分析中沒(méi)發(fā)現(xiàn)問(wèn)題的協(xié)議也進(jìn)行了驗(yàn)證，發(fā)現(xiàn)了用結(jié)構(gòu)