基于Horn逻辑扩展模型的安全协议反例的自动构造.pdf

ISSN 11—1777／TP 计算机研究与发展 1000一1239／CN of Researchand JournalComputer Development 基于Horn逻辑扩展模型的安全协议反例的自动构造 周 倜1 李梦君1 李舟军2 陈火旺1 1(国防科学技术大学计算机学院长沙4l0073) 2(北京航空航天大学计算机学院北京 100083) (tzhou@nudt．edu．cn) on 0f ProtOcolsBasedthe AutomaticallyConstructingCounter-ExamplesSecurity ExtendedHorn Model Logic ZhouTil，Li Chen Men翊unl，LiZhoujun2，andHuowan91 1(^00Z0，C0m抛￡eri鲫卯，Nn￡io挖“Uiw勿盯啦力咒卵Tk^加z0_削，吼乜卵g饥口410073) 100083) 2(矗。。Zo，CD研p“}8rSciP雄c已口行蠢Engi咒PPri行g，B西矗。起g乙‰i雠rs矗y，Be巧i竹g AbstractItis toconstruct of there veryimportant counte卜examplessecurityprotocolsautomatically，but arefewmethodstodothiswork．BasedontheextendedHorn modelandthe logic corresponding ve“ficationmethodof thesolution are whichareusedtoconstruct securityprotocols， strategiespresented， intuitionistic in whichbreakthe automaticaUy counter—examplesprotoc01s secu“typroperties．!；ome thecorrectnessofthese Based。nthis the。remsare t。makesure soluti。n important proved strategies． seriesof are toconstruct of model，a algorithmsdesigned counter-examplessecurityprotoc01sautomatically， the methodsofsomemain are their are indetail．These complexities optimal algo“thmsgiven，and analyzed whichis in functional