Wyniki wyszukiwania - BazTech

1

Simulation of Security Protocols based on Scenarios of Attacks

Jakubowska G., Dembiński P., Penczek W., Szreter M.

Fundamenta Informaticae

|

2009

|

Vol. 93, nr 1-3

185-203

EN

In this paper we offer a methodology allowing for simulation of security protocols, implemented in the higher-level language Estelle, using scenarios designed for external attacks. To this aim we apply a translation of specifications of security protocols from Common Syntax to Estelle and an encoding of schemes of attacks into Estelle scenarios. We show that such an intelligent simulation may efficiently serve for validating security protocols.

2

Towards Scenarios of External Attacks upon Security Protocols

Dembiński P., Jakubowska G., Penczek W.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2008

|

nr 1012

1-24

EN

In this paper we consider a taxonomy of external attacks on security protocols in terms of a message origin and destination in addition to a session and step number. We use this taxonomy for designing algorithms, which for a given type of attack and parameters of the protocol return a scenario of an attack of this type. This way we can dramatically reduce the number of protocol runs to be generated in order to look for an attack upon a protocol in the process of verification or simulation. We show that our algorithms generate scenarios of attacks upon all the protocols, classified within our taxonomy, which are known to susceptible to these attacks. We exemplify the results of our algorithms for several protocols from \cite{SPORE} and \cite{CJ}.

PL

Rozważamy taksonomię zewnętrznych ataków na protokoły kryptograficzne w terminach nazwy wysyłającego i odbierającego wiadmość oraz numeru kroku i sesji. Używamy tej taksonomii do zaprojektowania algorytmów, które dla zadanego typu ataku i parametrów protokołu, zwracają scenariusze ataku tego typu. W ten sposób bardzo istotnie redukujemy liczbę przebiegów protokołu, które mają byc wygenerowane w celu poszukiwania ataku na protokół w procesie weryfikacji lub symulacji W Raporcie jest pokazane, że nasze alorytmy generują scenariusze ataków na protokoły, sklasyfikowane w naszej taksonomii, na które istnieją ataki tego typu. Wyniki zastosowania algorytmów prezentujemy na przykładzie kilku protokołów z \cite{SPORE} i \cite{CJ}.

3

Modelling and Checking Timed Authentication of Security Protocols

Jakubowska G., Penczek W.

Fundamenta Informaticae

|

2007

|

Vol. 79, nr 3-4

363-378

EN

In this paper we offer a novel methodology for verifying correctness of (timed) security protocols. The idea consists in computing the time of a correct execution of a session and finding out whether the Intruder can change it to shorter or longer by an active attack. Moreover, we generalize the correspondence property so that attacks can be also discovered when some time constraints are not satisfied. An implementation of our method is described. As case studies we verify generalized (timed) authentication of KERBEROS, TMN, Neumann Stubblebine Protocol, Andrew Secure Protocol, Wide Mouthed Frog, and NSPK.

4

Verifying Timed Properties of Security Protocols

Jakubowska G., Penczek W.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2006

|

Nr 991

1-38

EN

In this paper we offer a methodology for verifying correctness of (timed) security protocols whose actions are parametrised with time. To this aim the model of a protocol involves delays and timeouts on transitions, and sets time constraints on actions to be executed. Our approach consists in specifying a security protocol, possibly with timestamps, in a higher-level language and translating automatically the specification to a timed automaton (or their networks). Moreover, we generalise the correspondence property so that attacks can be also discovered when some time constraints are not satisfied. Then, one can use each of the verification tools for timed automata (e.g., Kronos, UppAal, or Yerics) for model checking generalised time authentication of security protocols. As a case study we verify generalised (timed) authentication of KERBEROS, TMN, Neuman Stubblebine, and Andrew Secure Protocol.

PL

Weryfikacja własności zależnych od czasu dla protokołów uwierzytelniania stron. Proponujemy metodologię weryfikacji poprawności (czasowych) protokołów kryptograficznych, których akcje parametryzowane są czasem. W tym celu do modelu protokołu wprowadzone zostały opóźnienia, oczekiwania na tranzycjach oraz ustalone zostały ograniczenia czasowe dla akcji. Nasze podejście polega na specyfikacji protokołu (mogącego zawierać znaczniki czasu) w języku wysokiego poziomu i automatycznej translacji tej specyfikacji do automatu czasowego (lub do sieci automatów czasowych). Ponadto uogólniamy własność "correspondence" w taki sposób, by umożliwić wykrycie ataków, gdy pewne czasowe ograniczenia nie będą spełnione. Dzięki temu, korzystając z dowolnego narzędzia do weryfikacji automatów' czasowych (np. Kronos, UppAal, Yerics) możliwe jest sprawdzenie czy w modelu spełniona jest uogólniona czasowa własność uwierzytelnienia dla protokołów kryptograficznych. Jako przykłady przedstawiamy weryfikację protokołów KERBEROS, TMN, Neuman Stubblebine i Andrew Secure Protocol

5

Formalne metody analizy kryptograficznych protokołów uwierzytelniania przy zastosowaniu kolorowych sieci Petriego

Jakubowska G., Pejaś J.

Zeszyty Naukowe. Automatyka / Politechnika Śląska

|

2000

|

z. 130

53-64

PL

W artykule została przedstawiona propozycja zastosowania kolorowanych sieci Petri do opisu modeli protokołów uwierzytelniania, oraz modeli intruzów, atakujących analizowany protokół. Narzędzia będące rezultatem ich zastosowania wymagają jednak aktywnej współpracy weryfikatora, który na ich podstawie jest w stanie ocenić stopień bezpieczeństwa protokołu oraz budować bazę wiedzy intruza.

EN

In this paper we present an approach to model authenticating protocols and intruders inside analyzing system using Coloured Petri Nets. However, tools based on the CP-Nets need active human-verifier assistance, who can estimate a degree of security of analyzing protocol and build intruder's database of knowledge.