PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

Użycie czasowych automatów probabilistycznych do modelowania protokołów zabezpieczających

Identyfikatory
Warianty tytułu
EN
Use of probabilistic timed automata for security protocols modeling
Języki publikacji
PL
Abstrakty
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.
Czasopismo
Rocznik
Strony
191--201
Opis fizyczny
Bibliogr. 19 poz.
Twórcy
  • Czestochowa University of Technology, Institute of Computer Sciences and Information Sciences, ul. Dąbrowskiego 73, 42-201 Czestochowa, Poland
Bibliografia
  • 1. Alur R., Dill D.: A Theory of Timed Automata. Theoretical Computer Science 126, 1994, s. 183÷235.
  • 2. Anderson R.J. and Needham R.M.: Programming Satan’s Computer. Computer Science Today-Commemorative Issue. Lecture Notes in Computer Science, vol. 1000, Springer-Verlag, Berlin Germany 1995, s. 426÷441.
  • 3. Armando A., et. al.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. Proceedings of 17th Int. Conf. on Computer Aided Veriffcation CAV’05, LNCS, vol. 3576, Springer, 2005, s. 281÷285.
  • 4. Bengtsson J., Yi W.: Timed Automata: Semantics, Algorithms and Tools. In Lectures on Concurrency and Petri Nets, Lecture Notes in Computer Science, vol. 3098, Springer, 2013, s. 87÷124.
  • 5. Blanchet B.: Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security, 1(1-2), 2016, s. 1÷135.
  • 6. Cremers C.: The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. Proceedings CAV’08, vol. 5123, 2008, s. 414÷418.
  • 7. Dembinski P., Janowska A., Janowski P., Penczek W., Polrola A., Szreter M., Wozna B., Zbrzezny A.: VerICS: A Tool for Verifying Timed Automata and Estelle Specifications. Proceedings of 9th Int. Conf. TACAS’03, LNCS, vol. 2619, Springer-Verlag, 2003, s. 278÷283.
  • 8. Kurkowski, M., Penczek, W.: Verifying Security Protocols Modelled by Networks of Automata. Fundamenta Informaticae, vol. 79 (3-4), 2007, s. 453÷471.
  • 9. Kurkowski M., Siedlecka-Lamch O., Dudek P.: Using Backward Induction Techniques in (Timed) Security Protocols Verification. Proceedings of 12th Int. Conf. CISIM 2013, Lecture Notes in Computer Science, vol. 8104, Krakow Poland 2013, s. 265÷276.
  • 10. Kwiatkowska M., Norman G., Parker D., Sproston J.: Performance Analysis of Probabilistic Timed Automata Using Digital Clocks. Formal Methods in System Design, vol. 29 (1), 2006, s. 33÷78.
  • 11. Kwiatkowska M., Norman G., Segala R., Sproston J.: Automatic Verification of Realtime Systems with Discrete Probability Distributions. Theoretical Computer Science, vol. 282, 2002, s. 101÷150.
  • 12. Kwiatkowska M., Norman G., Sproston J., Wang F.: Symbolic Model Checking for Probabilistic Timed Automata. Information and Computation, vol. 205(7), 2007, s. 1027÷1077.
  • 13. Lowe G.: Breaking and Fixing the Needham-Schroeder Public-key Protocol Using fdr. In TACAS, LNCS, Springer, 1996, s. 147÷166.
  • 14. Lowe G.: Some New Attacks Upon Security Protocols, IEEE Computer Society Press. Proceedings of the Computer Security Foundations Workshop VIII, 1996.
  • 15. Norman G., Parker D., Sproston J.: Model Checking for Probabilistic Timed Automata. Formal Methods in System Design 43(2), 2013, s. 164÷190.
  • 16. Siedlecka-Lamch O., Kurkowski M., Piatkowski J.: Using Probabilistic Automata for Security Protocols Verification. Journal of Applied Mathematics and Computational Mechanics, vol. 15, issue 2, 2016, s. 125÷131.
  • 17. Siedlecka-Lamch O., Kurkowski M., Piatkowski J.: Probabilistic Model Checking of Security Protocols without Perfect Cryptography Assumption. Proceedings of 23rd International Conference on Computer Networks, Brunow, Poland, Communications in Computer and Information Science, vol. 608, Springer-Verlag, 2016, s. 107÷117.
  • 18. Sokolova A., de Vink E.: Probabilistic Automata: System Types, Parallel Composition and Comparison. Validation of Stochastic Systems: A Guide to Current Research, LNCS vol. 2925, 2004, s. 1÷43.
  • 19. Szymoniak S., Siedlecka-Lamch O., Kurkowski M.: Timed Analysis of Security Protocols. Proceeding of 37th International Conference ISAT 2016, Advances in Intelligent Systems and Computing, vol. 522, Springer, Karpacz Poland 2016, s. 53÷63.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-5a74f142-5300-4a43-9d66-ff30b622a44d
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ć.