Equivalences and calculi for formal verification of cryptographic protocols
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.
This paper describes and analyzes the security of a general-purpose cryptographic function design, with application in RFID tags and sensor networks. Based on these analyzes, we suggest minimum parameter values for the main components of this cryptographic ...
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
Although distributed systems are widely used nowadays, their implementation and deployment is still a time-consuming, error-prone, and hardly predictive task. In this paper, we propose a methodology for producing automatically efficient and correct-by-cons ...
Loosely speaking, an obfuscation O of a function f should satisfy two requirements: firstly, using O, it should be possible to evaluate f; secondly, O should not reveal anything about f that cannot be learnt from oracle access to f alone. Several definitio ...
ERLANG is an industrially successful functional language that uses the Actor model for concurrency. It supports the message-passing paradigm by providing pattern-matching over received messages. Unfortunately coding synchronisation between multiple process ...
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2010
The Algebra of Connectors AC(P) is used to model structured interactions in the BIP component framework. Its terms are connectors, relations describing synchronization constraints between the ports of component-based systems. Connectors are structured comb ...
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 ...
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 ...
Cryptographic protocols are an essential component of network communications. Despite their relatively small size compared to other distributed algorithms, they are known to be error-prone. This is due to the obligation to behave robustly in the context of ...
Meeting the requirements of NIST’s new cryptographic standard ‘Suite B Cryptography’ means phasing out usage of 1024-bit RSA and 160-bit Elliptic Curve Cryptography (ECC) by the year 2010. This write-up comments on the vulnerability of these systems to an ...
