Search

Your search keyword '"Radomirovic, Sasa"' showing total 48 results
Start Over Author "Radomirovic, Sasa"
48 results on '"Radomirovic, Sasa"'

1. On the Design and Security of Collective Remote Attestation Protocols

Author

Ahmadi, Sharar, Le-Papin, Jay, Chen, Liqun, Dongol, Brijesh, Radomirovic, Sasa, and Treharne, Helen

Subjects
Computer Science - Cryptography and Security
Abstract

Collective remote attestation (CRA) is a security service that aims to efficiently identify compromised (often low-powered) devices in a (heterogeneous) network. The last few years have seen an extensive growth in CRA protocol proposals, showing a variety of designs guided by different network topologies, hardware assumptions and other functional requirements. However, they differ in their trust assumptions, adversary models and role descriptions making it difficult to uniformly assess their security guarantees. In this paper we present Catt, a unifying framework for CRA protocols that enables them to be compared systematically, based on a comprehensive study of 40 CRA protocols and their adversary models. Catt characterises the roles that devices can take and based on these we develop a novel set of security properties for CRA protocols. We then classify the security aims of all the studied protocols. We illustrate the applicability of our security properties by encoding them in the tamarin prover and verifying the SIMPLE+ protocol against them.

Published
2024

2. Tactics for Account Access Graphs

Author

Arnaboldi, Luca, Aspinall, David, Kolb, Christina, Radomirović, Saša, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Tsudik, Gene, editor, Conti, Mauro, editor, Liang, Kaitai, editor, and Smaragdakis, Georgios, editor

Published
2024
Full Text
View/download PDF

3. Dispute Resolution in Voting

Author

Basin, David, Radomirovic, Sasa, and Schmid, Lara

Subjects
Computer Science - Cryptography and Security
Abstract

In voting, disputes arise when a voter claims that the voting authority is dishonest and did not correctly process his ballot while the authority claims to have followed the protocol. A dispute can be resolved if any third party can unambiguously determine who is right. We systematically characterize all relevant disputes for a generic, practically relevant, class of voting protocols. Based on our characterization, we propose a new definition of dispute resolution for voting that accounts for the possibility that both voters and the voting authority can make false claims and that voters may abstain from voting. A central aspect of our work is timeliness: a voter should possess the evidence required to resolve disputes no later than the election's end. We characterize what assumptions are necessary and sufficient for timeliness in terms of a communication topology for our voting protocol class. We formalize the dispute resolution properties and communication topologies symbolically. This provides the basis for verification of dispute resolution for a broad class of protocols. To demonstrate the utility of our model, we analyze a mixnet-based voting protocol and prove that it satisfies dispute resolution as well as verifiability and receipt-freeness. To prove our claims, we combine machine-checked proofs with traditional pen-and-paper proofs.

Published
2020

5. A Formal Analysis of 5G Authentication

Author

Basin, David, Dreier, Jannik, Hirschi, Lucca, Radomirović, Saša, Sasse, Ralf, and Stettler, Vincent

Subjects
Computer Science - Cryptography and Security, D.4.6, D.2.4, C.2.2
Abstract

Mobile communication networks connect much of the world's population. The security of users' calls, SMSs, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found., Comment: Categories (ACM class 2012): Security and privacy - Formal methods and theory of security -- Security requirements -- Formal security models -- Logic and verification; Network protocols - Protocol correctness -- Formal specifications; Security and privacy - Network security -- Mobile and wireless security - Security services -- Privacy-preserving protocols

Published
2018
Full Text
View/download PDF

6. Shaping Our Mental Model of Security (Transcript of Discussion)

Author

Radomirović, Saša, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Anderson, Jonathan, editor, Stajano, Frank, editor, Christianson, Bruce, editor, and Matyáš, Vashek, editor

Published
2020
Full Text
View/download PDF

7. Attack Trees with Sequential Conjunction

Author

Jhawar, Ravi, Kordy, Barbara, Mauw, Sjouke, Radomirovic, Sasa, and Trujillo-Rasua, Rolando

Subjects
Computer Science - Cryptography and Security
Abstract

