Online citations, reference lists, and bibliographies.

Secure Pseudonymous Channels

S. Mödersheim, L. Viganò
Published 2009 · Computer Science

Cite This
Download PDF
Analyze on Scholarcy
Share
Channels are an abstraction of the many concrete techniques to enforce particular properties of message transmissions such as encryption. We consider here three basic kinds of channels--authentic, confidential, and secure--where agents may be identified by pseudonyms rather than by their real names. We define the meaning of channels as assumptions, i.e. when a protocol relies on channels with particular properties for the transmission of some of its messages. We also define the meaning of channels as goals, i.e. when a protocol aims at establishing a particular kind of channel. This gives rise to an interesting question: given that we have verified that a protocol P2 provides its goals under the assumption of a particular kind of channel, can we then replace the assumed channel with an arbitrary protocol P1 that provides such a channel? In general, the answer is negative, while we prove that under certain restrictions such a compositionality result is possible.
This paper references
10.3233/JCS-1996-4104
A Calculus for Security Bootstrapping in Distributed Systems
U. Maurer (1996)
Chaining secure channels
C Dilloway (2008)
Secure Pseudonymous Channels (extended version)
S. Mödersheim (2009)
10.1006/inco.2002.3086
Secure Implementation of Channel Abstractions
M. Abadi (2002)
Basin . Formalizing and analyzing sender invariance
S. Mödersheim P. Hankes Drielsma (2009)
Rfc 2246: the tls protocol version 1
T. Dierks (1999)
Secure Pseudonymous Channels (extended version)
S. Mödersheim (2009)
10.1016/j.entcs.2009.05.030
Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives
Yohan Boichut (2009)
and L
A. Armando (2008)
A Framework for Purpose Built Keys (PBK)
A. Mankin (2003)
10.1016/j.ic.2007.07.002
A framework for compositional verification of security protocols
S. Andova (2008)
10.1109/CSFW.2006.10
Cryptographically sound theorem proving
C. Sprenger (2006)
and M
M. Backes (2004)
10.1007/978-3-540-75227-1_6
Formalizing and Analyzing Sender Invariance
P. Drielsma (2006)
10.1007/978-3-540-75227-1
Formal Aspects in Security and Trust, Fourth International Workshop, FAST 2006, Hamilton, Ontario, Canada, August 26-27, 2006, Revised Selected Papers
T. Dimitrakos (2007)
10.1109/CSFW.2000.856942
How to prevent type flaw attacks on security protocols
J. Heather (2000)
10.1007/s10703-008-0059-4
Safely composing security protocols
V. Cortier (2009)
10.3233/JCS-2004-123-405
Authentication tests and disjoint encryption: A design method for security protocols
J. Guttman (2004)
10.1145/1456396.1456397
Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for google apps
A. Armando (2008)
On the Specification of Secure Channels
G. Lowe (2007)
10.1109/DISCEX.2000.824980
CAPSL integrated protocol environment
G. Denker (2000)
Secure Asynchronous Reactive Systems
M. Backes (2004)
10.1109/CSFW.2002.1021815
A formal analysis of ome properties of kerberos 5 using MSR
F. Butler (2002)
10.1109/CSFW.1997.596782
A hierarchy of authentication specifications
G. Lowe (1997)
and L
A. Armando (2008)
10.1007/3-540-45657-0_24
Automated Unbounded Verification of Security Protocols
Y. Chevalier (2002)
10.1515/9783111576855-009
D
Saskia Bonjour (1824)
Cryptographic protocol generation from capsl
J. Millen (2001)
and C
T. Dierk (1999)
10.21236/ada327281
Model Checking for Security Protocols
W. Marrero (1997)
RFC3775 – Mobility Support in IPv6
D Johnson (2004)
and M
M. Backes (2004)
10.1109/CSF.2008.17
Language Based Secure Communication
M. Bugliesi (2008)
10.1109/49.223872
Security Architectures Using Formal Methods
C. Boyd (1993)
The Intermediate Format
AVISPA (2003)
and C
T. Dierk (1999)
10.3233/JCS-2009-0351
Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols
Sebastian Mödersheim (2010)
Improvements on the Genet and Klay technique to automatically verify security protocols
Yohan Boichut (2004)
10.1145/1035429.1035431
Secure protocol composition
A. Datta (2003)
10.1007/s10207-007-0041-y
SAT-based model-checking for security protocols analysis
A. Armando (2007)
10.1016/j.ic.2007.05.005
Breaking and fixing public-key Kerberos
I. Cervesato (2006)
10.1109/ARES.2009.95
Algebraic Properties in Alice and Bob Notation
Sebastian Mödersheim (2009)
10.1007/11836810_36
Designing and Verifying Core Protocols for Location Privacy
David von Oheimb (2006)
10.1007/978-3-642-00596-1_22
Cryptographic Protocol Composition via the Authentication Tests
J. Guttman (2008)
Deliverable 2.3: The Intermediate Format. Available at www.avispa-project.org
Avispa (2003)
10.1007/s10207-004-0055-7
OFMC: A symbolic model checker for security protocols
D. Basin (2004)
10.1007/3-540-44404-1_10
Compiling and Verifying Security Protocols
F. Jacquemard (2000)
10.1109/TIT.1976.1055638
New directions in cryptography
W. Diffie (1976)
10.1109/CSF.2008.6
Composition of Password-Based Protocols
Stéphanie Delaune (2008)
Basin . Formalizing and analyzing sender invariance
S. Mödersheim P. Hankes Drielsma (2009)
10.1007/11805618_21
The CL-Atse Protocol Analyser
Mathieu Turuani (2006)
10.1007/11513988_27
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications
A. Armando (2005)
10.1109/CSF.2007.24
LTL Model Checking for Security Protocols
A. Armando (2007)
The Intermediate Format
AVISPA (2003)
10.1109/SFCS.2001.959888
Universally composable security: a new paradigm for cryptographic protocols
R. Canetti (2001)
10.1109/CSFW.1997.596779
Casper: a compiler for the analysis of security protocols
G. Lowe (1997)
10.3929/ETHZ-A-005358764
Models and methods for the automated analysis of security protocols
S. Mödersheim (2007)



