Accueil

Stylianos Basagiannis

  1. Quantitative Analysis for Authentication of Low-cost RFID Tags.

    Wed, 12/07/2011 - 15:01 — SomNambul
    Authors: Stylianos Basagiannis, Ioannis Paparrizos, Sophia Petridou
    Subjects: Networking and Internet Architecture
    Abstract

    Formal analysis techniques are widely used today in order to verify and
    analyze communication protocols. In this work, we launch a quantitative
    verification analysis for the low- cost Radio Frequency Identification (RFID)
    protocol proposed by Song and Mitchell. The analysis exploits a Discrete-Time
    Markov Chain (DTMC) using the well-known PRISM model checker. We have managed
    to represent up to 100 RFID tags communicating with a reader and quantify each
    RFID session according to the protocol's computation and transmission cost
    requirements.

  2. Attacking an OT-Based Blind Signature Scheme.

    Wed, 11/11/2009 - 16:01 — SomNambul
    Authors: Stylianos Basagiannis, Panagiotis Katsaros, Andrew Pombortsis
    Subjects: Cryptography and Security
    Abstract

    In this paper, we describe an attack against one of the
    Oblivious-Transfer-based blind signatures scheme, proposed in [1]. An attacker
    with a primitive capability of producing specific-range random numbers, while
    exhibiting a partial MITM behavior, is able to corrupt the communication
    between the protocol participants. The attack is quite efficient as it leads to
    a protocol communication corruption and has a sound-minimal computational cost.
    We propose a solution to fix the security flaw.

  3. State Space Reduction with Message Inspection in Security Protocol Model Checking.

    Wed, 09/02/2009 - 12:02 — SomNambul
    Authors: Stylianos Basagiannis, Panagiotis Katsaros, Andrew Pombortsis
    Subjects: Cryptography and Security
    Abstract

    Model checking is a widespread automatic formal analysis that has been
    successful in discovering flaws in security protocols. However existing
    possibilities for state space explosion still hinder analyses of complex
    protocols and protocol configurations. Message Inspection, is a technique that
    delimits the branching of the state space due to the intruder model without
    excluding possible attacks. In a preliminary simulation, the intruder model
    tags the eavesdropped messages with specific metadata that enable validation of
    feasibility of possible attack actions.

Math-arch

Syndicate content