PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników
Powiadomienia systemowe
  • Sesja wygasła!

Znaleziono wyników: 11

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  security protocols
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available Security Verification in the Context of 5G Sensor Networks
Remlein Piotr, Stachowiak Urszula
Journal of Telecommunications and Information Technology
|
2021
|
nr 2
107--119
EN
In order to develop reliable safety standards for 5G sensor networks (SN) and the Internet of Things, appropriate verification tools are needed, including those offering the ability to perform automated symbolic analysis process. The Tamarin prover is one of such software-based solutions. It allows to formally prove security protocols. This paper shows the modus operandi of the tool in question. Its application has been illustrated using an example of an exchange of messages between two agents, with asynchronous encryption. The scheme may be implemented, for instance, in the TLS/DTLS protocol to create a secure cryptographic key exchange mechanism. The aim of the publication is to demonstrate that automated symbolic analysis may be relied upon to model 5G sensor networks security protocols. Also, a use case in which the process of modeling the DTLS 1.2 handshake protocol enriched with the TCP SYN Cookies mechanism, used to preventing DoS attacks, is presented.
2
Użycie czasowych automatów probabilistycznych do modelowania protokołów zabezpieczających
Siedlecka-Lamch O.
Studia Informatica
|
2017
|
Vol. 38, nr 3
191--201
PL
Czasowe automaty probabilistyczne mogą zostać użyte do modelowania i weryfikacji systemów przetwarzanych w czasie rzeczywistym i posiadających cechy probabilistyczne. Biorąc pod uwagę stochastyczne zachowania komunikacji w sieci, można znaleźć wspólne cechy protokołów i automatów. Modelowanie z wykorzystaniem automatów umożliwia użycie relacji i algorytmów, takich jak bisymulacja czy minimalizacja. To może ułatwić weryfikację/uproszczenie protokołów.
EN
Probabilistic timed automata can be used for modeling and verification of systems whose characteristic is real-time and probabilistic. Analyzing stochastic behavior of network communication, many common points of security protocols and automata can be easily found. Modeling with automata allows to use relations and algorithms, such as bisimulation or minimization. This can lead to verification/simplification protocols.
3
Analiza i symulacje czasowych protokołów zabezpieczających
Szymoniak S.
Studia Informatica
|
2017
|
Vol. 38, nr 2
55--66
PL
W pracy zawarto opis problemu weryfikacji czasowych protokołów zabezpieczających przy uwzględnieniu opóźnień w sieci. Za pomocą specjalnie skon-struowanego modelu formalnego, który stał się podstawą do implementacji narzędzia, możliwe jest obliczanie czasu poprawnego wykonania protokołu. Narzędzie umożli-wia przeprowadzenie badań czasowych protokołów zabezpieczających, w tym prze-prowadzenie symulacji.
EN
This paper contains a description of the problem of timed security pro-tocols verification, taking into account delays in the network. Using a specially con-structed formal model, which became the basis for the implementation of the special tool, it is possible to calculate the correct time of execution protocol. The tool enables testing timed security protocols, including simulations.
4
Weryfikacja protokołów zabezpieczających z uwzględnieniem opóźnień w sieci
Szymoniak S.
Studia Informatica
|
2016
|
Vol. 37, nr 1
71--82
PL
W pracy zawarto opis problemu modelowania i weryfikacji czasowych protokołów zabezpieczających z uwzględnieniem opóźnień w sieci. Specyfikacje protokołów są zapisane w formacie ProToc, który umożliwia pełną specyfikację czasowego protokołu. Integralną częścią tej pracy jest zaprojektowane i zaimplementowane narzędzie, służące weryfikacji czasowych protokołów zabezpieczających. Narzędzie warunkuje określenie podatności danego protokołu zabezpieczającego na ataki, przy uwzględnieniu opóźnień w sieci.
EN
This paper contains a description of the problem for modeling and verification of timed security protocols including delays in the network. Protocol specifications are written in the format ProToc, which allows full specification of the timed protocol. An integral part of this work is to designed and implemented tool for verifying time network security protocols. This tool allows specifying a particular protocol security vulnerability to attacks, taking into account the delays in the network.
5
Content available A Survey of Energy Efficient Security Architectures and Protocols for Wireless Sensor Networks
Daniluk K., Niewiadomska-Szynkiewicz E.
Journal of Telecommunications and Information Technology
|
2012
|
nr 3
64-72
EN
Data security and energy aware communication are key aspects in design of modern ad hoc networks. In this paper we investigate issues associated with the development of secure IEEE 802.15.4 based wireless sensor networks (WSNs) - a special type of ad hoc networks. We focus on energy aware security architectures and protocols for use in WSNs. To give the motivation behind energy efficient secure networks, first, the security requirements of wireless sensor networks are presented and the relationships between network security and network lifetime limited by often insufficient resources of network nodes are explained. Second, a short literature survey of energy aware security solutions for use in WSNs is presented.
6
Content available remote 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.
7
Content available remote 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.
8
Content available remote 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).
9
Content available remote Verifying Security Protocols Modelled by Networks of Automata
Kurkowski M., Penczek W.
Fundamenta Informaticae
|
2007
|
Vol. 79, nr 3-4
453-471
EN
In this paper we show a novel method for modelling behaviours of security protocols using networks of communicating automata in order to verify them with SAT-based bounded model checking. These automata 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.
10
Content available remote 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.
11
Content available remote 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.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.