Publication

Model Checking Security Protocols: A Multiagent System Approach

Publications associées (82)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

Model Checking Detectability of Attacks in Multiagent Systems

Information security is vital to many multiagent system applications. In this paper we formalise the notion of detectability of attacks in a MAS setting and analyse its applicability. We introduce a taxonomy of detectability specifications expressed in tem ...

International Foundation for Autonomous Agents and Multiagent Systems2010

Dissent: Accountable Group Anonymity

Bryan Alexander Ford, Henry Nathaniel Corrigan-Gibbs

Users often wish to participate in online groups anonymously, but misbehaving users may abuse this anonymity to disrupt the group. Messaging protocols such as Mix-nets and DC-nets leave online groups vulnerable to denial-of-service and Sybil attacks, while ...

2010

Joint Identity-Message Coding for Sensor Networks

Christina Fragouli, Suhas Diggavi, Lorenzo Keller, Mahdi Jafari Siavoshani

In a significant class of sensor-network applications, the identities of the reporting sensors constitute the bulk of the communicated data, whereas the message itself can be as small as a single bit—for instance, in many cases, sensors are used to detect ...

Institute of Electrical and Electronics Engineers2010

The Next 700 BFT Protocols

Rachid Guerraoui, Marko Vukolic, Nikola Knezevic

Modern Byzantine fault-tolerant state machine replication (BFT) protocols involve about 20,000 lines of challenging C++ code encompassing synchronization, networking and cryptography. They are notoriously difficult to develop, test and prove. We present a ...

2010

Automatic Verification of Temporal-Epistemic Properties of Cryptographic Protocols

We present a technique for automatically verifying cryptographic protocols specified in the mainstream specification language CAPSL. We define a translation from CAPSL models into interpreted systems, a popular semantics for temporal-epistemic logic, and r ...

2009

Secure communication using authenticated channels

Sylvain Pasini

Our main motivation is to design more user-friendly security protocols. Indeed, if the use of the protocol is tedious, most users will not behave correctly and, consequently, security issues occur. An example is the actual behavior of a user in front of an ...

EPFL2009

On Tamper-Resistance from a Theoretical Viewpoint: The Power of Seals

Serge Vaudenay

Tamper-proof devices are pretty powerful. They can be used to have better security in applications. In this work we observe that they can also be maliciously used in order to defeat some common privacy protection mechanisms. We propose the theoretical mode ...

Springer2009

Compilation Method for the Verification of Temporal-Epistemic Properties of Cryptographic Protocols

We present a technique for automatically verifying cryptographic protocols specified in the mainstream specification language CAPSL. Our work is based on model checking multi-agent systems against properties given in AI logics. We present PC2IS, a compiler ...

2009

Smashing SQUASH-0

Serge Vaudenay, Khaled Ouafi

At the RFID Security Workshop 2007, Adi Shamir presented a new challenge-response protocol well suited for RFIDs, although based on the Rabin public-key cryptosystem. This protocol, which we call SQUASH-0, was using a linear mixing function which was subse ...

Springer2009

A New Message Recognition Protocol with Self-recoverability for Ad Hoc Pervasive Networks

Atefeh Mashatan

We examine the problem of message recognition by reviewing the definitions and the security model in the literature. In particular, we examine the Jane Doe protocol, which was proposed by Lucks et al., more closely and note its inability to recover in case ...

Springer2009