We provide the first formal foundation of SAND attack trees which are a popular extension of the well-known attack trees. The SAND attack tree formalism increases the expressivity of attack trees by introducing the sequential conjunctive operator SAND. This operator enables the modeling of ordered events. We give a semantics to SAND attack trees by interpreting them as sets of series-parallel graphs and propose a complete axiomatization of this semantics. We define normal forms for SAND attack trees and a term rewriting system which allows identification of semantically equivalent trees. Finally, we formalize how to quantitatively analyze SAND attack trees using attributes., Comment: This is an extended version of the work published at IFIP SEC 2015

Published
2015

8. Generalizing Multi-party Contract Signing

Author

Mauw, Sjouke and Radomirovic, Sasa

Subjects
Computer Science - Cryptography and Security
Abstract

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 abort-chaining 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., Comment: Extended version of POST 2015 paper

Published
2015

9. An Anti-pattern for Misuse Cases

Author

Dashti, Mohammad Torabi, Radomirović, Saša, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Katsikas, Sokratis K., editor, Cuppens, Frédéric, editor, Cuppens, Nora, editor, Lambrinoudakis, Costas, editor, Kalloniatis, Christos, editor, Mylopoulos, John, editor, Antón, Annie, editor, and Gritzalis, Stefanos, editor

Published
2018
Full Text
View/download PDF

10. A framework for compositional verification of security protocols

Author

Andova, Suzana, Cremers, Cas, Gjosteen, Kristian, Mauw, Sjouke, Mjolsnes, Stig F., and Radomirovic, Sasa

Subjects
Computer Science - Cryptography and Security
Abstract

Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach. We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation. To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMax consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.

Published
2006

12. Guided Specification and Analysis of a Loyalty Card System

Author

Cuennet, Laurent, Pouly, Marc, Radomirović, Saša, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Mauw, Sjouke, editor, Kordy, Barbara, editor, and Jajodia, Sushil, editor

Published
2016
Full Text
View/download PDF

13. Derailing Attacks

Author

Radomirović, Saša, Dashti, Mohammad Torabi, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Christianson, Bruce, editor, Švenda, Petr, editor, Matyáš, Vashek, editor, Malcolm, James, editor, Stajano, Frank, editor, and Anderson, Jonathan, editor

Published
2015
Full Text
View/download PDF

14. Location-Private Interstellar Communication

Author

Jonker, Hugo, Mauw, Sjouke, Radomirović, Saša, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Christianson, Bruce, editor, Švenda, Petr, editor, Matyáš, Vashek, editor, Malcolm, James, editor, Stajano, Frank, editor, and Anderson, Jonathan, editor

Published
2015
Full Text
View/download PDF

15. Alice and Bob Meet Equational Theories

Author

Basin, David, Keller, Michel, Radomirović, Saša, Sasse, Ralf, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Martí-Oliet, Narciso, editor, Ölveczky, Peter Csaba, editor, and Talcott, Carolyn, editor

Published
2015
Full Text
View/download PDF

16. Security Protocols for Secret Santa

Author

Mauw, Sjouke, Radomirović, Saša, Ryan, Peter Y. A., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Christianson, Bruce, editor, and Malcolm, James, editor

Published
2014
Full Text
View/download PDF

17. Insider Attacks and Privacy of RFID Protocols

Author

van Deursen, Ton, Radomirović, Saša, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Petkova-Nikova, Svetla, editor, Pashalidis, Andreas, editor, and Pernul, Günther, editor

Published
2012
Full Text
View/download PDF

18. Foundations of Attack–Defense Trees

Author

Kordy, Barbara, Mauw, Sjouke, Radomirović, Saša, Schweitzer, Patrick, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Degano, Pierpaolo, editor, Etalle, Sandro, editor, and Guttman, Joshua, editor

Published
2011
Full Text
View/download PDF

19. EC-RAC: Enriching a Capacious RFID Attack Collection

Author

van Deursen, Ton, Radomirović, Saša, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Ors Yalcin, Siddika Berna, editor

Published
2010
Full Text
View/download PDF

20. Contextual Biometric-Based Authentication for Ubiquitous Services

Author

Buhan, Ileana, Lenzini, Gabriele, Radomirović, Saša, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Yu, Zhiwen, editor, Liscano, Ramiro, editor, Chen, Guanling, editor, Zhang, Daqing, editor, and Zhou, Xingshe, editor

Published
2010
Full Text
View/download PDF

21. Secure Ownership and Ownership Transfer in RFID Systems

Author

