電力系統(tǒng)安全協(xié)議形式化分析技術(shù)研究.pdf

1、電力通信是電力系統(tǒng)的重要組成部分。電力通信的安全需求包括身份認(rèn)證，存取控制，防火墻等，這些安全需求的實(shí)現(xiàn)都依靠安全協(xié)議。安全協(xié)議是構(gòu)建在密碼體制上的一種交互協(xié)議，是電力通信系統(tǒng)可靠性的重要保障。但是，設(shè)計(jì)一個(gè)符合安全目標(biāo)的安全協(xié)議是十分困難的。從安全協(xié)議的發(fā)展過程分析，往往是先設(shè)計(jì)協(xié)議，若在使用過程中發(fā)現(xiàn)了某個(gè)安全漏洞，彌補(bǔ)該漏洞，再繼續(xù)使用。有些漏洞甚至在協(xié)議設(shè)計(jì)后的十幾年才得以發(fā)現(xiàn)。因此，我們必須借助一些方法和技術(shù)指導(dǎo)協(xié)議的設(shè)計(jì)，并

2、在協(xié)議設(shè)計(jì)后對(duì)其進(jìn)行分析。本文研究協(xié)議的分析技術(shù)。 自動(dòng)化分析一直以來都是國內(nèi)外研究人員的追求目標(biāo)，形式化分析是自動(dòng)化分析的基礎(chǔ)和前期研究，在形式化分析的基礎(chǔ)上，通過形式描述語言可以具體實(shí)現(xiàn)自動(dòng)化分析。本文是針對(duì)自動(dòng)化分析的基礎(chǔ)研究：采用BAN類邏輯(BurrowsAbadi Needham Logic)和串空間方法，先對(duì)安全協(xié)議進(jìn)行不同類型的數(shù)學(xué)抽象，再基于這些抽象分析協(xié)議的安全性。主要的研究工作和成果有：一是把AODV安全協(xié)