Generalizing multi-party contract signing

in Proc. 4th Conference on Principles of Security and Trust (POST'15) (2015)

Multi-party contract signing (MPCS) protocols allow a group of signers to exchange signatures on a predefined contract. Previous approaches considered either completely linear protocols or fully parallel ... [more ▼]

Multi-party contract signing (MPCS) protocols allow a group of signers to exchange signatures on a predefined contract. Previous approaches considered either completely linear protocols or fully parallel broadcasting protocols. We introduce the new class of DAG MPCS protocols which combines parallel and linear execution and allows for parallelism even within a signer role. This generalization is useful in practical applications where the set of signers has a hierarchical structure, such as chaining of service level agreements and subcontracting. Our novel DAG MPCS protocols are represented by directed acyclic graphs and equipped with a labeled transition system semantics. We define the notion of abort-chaining sequences and prove that a DAG MPCS protocol satisfies fairness if and only if it does not have an abortchaining sequence. We exhibit several examples of optimistic fair DAG MPCS protocols. The fairness of these protocols follows from our theory and has additionally been verified with our automated tool. We define two complexity measures for DAG MPCS protocols, related to execution time and total number of messages exchanged. We prove lower bounds for fair DAG MPCS protocols in terms of these measures. [less ▲]

Attack-Defense Trees

in Journal of Logic and Computation (2012)

Attack-defense trees are a novel methodology for graphical security modeling and assessment. They extend the well known formalism of attack trees by allowing nodes that represent defensive measures to ... [more ▼]

Attack-defense trees are a novel methodology for graphical security modeling and assessment. They extend the well known formalism of attack trees by allowing nodes that represent defensive measures to appear at any level of the tree. This enlarges the modeling capabilities of attack trees and makes the new formalism suitable for representing interactions between an attacker and a defender. Our formalization supports different semantical approaches for which we provide usage scenarios. We also formalize how to quantitatively analyze attack and defense scenarios using attributes. [less ▲]

Insider Attacks and Privacy of RFID Protocols

in EuroPKI 2011 (2012)

Security protocols for Secret Santa

in Proc. 18th Security Protocols Workshop (2010)

EC-RAC: Enriching a Capacious RFID Attack Collection

in 6th Workshop on RFID Security (RFIDSec 2010) (2010)

On a new formal proof model for RFID location privacy

in Information Processing Letters (2009), 110(2), 57-61

Security of RFID protocols - A case study

in Electronic Notes in Theoretical Computer Science (2009), 244

Minimal message complexity of asynchronous multi-party contract signing

in Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF'09) (2009)

Towards a decision model based on trust and security risk management. In Ljiljana Brankovic and Willy Susilo

in Seventh Australasian Information Security Conference (AISC 2009) (2009)

Chosen-name attacks: An overlooked class of type-flaw attacks

in Electronic Notes in Theoretical Computer Science (2008), 197(2), 31-43

In the context of Dolev-Yao style analysis of security protocols, we consider the capability of an intruder to dynamically choose and assign names to agents. This capability has been overlooked in all ... [more ▼]

In the context of Dolev-Yao style analysis of security protocols, we consider the capability of an intruder to dynamically choose and assign names to agents. This capability has been overlooked in all significant protocol verification frameworks based on formal methods. We identify and classify new type-flaw attacks arising from this capability. Several examples of protocols that are vulnerable to this type of attack are given, including Lowe’s modification of KSL. The consequences for automatic verification tools are discussed. [less ▲]