Д-р Генадий А. Черней
Директор на Департамента Информационни
Технологии при Националната банка на Молдова
Проф. Д-р ек.н. Сергей А. Охрименко
Лаборатория по информационна безопасност
към Молдовска икономическа академия
АНАЛИЗ НА НАДЕЖДНОСТТА НА ПРОТОКОЛИТЕ ЗА АУТЕНТИФИКАЦИЯ
В настоящата разработка се прави опит за кратък обзор на съвременното състояние и използването на формалните методи и развитието на съответстващ инструментариум за анализ, съставяне и проверка на криптографските протоколи. Очертани са главните тенденции в изследванията в посочената област.
Разработката е продължение на изследванията, отразени в публикации на авторите [1-4]. За сравняване на различните протоколи за аутентификация, разкриване на общите и специфичните свойства, а също и за подреждане на множеството, е целесъобразно да се изгради класификационнна система. Възможно е обособяване на групи от гледна точка на типа ауентификация, обема, типа на използваната заявена информация (или според начина на разпределяне на тайните). Ще се спрем по подробно.
От гледна точка на мястото аутентификацията се разглежда като локална и отдалечена. Локална е тази аутентификация, която осъществява непосредствено от интерактиращ компютър. Като приемер може да се разгледа ситуацията, в която позволяващият се ауинтефицира при зареждането на компютъра.
При отдалечената аутентификация обектът или субектът, които са източник на информация, се намират на значително разстояние от проверяващия, разделяни от канала за връзка. В този случай задачата за ауентифициране се свежда до процеса на доказване:
Според обекта на ауентификация се разграничават: източник на данни; получател; участник в протокола; начин на разпределяне на тайните.
Източникът на данни доказва авторството на заявителя на данните, приети от получателя. В процеса на обмен на данни възниква необходимостта за осигуряване на автентичността на източника на данни и дори след като протокола за аутентификация или дори сеансът на връзка е завършен.
Обект на аутентификация може да бъде получателят (получателите). Някои протоколи позволяват аутентифициране на един или няколко получателя.
Използването на участника в протокола като обект следва да докаже присъствието на заявеното лице, обекта или процеса на другия край на канала за връзка. За решаване на задачата е необходимо да се поддържа състояние на автентичност на участника в протокола след приключване на първичната му аутентификация, тъй като в противен случай е възможно подвключване на нарушител веднага след нейното завършване.
Последният класификационен признак е според начина на разпределение на секретите:
Значителна част от протоколите в стандартно изпълнение са свързани и постоянно се усъвършенстват. Този процес предопределя необходимостта от изследвания, насочени към разработване като цяло на методология и в частност на методики в областта на анализа на надеждността на протоколите, а също и построяване на безопасни протоколи за аутентификация.
В теорията и практиката са апробирани комплекс от решения, които могат да се разпределят в два клас:
Методи за построяване на атаката.
Методите за построяване на атаката могат да бъдат разделени от гледна точка на теоретичните им основи на три групи:
Методи, базирани на езици за проверка на правилнстта. Те анализират криптографския протокол като програма с цел доказване на неговата правилноет. Това се постига с определяне на протокола като краен автомат, с използване на изцхисления на предиката, или с помощта на алгебра на процесите.
В разработките [24,28], авторите Sidhu и Varadharajan свеждат протокола до модела на крайния автомат. Първият метод за анализ проверява основните свойства на поредицата протоколи, разкрива основните недостатъци, но не може да разкрие всички недостатъци поради многократното използване на стари съобщения, доколкото не се използват никакви времеви категории. Вторият метод също проверява основните свойства на поредицата протоколи, но показва много проблеми като увеличение броя на состоянията. Освен това, за да се избегнат недостатъците, свързани с многократното използоване на стари съобщения, авторите предлагат включване в съобщението за анализируемите протоколи на съдържанието на съобщенията от конкретния сеанс.
Друг подход, представен от Kemmerer, е основан на исчисляване на предикатите [18]. При този метод се използва езикът Ina Jo и Методологията за формално разработване (Formal Development Methodology - FDM). Ina Jo е непроцедурен език, твърденията на който са разширение на изчисленията на предикатите от първо ниво. Спецификаците, написани на този непроцедурен език, могат да се изпълняват и проверяват с помощта на инструментали средства от типа на Inatest. Този подход се оказва твърде удачен за разкриване както на активни, така и на пасивни атаки, а също при разкриване много уязвимите места на протоколите за аутентификация. Примечательно, что в рамках данного подхода злоумышленнику определяется отдельная роль, формализуемая в математической модели протокола.
Roscoe предлага по-строг подход за анализ и доказване устойчивостта на протоколите [22]. Подходът е основан на моделиране на действията на всички участници в протокола с открояване на главния участник и на злоумишленика. Предложеният метод може да бъде използван за формализиране и моделиране на съобщения, потоколи и злоумишленици, а също за използоване на случайни чиса за осигуряване "свежеста" на съобщенията.
J.C.Mitchell, M.Mitchell и Stern предлагат подход, основан на моделиране на всички състояния на протокола, наречен Mur [13]. Разработеният от тях инструментариум, за реализиране на този подход, позволява да се моделират протокола и неговите свойства на одноименен език. След специфицирането на протокола на езика Mur се проверяват всички състояния на всички участници в него и съобщенията.
Стандартизираният език LOTOS [9, 17] е използван за разработване на криптографически протоколи за аутентификации [15] и за проверка на устойчивостта им за отказ при нападения на злоумишленика. LOTOS е съставен от два основни компонента: алгебра на процесите със структурана операционна семантика и език за абстрактно описание на данните. LOTOS също е бил използован от Germeau и Leduc при разработване на протокола за двустранна аутентификация между довереното лице и ползвателя.
Всички описани по-горе подходи се използват за разкриване на нападения, предизвикани от недостатъчна яснота в описанието на съобщенията на протоколите. За съжаление следва да отбележим, че те страдат от големия размер на простаранството на състоянието при изследване на конкретния протокол. Освен това, ако методът не разкрива уязвимост в конкретния протокол, то това означава само, че зададеното пространство от предпоставки и изисквания отсъства атака на протокола, която може да се увенчая с успех по отношение на анализираната система. В същото время следва да се докаже, че при прилагане на протокола към система с по-голяма размерност или при количествено изменение на предпоставките, той е устойчив към определени нападения. Следва също да се докаже ефективността на посочените по-горе методи за анализ на протоколите по отношение на големите системи.
Методи за алгебраично опростяване на теоретичните модели. Тези методи моделират протокола чрез прилагане на набор от правила за преобразуване и съкращаване на алгебричните изрази, представящи съобщенията на протокола. Методте от тази група са разработени от Dolev и Yao [14], и Meadows [20].
Dolev и Yao предлaга базов модел с прилагане на модела на крайния автомат [14]. В рамките на предложения модел се описва протокола, а след това се въвежда понятие за нападащия и се осъществявя разносттранен анализ на возможностите за нападение на конкретния протокол. По този начин задачата на анализа на протокола се свежда до задача за търсене. Следва да се отбележе, че този подход е ефективен само по отношение на посочения кръг протоки. Но основният недостаток се състои в това, че е невозможно да се анализира състоянието на съобщението между двата етапа на протокола.
Подходът, предложен от Meadows е получил наименованието Анализатор на Протоколи (АП). Като базови предпоставки се използва също модела на крайния автомат. Инструментариумът за проверка на прототипа на протокола е написан на Прологе и има за цел откриване дефекти на протокола по задавани параметри.
Основна разлика между между двата разгледани подхода е тази, че ако решението на Dolev и Yao обработва протокола като автомат за генеритане на думи, то решението на Meadows го разглежда като автомат за генериране на думи, събития и доверителни отношения. Той разширява съществено функциите на моделирания краен автомат и неговите състояния. Освен това се осъществява фиксиране на състоянието на съобщението не само на всяка стъпка от протокола, но и в периодите между тях. АП Meadows е успешно приложен за разкриване на редица преди това неизвестни уязвими места в редица протоколи, а също и за доказване на вече известни и публикувани недостатъци.
Специални експертни системи и методи за построяване на сценарии. Една от най-ранните експертни системи, която е използвала подхода Dolev-Yao, е Разпитващия Модел на Милен (РММ) [21]. Инструмент за разпитване е програмната реализация, написаня на Пролог и включваща модела за изменения на состоянията на протокола. В същото време, в което моделът фиксира фазовите променливи на състоянието на злоумишленика, инструментариумът за търсене рекурсивно преглежда состоянията на сообщенията в търсене на уязвимоет. Освен това, инструментариумът за разпитване/изпитване има модул от решения на уравнения за шифровани съобщения, а така също и други оператори за моделиране състоянията на аутентификация. Участниците в протоколите се обозначават като крайни автомати, предаващи един на друг съобщения, които могат да бъдат прехванати от злоумишленика. Злоумишленникът може да осъществи върху тях краен брой операции (например, такива като пропуск без изменения, отстраняване, изменение, повторение и др.). Протоколът се приема за доказан, ако действията на злоумишленика немогут да изведат протокола от зададеното количество щатни състояния. В момента на разработката с помощта на тази система не са били открити нови атаки, но са били възпроизведени вече известни [18].
Методи за построяване на изводи.
Към този клас методи следва да бъдат отнесени два известни подхода. Това е преди всичко логистика BAN, предложена от Burrows, Abadi, Needham [12], и логистиката GNY, разработена от Gong, Needham и Yahalom [16].
Логистиката BAN е най-известнят инструмент за анализ на протоколи за аутентификация. Нейната идеология се основава на дългогодишните изследвания на природата на идентификацията и опита, натрупан в тази област. В рамките на този подход се правят множество предположения, но главното се състои в това, че всеки факт е производен на доверието и не трябва да бъде универсален. Цялата логика на BAN-моделите е основана на фактите на доверие, т.е. съобщенията от протокола за аутентификация се разглеждат от гледна точка "вярвам/невярвам". В рамките на дадения модел аутентификацията се разглежда като функция на целостносттаи и "свежестта" на съобщението. Необходимо е да се отбележи, че този модел е получил разпространение при разработване на проблемите на аутентификациита в информационните системи. С негова помощ са били разкрити недостатъците в редица известни протоколи, такива като Needham-Schroeder и CCITT X.509. Моделът е позволил да се разкрият излишните преобразувания в някои протоколи, в т.ч. Needham-Schroeder, Kerberos, Otway-Rees, CCITT X.509.
Днес де-факто логистиката BAN е стандарт в областта на анализа на протоколите и значителен брой от разработващите нови протоки за аутентификация посочват, че техните протоколи са доказани с помощта на логистиката BAN.
Логистиката BAN има и определени недостататъци и ограничения. Основнте проблеми са свързани с интерпретирането и използването на времеви параметри, а именно:
1. Един от основните недостатъци на логистиката е този, че тя разделя времето на две "епохи", при което се обуславя, че само съобщения, генерирани в сегашно време могат да бъдат свежи/нови. Всъщност това не е така. Могат да се посочат много примери, когато съобщенията, генерирани в миналото остават свежи и в настоящето.
2. Следващ недостатък е интерпретацията на отметката "дата-време". Логистиката по никакъв начин не определя реда за използване на срока, в течение на който съобщението е действително. Това обуславя някои проблеми при построяването на протоколите, свързани с използването на голям брой ключове.
3. Използваният в логистиката апарат предвижда, че часовниците на взаимодействащите си страни са синхронизирани и работят в единно времево пространство.
4. Протоколите трябва да бъдат кратки. В случая, ако протоколите са продължителни във времето, страните трябва да вярват на съобщенията в течение на целия протокол за аутентификации.
5. Логистиката BAN приема като едно от базовите допускания, криптосистемата не може да бъде разбита. Това е нормално допускане, което е опорена пункт/ стержнем за цялата криптографска система, но то може да се отнесе към недостатъците дори и за това, че трябва да бъде декларирано във вид на правила или допускания. В логистиката липсва както първото, така и второто.
Твърде успешен, но много по-сложен отколкото BAN, подход се използва в предложената Gong, Needham и Yaahalom [16] логистика, получила наименованието GNY. Този подход разглежда протокола в постъпков режиме, с предявяване на всяка стъпка на необходимите предположения и формира изводи за финалните състояния. Получените на предходния етапе изводи се приемат за базови при перехода към следващия етап. Логистиката GNY предоставя дополнителни преимущества в сравнение с логистиката BAN. Те се свеждат до това, че в рамките на анализа на протокола ясно се откроява разбирането на съдържанието и значението на съобщението, което позволява едновременно да се правят изводи за състоянието на протокола не отделно на всеки етапа, а комплексно, разглеждайки гокато процес, протичащ във времето. В съответствие с логиката GNY участниците могут да включват в сообщенията факти, в които те невярват, но с които те разполагат. Друго важно достижение е способносттра на участниците да разпознават получените съобщения и да идентифицират повторенията на прешестващите ги съобщения или съобщения, прехванати в рамките на други протоколи.
Въпреки че логистиката GNY е по-удачна, отколкото BAN, тя е по-слабо разпространена. Това е свързано, първо с това, че тя обхваща само проблемите на аутентификацията, оставяйки извън анализа проблемите за конфиденциалността. Второ, тя е много по-сложна, отколкото другите решения в тази област, а също также има голям брой правила, които следва да бъдат отчитани на всяка стъпка от анализа на протоколите.
Друга логика, получила наименованието SvO, е предложена от Syverson и Oorschot [26]. Тя е разработена с цел решаване на ограничения, наложени от разработените до това време логистики, а именно: от една страна, да се използват преимуществата на BAN и GNY, а също по-малко известните AT [6] и vO [27], от друга страна - да се формулира единнен подход. Авторите са предложили моделно-теоретична семантика, с помощта на която се олекотява разбирането и възприемането на посочената логики, и съответно нейното използване. Следва да се отбележи, че SvO е по-опростена, отколкото всички взети поотделно логики, на които тя е производна, и смята, че тя е по-изразителна по отношение на доказване правилността на протоколите [7].
Методи за построяване на доказателства.
Вече беше отбелязано, че методите за построяване на изводи не разглеждат конфиденциалността като задължителен параметър на съобщението на протокола. Те също изпитват недостига на чиста семантика, а понякога е трудно да се твърди еднозначно, че основаното на доверителните модели доказателство фактически доказва. От друга страна, при прилагане на методите за построяване на атаки на областта от възможни решения, в които е необходимо да се осъществи търсенето, нараства експоненциално с нарастване на размерите на протокола, съответно, изчислителните ресурси, необходими за анализа, могат да превишават достъпните.
За предотвратяване на посочените недостатъци Bolignano [8] предлага подход, който определя началото на развитието на т. нар. чевеко-четими доказателства. Този подход може да се използва като част от анализа на правилностт на протоколите или за изучаване на техните формални спецификации. Той предполага специална формализация на протоколите за аутентификация и ясно разделя участниците на надеждни и ненадеждни, а също дава точно описание на техните роли, доверителния модел и управляващите структури. В рамките на анализа се осъществява налагане на връзките и последователно се изпълняват операците с фиксиране на аутентификаторите, основани на времевите параметри. Използването на мощни инварианти, а също и аксиоматични знания за поведението на злоумшленика позволява да се направи анализ на протокола към процеса на изследоване на модалните състояния.
В рамките на подобен подхода Schneider в своята разработка [23] предлага метод за анализ на протоколи за аутентификация на езика CSP. Целта на неговата работа е да развитие собствена теория за анализ на протоколи, реализирана с помощта на семантиката на езика CSP, тъй като тази семантика позволява да се опише точно протокола за аутентификация в термините на съобщенията, передадени и получени от участниците в протокола. Този подход позволява да се обедини преимуществото на точното описание на съобщенията и участниците в протокола и возможността за точно, формално фиксиране на свойствата им.
Друго твърде интересно решение е подходът, предложен от Snekkenes в [25], който използва като основа теорията и инструментариума на автоматичното доказване на теоремите. В рамките на модела протоколът се разглежда като теорема, а целта на модела е да се докаже дадената теорема. Открояват се участниците, техните състояния, съобщенията, предавани между тях, използваните типове криптографски преобразования, а също множество возможни въздействия на нападащия. Теоремата се доказва чрез моделиране на действията на нападъщия протокола, и в случая, ако не е намерена успешна атака от страна на нападателя, се счита за доказана.
Формални езици за спецификация и средства за автоматизиран анализ на протоколи. Представените методи за анализ на протоколите имат свои достойнства и недостатъци. Некои от тях са получили по голямо разпространение, други - единично. Но е необходимо да се признае, че почти все те могат да бъдат използвани само от самите разработчици на тези модели. Основната причина е в това, че протоколите трябва да бъдат отново определяни за всяка прилагана методика за анализ, а това е твърде сложна задача, ако се отчита, че всеки подход използва своя система за обозначения, формализация и т.п. По този начин, възниква идеята за разработване на инструментални средства за автоматизиран анализ на протоколите.
Разработените системи могат да се разпределят в два класа: системи за автоматично преобразуване на протоколи и системи за техния автоматичен анализ.
Естествено е, че на входа на преобразователите е необходимо да се подава формализирана структура, но това може да се направи на вече добре описан, изучен и удобен език за специфициране. Това е обусловило и необходимостта от разработване на подобен език за формално описание на протоколи. Прилагането на подобен подход би позволило на изхода да се получи формализирано описание за всяка система за анализ на протоколите в необходимия вид и с използване на съответстваща на конкретния модел семантика. Ще разгледаме няколко решения в тази област.
През 1997 година Brackin разработва елементарен език за техническо описание на интерфейси (ISL - Interface Specification Language) и описва Автоматичен Анализатор на Протоколи за Аутентификация (AAPA - Automatic Authentification Protocol Analyzer), който може или автоматично да докаже, че конкретният протокол е правилен, или точно да откроява стъпка или състояние, където е нарушено доказателствоо [10,11]. AAPA може да се използва както отделно, така и като част от системата за доказателства. Система не само осъществява доказване на протокола, но предоставя на ползвателя графична представа на всяка стъпка от състоянието на всички компоненти. Това е твърде успешное решение, което може да се използва за анализ на протоколите, но неговото прилагане предполага наличието на значителни изчислителни ресурси.
С помощта на AAPA са били анализирани повече от 50 протокола, а резултатите, представен в обзорна разработка [11]. AAPA е непрекъснато развиваща се библиотека, в която се добавят нови видове атаки на протокол за аутентификация, а също и самите протоколи във формализиран, пригоден за анализ вид. Така с помощта на AAPA е возможно извършване на анализ на вече известните протоколи и тяхната модификация, а също на разработените отново. Това определя широкото разпространение и приложение в сфера като образованието, а също и на професионалното осигуряване на информационна безопасност.
Друг перспективeн eзик, предназначен за анализ на протоколи, е разработеният от Millen [21] език CAPSL (Common Authentication Protocol Specification Language). Основните цели на езика CAPSL са осигуряване на примственост, на необходимото (и, естествено, разумно) равнище на абстракция, завършеност на анализа и доказателствата, а също расширяемост. В последно време все по-често и по-често се наблюдават призиви за премане на езика CAPSL като стандарт за описание на протоколите.
Достаточно функционалeн инструмент, предназначен за автоматизиран анализ на протоколите за аутентификация, е програмният продукт, разработен от Lowe [19], и получил наименованието Casper. Това е полуавтоматичен анализатор от CSP тип, реализиращ на основата на абстрактното описание на протокола неговото моделиране и анализ. Като входни данни Casper получава CSP скриптове. Макар Casper да не покрива всички типове атаки на протоколите за аутентификация, той е приложен успешно при анализа на такива протоколи, като протоколът Andrew, Kerberos версия 5, протокол CCITT X.509, а също протоколът Yahalom.
Основната разлика между CAPSL и езикът Casper е тази, че ако първият изисква само формализирано описание на протокола, то вторият изисква еще и описание на системата, в която този протокол ще работи. Най-важното изискване на Casper е необходимостта от описание не само на съобщението и участниците, но и на техните роли в рамките на протокола.
Сравнително неотдавно, през 1998 г., M.Abadi и A.Gordon разработват езика Spi [5], предназначен за специфициране на криптографски протоколи, които са език за описание на мобилните изчисления, но не предвижда описание на операците по шифриране и разшифриране. В рамките на този език протоколите се представят като процеси, а техните свойства на защитеност са предстаени чрез използване на понятията за еквивалентност на протокола. Забележително е, че се разглежда не само автентичността на съобщението, но също и цялостността и конфиденциалността като задължителни характеристики на състоянието на защитеност на предаваните данни.
По-горе беше представен обзор на решения в областта на формалния анализ. И трите групи подходови са полезни на различните нива на абстракция на описанието на протоколите за аутентификация. Представените модели могат да бъдат използвани в ранните етапи на разработване на протоколи. Прилагането на инструментариума за разработване на протоколи позволява да се извърши многоетапен анализ. През първия етап се използват методите за построяване на изводи (например, такива като BAN), за определяне ролята на всяко съобщение в протокола, контрол на "свежести" на съобщението и др. През втория - методите за моделиране на атаки за бърза проверка на устойчивостта към известни атаки. Накрая се използва доказателствения подход за изследоване на по-детайлните свойства на протоколите.
Пявиха се и нови направления в изследванията, които не бяха разгледани е рамките на пососчената група, но при които се използват нетрадициопнни подходи, и които могат в близко бъдеще да дадат интересни резултати. Към тях могат да се отнесе подхода за анализ на протоколите в контекста на съблюдаване на изискванията на ITSEC за различните класове защитимост.
Други, твърде интересни подходи са описаните в [10,21], същността на които е в анализа на протоколите, специфицирани на специални езци за абстракция. В това направленивюе е разработен езикът PDL (Protocol Description Language), който съдържа не само специална терминология за описание на протоколите, но и апарат за тяхното доказателство. Още повече, даденият език има като допълнителна реализация интерпретацията на базовата специфика на протокола във формат CAPSL, което дава възможност за дополнителен анализ на неговите свойства с прилагане на други формални методи.
В заключение следва да отбележим, че в настояще време се наблюдава активна работа в областта на уточняване на методите за анализа на протоколите, ориентирани към приложение на Web-технологии и т.н.
Литература
1. Охрименко С.А., Черней Г.А. Угрозы безопасности автоматизированным информационным системам (программные злоупотребления). //Научно-техническая информация. Серия 1. Организация и методика информационной работы. - 1996, № 5, с.5-13.
2. Черней Г.А., Охрименко С.А., Ляху Ф.С. Безопасность автоматизированных информационных систем. - Кишинев: Ruxanda, 1996ю - 186 с.
3. Радев Е., Охрименко С., Черней Г. Информационното противостоене - възможности и оценка на риска.//Автоматика и информатика, 2000, № 2-3, с. 14-16.
4. Черней Г.А. Проблемы аутентификации в информационных системах. - Кишинев: Реклама, 2001. - 112 с.
5. Abadi M., Gordon A. A Calculus for Cryptographic Protocols: The Spi Calculus. Proceedings of the Fourth ACM Conference on Computers and Communications Security, (1997), 36-47, ACM Press.
6. Abadi M., Tuttle. Semantics for Logic of Authentication. Proceedings of the Tenth ACM Symposium on Principles of Distributed Computing, (1991), 201-216, CAN Press.
7. Anderson R. A Second Generation Wallet, ESORICS'92 Proceedings of the Second European Symposium on Research in Computer Security, (1992), 411-418, SpringerVerlag.
8. Bolignano D. An approach to the formal verification of cryptographic protocols. Proceedings of the Third ACM Conference on Computer and Communications Security.(1996), 106-118, ACM Press.
9. Bolognesi T., Bribksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems. (1987), vol.14, 25-59.
10. Brackin S. An Interface Specification Language for Automatically Analyzing Cryptographic Protocols. Proceedings of the 1997 Symposium on Network and Distributed System Security. (1997), 40-51. IEEE Computer Society Press.
11. Brackin S. Evaluating and Improving Protocol Analysis by Automatic Proof. Proceedings of the IEEE Computer Security Foundation Workshop XI .(1998), 138-152, IEEE Pres.
12. Burrows M., Abadi M., Needham R. A Logic of Authentication. ACM Transactions on Computer Systems. (1990), 8 (1), 18-36.
13. Dill D.L., Drexler A.J., Yang C.H. Protocol verification as a hardware design aid. Proceedings of the 1992 IEEE International Conference on Computer Design: VLSI in Computer and Processors. (1992), 522-525, IEEE Computer Society Press.
14. Dolev D., Yao A. On the Security of Public Key Protocols. IEEE Transactions on Information Theory. (1983), 29 (2), 198-208.
15. Germeau F., Leduc G. Model-based Design and Verification of security protocols using LOTOS. Proceedings of the 1997 DIMACS Workshop on Design and Formal Verification of Security Protocols. (1997), http://dimacs.rutgers.edu/Workshops/Security.
16. Gong L., Needham R., Yahalom R. Reasoning about Belief in Cryptographic Protocols. Proceedings of the 1990 IEEE Symposium on Security and Privacy. (1990), 234-248, IEEE Computer Society Press.
17. ISO/IEC Information Proceeding Systems - Open Systems Interconnection: LOTOS, a Formal Description Technique based on the Temporal Ordering of Observational Behaviour. IS8807, (1989).
18. Kemmerer R. Analysing encryption protocols using formal verification techniques. IEEE Journal on Selected Areas in Communications. (1989), 7(4), 448-457.
19. Lowe G., Casper. A Compiler for the Analysis of Security Protocols. Proceedings of the 1977 IEEE Computer Security Foundations Workshop X. (1997), 18-30. IEEE Computer Society Press.
20. Meadows C. The NRL Protocol Analyser: An overview. Journal of Logic Programming. (1996), Vol. 26, No. 2, 113-131.
21. Millen J. The Interrogator Model. Proceedings of the 1995 IEEE Symposium on Security and Privacy. (1995), 251-260. IEEE Computer Society Press.
22. Roscoe A.W. Modelling and verifying key-exchange protocols using CSP @ FDR. Proceedings of the 1995 IEEE Computer Security Foundations Workshop IX. (1995), 98-107. IEEE Computer Society Press.
23. Schneider S. Verifying Authentication Protocols with CSP. Proceedings of the IEEE Computer Security Foundations Workshop X. (1997), 3-17. IEEE Computer Society Press.
24. Sidhu D. Authentication Protocols for Computer Networks. Computer Networks and ISDN Systems. (1986), Vol. II, 297-310.
25. Snekkenes E. Formal Specification and Analysis of Cryptographic Protocols. Ph.D. Thesis, University of Oslo. (1995).
26. Syverson P., van Oorschot P.C. On unifying some Cryptographic Protocols. Proceedings of the 1990 IEEE Computer security Foundation Workshop YII. (1994), 14-29. IEEE Computer Society Press.
27. van Oorschot P.C. Extending Cryptographic Logics of Belief to Key Agreement Protocols. Proceedings of the First ACM Conference ob Computer and Communications Security. (1993), 232-243. ACM Press.
28. Varadharajan V. Verification of Network Security Protocols. Computers and Security. (1989), Vol. 8, 693-708, Elsevier Advanced Technology.