復(fù)雜安全協(xié)議的形式化分析、設(shè)計(jì)與驗(yàn)證研究.pdf

1、保障網(wǎng)絡(luò)通信安全的一個(gè)極其重要的環(huán)節(jié)是安全協(xié)議,安全協(xié)議的形式分析方法已成為近年來安全領(lǐng)域研究的熱點(diǎn)之一.同時(shí)PKI體系作為一個(gè)強(qiáng)有力的網(wǎng)絡(luò)安全保障系統(tǒng)已被廣泛應(yīng)用于各種商業(yè)網(wǎng)絡(luò)環(huán)境,各種基于PKI應(yīng)用的復(fù)雜安全協(xié)議也成為研究和發(fā)展熱門,其中以SSL協(xié)議的應(yīng)用最為成功.目前,試圖用簡單的推理構(gòu)造邏輯方法分析諸如SSL的復(fù)雜安全協(xié)議其效果不盡人意,因此,該文的研究重點(diǎn)就在于提出一種新的形式化分析思路來分析和設(shè)計(jì)復(fù)雜的安全協(xié)議.復(fù)雜安全協(xié)議

2、本質(zhì)上就是由簡單的協(xié)議模型不斷進(jìn)化而得,因此該文采用基于代數(shù)規(guī)范的方法提出一個(gè)安全協(xié)議的進(jìn)化模型框架,安全協(xié)議的主體均可采用該框架得以形式化描述,并通過進(jìn)化模型的擴(kuò)展達(dá)到安全協(xié)議進(jìn)化的目的.該文采用著名的信念邏輯GNY邏輯系統(tǒng)及其相關(guān)的形式化工具SPEARII,以SSL協(xié)議為分析實(shí)例,詳細(xì)闡述了從初始協(xié)議模型到各個(gè)進(jìn)化協(xié)議模型的分析過程,并將最終的進(jìn)化模型與SSL協(xié)議作比較,給出SSL協(xié)議的安全分析,同時(shí)在分析過程中以協(xié)議模型為基礎(chǔ)設(shè)計(jì)