van Deursen, Ton, Mauw, Sjouke, Radomirović, Saša, Vullers, Pim, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Backes, Michael, editor, and Ning, Peng, editor

Published
2009
Full Text
View/download PDF

22. Algebraic Attacks on RFID Protocols

Author

van Deursen, Ton, Radomirović, Saša, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Markowitch, Olivier, editor, Bilas, Angelos, editor, Hoepman, Jaap-Henk, editor, Mitchell, Chris J., editor, and Quisquater, Jean-Jacques, editor

Published
2009
Full Text
View/download PDF

23. Untraceability of RFID Protocols

Author

van Deursen, Ton, Mauw, Sjouke, Radomirović, Saša, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Onieva, Jose A., editor, Sauveron, Damien, editor, Chaumette, Serge, editor, Gollmann, Dieter, editor, and Markantonakis, Konstantinos, editor

Published
2008
Full Text
View/download PDF

29. Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (Extended Version)

Author

Dreier, Jannik, Hirschi, Lucca, Radomirovic, Sasa, Sasse, Ralf, Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Department of Computer Science [ETH Zürich] (D-INFK), Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), University of Dundee, LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy, and ETH Zurich, Switzerland

Subjects
[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Computer Science::Networking and Internet Architecture, Computer Science::Cryptography and Security
Abstract

Exclusive-or (XOR) operations are common in cryptographic protocols, in particular in RFID protocols and electronic payment protocols. Although there are numerous applications, due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR.The TAMARIN prover is a state-of-the-art verification tool for cryptographic protocols in the symbolic model. In this paper, we improve the underlying theory and the tool to deal with an equational theory modeling XOR operations. The XOR theory can be freely combined with all equational theories previously supported, including user-defined equational theories. This makes TAMARIN the first tool to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrate the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs.

Published
2018

32. Über die Sicherheit digitaler Coupons

Author

Mazumder, Sita, Pouly, Marc, Radomirovic, Sasa, Mazumder, Sita, Pouly, Marc, and Radomirovic, Sasa

Abstract

Treueprogramme als Kundenbindungsmittelwerden in der digitalen Welt zur Realität.Ebenfalls Realität ist, dass manchekommerziellen Anbieter bereits im Designihrer digitalen Treueprogramme Sicherheitsfehlergemacht haben. Wie kann verhindertwerden, dass Treuepunkte vervielfältigtund im schlimmsten Fall gegen Bargeldeingetauscht werden?, + ID der Publikation: hslu_51266 + Art des Beitrages: Fachmedien + Sprache: Deutsch + Letzte Aktualisierung: 2023-10-09 11:00:14

Published
2017

33. mCarve: Carving attributed dump sets

Author

van Deursen, Ton, Mauw, Sjouke, and Radomirovic, Sasa

Subjects
Computer science [C05] [Engineering, computing & technology], Sciences informatiques [C05] [Ingénierie, informatique & technologie]
Published
2011

37. Attack-Defense Trees

Author

Kordy, Barbara, Mauw, Sjouke, Radomirovic, Sasa, Schweitzer, Patrick, Kordy, Barbara, Mauw, Sjouke, Radomirovic, Sasa, and Schweitzer, Patrick

Abstract

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.

Published
2012

39. Foundations of Attack-Defense Trees

Author

Kordy, Barbara, Mauw, Sjouke, Radomirovic, Sasa, Schweitzer, Patrick, Kordy, Barbara, Mauw, Sjouke, Radomirovic, Sasa, and Schweitzer, Patrick

Abstract

We introduce and give formal definitions of attack–defense trees. We argue that these trees are a simple, yet powerful tool to analyze complex security and privacy problems. Our formalization is generic in the sense that it supports different semantical approaches. We present several semantics for attack–defense trees along with usage scenarios, and we show how to evaluate attributes.

Published
2010

41. Secure ownership and ownership transfer in RFID systems

Author

Backes, Michael, Ning, Peng, Deursen, Ton van, Mauw, Sjouke, Radomirovic, Sasa, Vullers, Pim, Backes, Michael, Ning, Peng, Deursen, Ton van, Mauw, Sjouke, Radomirovic, Sasa, and Vullers, Pim

Abstract

Computer Security – ESORICS 2009 : 14th European Symposium on Research in Computer Security, 21 september 2009, Item does not contain fulltext

Published
2009

Catalog

Books, media, physical & digital resources
See catalog results