We show how a standard deck of playing cards can be used to implement a secure multiparty protocol to compute any boolean function. Our contribution to previous work: no identical copies of cards are needed, and the number of necessary cards is reduced.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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
Many network services and protocols can work correctly only when freshness of messages sent between participants is assured and when the protocol parties’ internal clocks are adjusted. In this paper we present a novel, secure and fast procedure which can be used to ensure data freshness and clock synchronization between two communicating parties. Next, we show how this solution can be used in other cryptographic protocols. As an example of application we apply our approach to the Internet Key Exchange (IKE) protocol family.
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ć.