Wyniki wyszukiwania - BazTech

1

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}.

2

Timed automata based model checking of timed security protocols

Kurkowski M., Penczek W.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2008

|

nr 1010

1-36

EN

A new approach to verification of timed security protocols is given. The idea consists in modelling a finite number of users (including an intruder) of the computer network and their knowledge about secrets by timed automata. The runs of the product automaton of the above automata correspond to all the behaviours of the protocol for a fixed number of sessions. Verification is performed using the module BMC of the tool VerICS.

PL

W pracy przedstawiono nową metodę weryfikacji czasowych protokołów kryptograficznych. Sko\'nczona liczba użytkowników sieci oraz ich wiedza podczas wykonywania protokołu są modelowane przy pomocy automatów czasowych. Sieć automatów w pełni odzwierciedla zachowania podczas wykonywania protokołu niezbędne do weryfikowania założonych własności. Weryfikacja przeprowadzana jest za pomocą modułu BMC narzędzia VerICS.

3

Verifying Security Protocols Modeled by Networks of Automata

Kurkowski M., Penczek W.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2007

|

Nr 998

1-38

EN

In this paper we show a novel method for modelling behaviours of security protocols using networks of communicating autornata in order to verify them with SAT-based bounded model checking. These autornata correspond to executions of the participants as well as to their knowledge about letters. Given a bounded number of sessions, we can verify both correctness or incorrectness of a security protocol proving either reachability or unreachability of an undesired state. We exemplify all our notions on the Needham Schroeder Public Key Authentication Protocol (NSPK) and show experimental results for checking authentication using the verification tool VerICS.

PL

Praca prezentuje nowa metodę modelowania wykonań protokołów kryptograficznych za pomocą sieci synchronizujacych się automatów. Problem badania własności protokołów został sprowadzony do problemu testowania osiagalności odpowiednich stanów globalnych w sieci. Do badań wykorzystuje się algorytmy SAT i narzędzie VerlCS. Jako przykład opisano budowę sieci automatów dla protokołu Needhama Schroedera (NSPK). Przedstawiono również pierwsze wyniki eksperymentalne oraz pierwsze porównania z wynikami uzyskanymi przy użyciu narzędzia SAT-MC (AVISPA).

4

Model checking security protocols : a multi-agent system approach

Lomuscio A., Penczek W.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2007

|

Nr 1000

1-23

EN

We present a formalism for the automatic verification of security protocols based on multi-agent systems semantics. We give syntax and semantics of a temporal-epistemic security-specialised logie and provide a lazy-intruder model for the protocol rules that is arguably particularly suitable for verification purposes. We exemplify the techniąue by finding a (known) bug in the traditional NSPK protocol

PL

Praca prezentuje nowe podejście do automatycznej weryfikacji protokołów kryptograficznych, bazujące na semantyce systemów wieloagentowych. Podajemy składnię i semantykę temporalno-epistemicznej logiki dla protokołów kryptograficznych oraz model intruza typu "lazy", który jest szczególnie właściwy dla celów weryfikacji. Nasza technika jest przedstawiona na przykladzie protokołu NSPK, dla którego znajdujemy znany atak.

5

A model to specify security protocols on the ISDN

Mengual L., Barcia N., Fernandez C., Morant F., Yaguez J.

Journal of Applied Computer Science

|

1999

|

Vol. 7, nr 2

7-29

EN

In this paper, a general model to incorporate security services in the Integrated Services Digital Network (ISDN) is proposed. As an example to prove the model, a security protocol based on public key encryption is proposed. The data units of the security protocol are incorporated to the network layer protocol, Q.93I, as an integrating part of the "user-user" information element content in the USER INFORMATION, SETUP and ALERTING messages. The main objective is to distribute session keys between final applications to obtain a secure channel through the ISDN. The process is completely transparent both to users and applications. The complete description of the interchanges made by the Q.931 protocol incorporating the proposed security protocol has been formally specified in LOTOS.