This paper is referenced by
10.1109/CSF.2014.26
A Sound Abstraction of the Parsing Problem
Sebastian Mödersheim (2014)
Secure Implementation of Asynchronous Method Calls and Futures
AS Cybernetica (2012)
10.1109/CSF.2007.24
LTL Model Checking for Security Protocols
A. Armando (2007)
10.1007/978-3-642-28756-5_19
The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures
A. Armando (2012)
10.1109/TrustCom.2011.29
A Privacy-Friendly RFID Protocol Using Reusable Anonymous Tickets
M. Asadpour (2011)
10.1109/ARES.2009.95
Algebraic Properties in Alice and Bob Notation
Sebastian Mödersheim (2009)
10.1109/IWCMC.2011.5982705
Verifying SeVeCom using set-based abstraction
Sebastian Mödersheim (2011)
10.1016/j.jisa.2016.05.004
Security protocol specification and verification with AnBx
Michele Bugliesi (2016)
Security Analysis of the Open Banking Account and Transaction API Protocol
Abdulaziz Almehrej (2020)
10.1007/978-3-642-35371-0_3
Secure Implementation of Asynchronous Method Calls and Futures
Peeter Laud (2012)
10.1007/978-3-319-25527-9_7
Alice and Bob: Reconciling Formal Models and Implementation
Omar Almousa (2015)
10.1109/CSF.2010.29
Protocol Composition for Arbitrary Primitives
Stefan Ciobaca (2010)
10.1109/CSF.2014.31
Automated Generation of Attack Trees
Roberto Vigo (2014)
A Formal Model of Identity Mixer Camenisch ,
Jan Mödersheim (2017)
10.1007/978-3-642-41488-6_1
Detecting and Preventing Beacon Replay Attacks in Receiver-Initiated MAC Protocols for Energy Efficient WSNs
Alessio Di Mauro (2013)
Trustworthy Clouds – Privacy and Resilience for Internet-scale Critical Infrastructure
Imad M. Abbadi (2011)
Vertical Protocol Composition
Dtu Informatics (2011)
10.1007/s10009-015-0385-y
SATMC: a SAT-based model checker for security protocols, business processes, and security APIs
Alessandro Armando (2015)
10.1007/978-3-319-89722-6
Principles of Security and Trust
Lujo Bauer (2018)
Medium Access Control in Energy Harvesting - Wireless Sensor Networks
Xenofon Fafoutis (2014)
10.3233/JCS-150526
Verifying layered security protocols
Thomas Gibson-Robinson (2015)
10.2168/LMCS-12(4:5)2016
Discovering, quantifying, and displaying attacks
Roberto Vigo (2016)
10.1109/CSF.2015.21
A Complete Characterization of Secure Human-Server Communication
D. Basin (2015)
A Sound Abstraction of the Parsing Problem (Extended Version)
S. Mödersheim (2014)
10.1007/978-3-662-46666-7_17
Composing Security Protocols: From Confidentiality to Privacy
Myrto Arapinis (2015)
Structured Intuition: A Methodology to Analyse Entity Authentication
Naveed Ahmed (2012)
10.1109/CSF.2011.23
Vertical Protocol Composition
Thomas Groß (2011)
Stateful Protocol Composition ( Extended Version ) DTU
A. Hess (2018)
10.1109/TII.2013.2277938
Privacy-Enhanced Data Aggregation Scheme Against Internal Attackers in Smart Grid
C. Fan (2014)
10.1007/978-3-642-35371-0
Trusted Systems
J. Kittler (2012)
Vertical Protocol Composition (Extended Version)
T. Gross (2011)
10.1007/978-3-642-29420-4_11
Analysing Applications Layered on Unilaterally Authenticating Protocols
Thomas Gibson-Robinson (2011)
See more
Semantic Scholar Logo Some data provided by SemanticScholar