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

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

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