Wyniki wyszukiwania - Biblioteka Nauki

1

Verifying Timed Properties of Security Protocols

100%

Jakubowska G. , Penczek W.

|

tom 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

2

Bounded Model Cheking for Interpreted Systems

100%

Penczek W. , Lomuscio A.

|

tom Nr 946

1-8

EN

We present an extension of a bounded model checking algorithm to deal with temporal epistemic formulas. We use the algorithm to solve a variant of the bit transmission problem

PL

W pracy przedstawiamy rozszerzenie algorytmu ograniczonej weryfikacji modelowej do temporalnych formuł epistemicznych. Algorytm jest zastosowany do weryfikacji pewnego wariantu problemu transmisji bitów.

3

SAT-Based Bounded Model Checking for the Universal Fragment of TCTL

80%

Penczek W. , Woźna B. , Zbrzezny A.

|

tom Nr 947

1-26

EN

Bounded Model Checking (BMC) based on SAT methods consists in searching for a counterexample of a particular length and to generate a propositional formula that is satisfiable iff such a counterexample exists. Our paper shows how the concept of bounded model checking can be extended to deal with \TACTL\ (the universal fragment of \TCTL ) properties of a network of concurrent Timed Automata.

PL

Ograniczona Weryfikacja Modelowa, bzaująca na metodach SAT, polega na poszukiwaniu kontrprzykładów o długości ograniczonej przez pewną liczbę całkowitą k > 0 oraz generowanie formuły zdaniowej, która jest spełniana wtedy i tylko wtedy, gdy taki kontrprzykład istnieje. Celem tej pracy jest przedstawienie koncepcji ograniczonej weryfikacji modelowej dla automatów czasowych reprezentowanych przez siec współbieżnych i wzajemnie komunikujących się komponentów oraz własności wyrażanych w języku logiki TACTL (uniwersalnego fragmentu TCTL).

4

Reachability Analysis for Timed Automata Based on Partitioning

80%

Półrola A. , Penczek W. , Szreter M.

|

tom Nr 961

1-23

EN

Model checking is an approach commonly applied for automated verification of reachability properties. Given a system $S$ and a property $p$, reachability model checking consists in an exploration of the state space of $S$, checking whether there exists a state where $p$ holds. Since concrete state spaces (models) of timed systems are usually infinite, they cannot be directly applied to model checking. One of the solution to this problem is to exploit finite abstract models, preseving the properties of interest. The paper presents a new method of buildng abstract models for Timed Automata, based on a partitioning algorithm. Our pseudo-bisimulating models are often smaller than forward-reachability graphs , commonly used in reachability analysis. The method enables verification on-the-fly, i.e., generating of the model can be stopped as soon as a state satisfying $p$ is found.

PL

Automatyczne testowanie osiągalności wykonywane jest zazwyczaj za pomocą metod weryfikacji modelowej. Dla danego systemy S i właściwości p polega ono na przejrzeniu przestrzeni stanów S i sprawdzeniu, czy zawiera ona stan w którym p zachodzi. Istotne znaczenie ma zatem rozmiar przeglądanej przestrzeni (modelu), który w wielu przypadkach (np. dla systemów z czasem) może być nawet nieskończony. Jednym z możliwych rozwiązań jest zastosowanie skończonych modeli abstrakcyjnych zachowujących żądane własności. Praca przedstawia nową metodę generowania modeli abstrakcyjnych dla automatów czasowych, bazujących na algorytmie minimalizacji (podziału). Otrzymywane modele pseudobisymulacyjne zachowują osiągalność, a przy tym są często mniejsze niż używane zwykle do jej testowania tzw. grafy forward-reachability. Metoda pozawala też na wykonywanie weryfikacji "w locie", tj. przerywanie budowania modelu gdy wygenerowany zostanie stan spełniający p.

5

Checking Reachability Properties for Timed Automata via SAT

80%

Woźna B. , Penczek W. , Zbrzezny A.

|

tom Nr 949

1-19

EN

The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a state satisfying some desired property, first the transition relation of a timed automaton is unfolded to the depth k Î N and encoded as a prepositional formula. Next the desired property is translated to a prepositional formula and the satisfiability of the conjunction of the two above defined formulas is checked. The unfolding of the transition can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. The efficiency of the method is strongly supported by the experimental results. Keywords : Reachability problem, bounded model checking, translation to SAT, Timed Automata, Augmented Region Graphs, discretization.

PL

Testowanie osiągalności automatów czasowych z wykorzystaniem SAT. Praca opisuje nowe podejście do problemu osiągalności dla automatów czasowych. Główna idea polega na połączeniu znanego algorytmu przeszukującego przestrzeń stanów wszerz metodą BFS oraz metody ograniczonej weryfikacji modelowej. Aby sprawdzić, czy stan spełniający daną własność jest osiągalny w modelu dla rozważanego automatu czasowego postępujemy następująco. Rozwijamy stopniowo relację przejścia dla automatu, aż do głębokości k Î N i kodujemy ją jako formułę zdaniową. Następnie, za pomocą formuły zdaniowej kodowana jest rozważana własność i sprawdzana jest spełnialność koniunkcji obydwu zdefiniowanych formuł zdaniowych. Rozwijanie relacji przejścia może zostać zakończone jeśli poszukiwany stan został znaleziony lub wszystkie stany danego automatu czasowego zostały przeszukane.

6

Runtime Monitoring of Contract Regulated Web Services

80%

Lomuscio A. , Penczek W. , Solanki M. , Szreter M.

|

tom Vol. 111, nr 3

339-353

EN

We investigate the problem of locally monitoring contract regulated behaviours in agentbased web services. We encode contract clauses in service specifications by using extended timed automata. We propose a non intrusive local monitoring framework along with an API to monitor the fulfillment (or violation) of contractual obligations. A key feature of the framework is that it is fully symbolic thereby providing a scalable solution to monitoring. At runtime execution steps generated by the service are passed as input to the runtime monitor. Conformance of the execution against the service specification is checked using a symbolically represented extended timed automaton. This allows us to monitor service behaviours over large state spaces generated by multiple, long running contracts. We illustrate our methodology by monitoring a service composition scenario from the vehicle repair domain, and report on the experimental results.