網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析-全文預(yù)覽
【正文】 ly successful and widely used software modelchecking system based on formal methods from Computer Science. It has made advanced theoretical verification methods applicable to large and highly plex software systems. In April 2022 the tool was awarded the prestigious System Software Award for 2022 by the ACM. SPIN uses a high level language to specify systems descriptions, including protocols, called Promela (PROcess MEta LAnguage). 2022/2/5 第二十次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì) 15 BANYahalom Protocol [1] A→B: A, Na [2] B→S: B, Nb, {A, Na}K bs [3] S→A: Nb, {B, Kab, Na}K as , {A, Kab, Nb}Kbs [4] A→B: {A, Kab, Nb}K bs , {Nb}Kab 2022/2/5 第二十次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì) 16 Attack 1 (intruder impersonates Bob to Alice) A→I(B): A, Na I(B)→A: B, Na A→I(S): A, Na’, {B, Na}K as I(A)→S: A, Na, {B, Na}K as S→I(B): Na, {A, Kab, Na}K as , {B, Kab, Na}Kbs I(S)→A: Ne, {B, Kab, Na}K as , {A, Kab, Na}Kbs A→I(B): {A, Kab, Nb}K bs , {Ne}Kab 2022/2/5 第二十次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì) 17 Attack 2 (intruder impersonates Alice) A→B: A, Na B→S: B, Nb, {A, Na}K bs I(A)→B: A, (Na, Nb) B→I(S): B, Nb’, {A, Na, Nb}K as (Omitted) I(A)→B: {A, Na, Nb}K bs , {Nb}Na 2022/2/5 第二十次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì) 18 Attack 3 A→B: A, Na B→S: B, Nb, {A, Na}K bs I(B)→A: B, Nb A→I(S): A, Na’, {B, Nb}K as I(A)→S: A, Na, {B, Nb}K as S→I(B): Na, {A, Kab’, Nb}K bs , {B, Kab’, Na}Kas I(S)→A: Nb, {B, Kab’, Na}K as , {A, Kab’, Nb}Kbs A→B: {A, Kab’, Nb}K bs , {Nb}Kab’ 2022/2/5 第二十次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì) 19 Optimization strategies ? Using static analysis and syntactical reordering techniques ? T
試題試卷相關(guān)推薦
鄂ICP備17016276號(hào)-1