I used to sort papers by
subject and by type of publication venue, rather than chronologically. The
classification was approximate, but I did not mind; I would not make fine
distinctions between large workshops and small conferences, nor did I attempt
to be precise on whether a paper on a calculus for modeling security protocols,
say, should be under “Security”, “Programming
languages”, or “Specification and verification”. My sense now
is that such classifications may have their place, but that a chronological
classification is more useful here. In particular, a
(reverse) chronological classification puts all recent papers near the top. It
also makes obvious the simultaneity of various apparently unrelated lines of
work. In Tlön, literary critics often attribute
two dissimilar works to the same imaginary author; sometimes I feel like one of
those authors.
The versions given here are not necessarily identical to any of the previously
published ones. I believe that the technical contents are the same.
The documents distributed by this server have been provided as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Web PKI: Closing the Gap between Guidelines and Practices
[with Antoine Delignat-Lavaud, Andrew Birrell, Ilya Mironov,
Ted Wobber, and Yinglian Xie]
Proceedings of the 21st Annual Network and Distributed System Security
Symposium (February 2014).
© Internet Society.
Naiad: A Timely Dataflow System
[with Derek G. Murray, Frank McSherry, Rebecca Isaacs,
Michael Isard, and Paul Barham]
Proceedings of the 24th ACM Symposium on Operating System Principles (November
2013), 439-455.
On Protection by Layout
Randomization
[with Gordon Plotkin]
ACM Transactions on Information and System Security 15, 2 (July 2012),
8:1-8:29.
© ACM.
Host Fingerprinting and Tracking on the Web:
Privacy and Security Implications
[with Ting-Fang Yen, Yinglian Xie, Fang Yu, and Roger Peng Yu]
Proceedings of the 19th Annual Network and Distributed System Security
Symposium (February 2012).
© Internet
Society.
AC: Composable Asynchronous IO for Native
Languages
[with Tim Harris, Rebecca Isaacs, and Ross McIlroy]
Proceedings of the 2011 ACM Conference on Object-Oriented Programming Languages
and Systems (October 2011), 903-920.
© ACM
Informatique et Sciences
Numériques : La Sécurité Informatique
Cours et travaux du Collège de
France, Résumés 2010—2011 (2011), 805-810.
deSEO: Combating
Search-Result Poisoning
[with John P. John, Fang Yu, Yinglian Xie, and Arvind Krishnamurthy]
Proceedings of the 20th USENIX Security Symposium (August 2011), 299-313.
Position Paper: Differential Privacy with
Information Flow Control
[with Arnar Birgisson and Frank McSherry]
Proceedings of ACM SIGPLAN Sixth Workshop on Programming Languages and Analysis
for Security (June 2011).
© ACM.
Heat-seeking Honeypots: Design and Experience
[with John P. John, Fang Yu, Yinglian Xie, and Arvind Krishnamurthy]
Proceedings of the Twentieth International World Wide Web Conference (March
2011), 207-216.
© ACM.
Semantics of
Transactional Memory and Automatic Mutual Exclusion
[with Andrew Birrell, Tim Harris, and Michael Isard]
ACM Transactions on Programming Languages and Systems 33, 1 (January 2011),
2:1-2:50.
© ACM.
A Model of Cooperative Threads
[with Gordon Plotkin]
Logical Methods in Computer Science 6, 4 (October 2010), paper 2, 1-39.
A Model of Dynamic
Separation for Transactional Memory
[with Tim Harris and Katherine F. Moore]
Information and Computation 208, 10 (October 2010), 1093-1117.
© Elsevier.
How to Tell an Airport from a Home: Techniques and Applications
[with Andreas Pitsillidis, Yinglian Xie, Fang Yu, Geoffrey M. Voelker, and Stefan Savage]
Proceedings of HotNets-IX: Ninth ACM Workshop on Hot Topics in Networks (October 2010).
Searching the Searchers with SearchAudit
[with John P. John, Fang Yu, Yinglian Xie, and Arvind Krishnamurthy]
Proceedings of the 19th USENIX Security Symposium (August 2010), 127-142.
Guessing Attacks and the Computational
Soundness of Static Equivalence
[with Mathieu Baudet and Bogdan Warinschi]
Journal of Computer Security 18, 5 (August 2010), 909-968.
© IOS Press.
On Protection by Layout Randomization
[with Gordon Plotkin]
Proceedings of the 23rd IEEE Computer Security Foundations Symposium (July
2010), 337-351.
The on-line version contains minor
corrections and an additional appendix. This is a preliminary version of a
journal paper (see citation).
© IEEE.
The Fine Print of Security
(Invited Lecture)
Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science
(July 2010), 110.
© IEEE
Control-Flow Integrity:
Principles, Implementations, and Applications
[with Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti]
ACM Transactions on Information and System Security 13, 1 (October 2009), 1-40.
© ACM
Perspectives on Transactional Memory
[with Tim Harris]
CONCUR 2009, Springer-Verlag (August 2009), 1-14.
© Springer-Verlag.
Logic in Access Control (Tutorial Notes)
Foundations of Security Analysis and Design V, FOSAD 2008/2009 Tutorial
Lectures, Springer-Verlag (2009), 145-165.
© Springer-Verlag.
De-anonymizing the Internet Using
Unreliable IDs
[with Yinglian Xie and Fang Yu]
Proceedings of the ACM SIGCOMM 2009 Conference on Applications, Technologies,
Architectures, and Protocols for Computer Communications (August 2009), 75-86.
© ACM
Models and Proofs of Protocol Security: A
Progress Report
[with Bruno Blanchet and Hubert Comon-Lundh]
Computer Aided Verification, 21st International Conference 2009,
Springer-Verlag (June/July 2009), 35-49.
© Springer-Verlag.
Unified Declarative Platform for Secure
Networked Information Systems
[with Wenchao Zhou, Yun Mao, and Boon Thau Loo]
Proceedings of the 25th International Conference on Data Engineering (March
2009), 150-161.
© IEEE.
Implementation and Use of Transactional
Memory with Dynamic Separation
[with Andrew Birrell, Tim Harris, Johnson Hsieh, and Michael Isard]
International Conference on Compiler Construction 2009, Springer-Verlag (March
2009), 63-77.
© Springer-Verlag.
Transactional Memory with Strong Atomicity
Using Off-the-Shelf Memory Protection Hardware
[with Tim Harris and Mojtaba Mehrara]
Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of
Parallel Programming (February 2009), 185-196.
© ACM
A Model of Cooperative Threads
[with Gordon Plotkin]
Proceedings of the 36th Annual ACM Symposium on Principles of Programming
Languages (January 2009), 29-40.
This is a preliminary version of a journal paper (see citation).
© ACM
Code-Carrying Authorization
[with Sergio Maffeis, Cédric Fournet, and Andrew D. Gordon]
Computer Security -- ESORICS 2008, Springer-Verlag (October 2008), 563-579.
© Springer-Verlag.
A Model of Dynamic Separation for Transactional Memory
[with Tim Harris and Katherine F. Moore]
CONCUR 2008, Springer-Verlag (August 2008), 6-20.
This is a preliminary version of a journal paper (see citation).
© Springer-Verlag.
Variations in Access Control
Logic
Ninth International Conference on Deontic Logic in Computer Science (DEON
2008), Springer-Verlag (July 2008), 96-109.
© Springer-Verlag.
Security Analysis of Cryptographically
Controlled Access to XML Documents
[with Bogdan Warinschi]
Journal of the ACM 55, 2 (May 2008), 6:1-6:29.
© ACM.
A Modal Deconstruction of Access Control
Logics
[with Deepak Garg]
Foundations of Software Science and Computation Structures, FOSSACS 2008,
Springer-Verlag (April 2008), 216-230.
© Springer-Verlag.
Dynamic
Separation for Transactional Memory
[with Andrew Birrell, Tim Harris, Johnson Hsieh, and Michael Isard]
MSR-TR-2008-43 (March 2008).
Automated Verification of
Selected Equivalences for Security Protocols
[with Bruno Blanchet and Cédric Fournet]
Journal of Logic and Algebraic Programming 75, 1 (February-March 2008), 3-51.
© Elsevier Science.
Automatic Mutual
Exclusion and Atomicity Checks
Concurrency, Graphs and Models: Essays Dedicated to Ugo Montanari on the
Occasion of His 65th Birthday, Springer-Verlag (2008), 510-526.
© Springer-Verlag.
Semantics of Transactional Memory and Automatic Mutual Exclusion
[with Andrew Birrell, Tim Harris, and Michael Isard]
Proceedings of the 35th Annual ACM Symposium on Principles of Programming
Languages (January 2008), 63-74.
This is a preliminary version of a journal paper (see citation).
© ACM.
Policies and Proofs for Code Auditing
[with Nathan Whitehead and Jordan Johnson]
Automated Technology for Verification and Analysis, 5th International Symposium,
ATVA 2007, Springer-Verlag (October 2007), 1-14.
© Springer-Verlag.
Security Protocols: Principles and
Calculi (Tutorial Notes)
Foundations of Security Analysis and Design IV, FOSAD 2006/2007 Tutorial
Lectures, Springer-Verlag (2007), 1-23.
© Springer-Verlag.
Operating
System Protection against Side-Channel Attacks that Exploit Memory Latency
[with Úlfar Erlingsson]
Microsoft Research Technical Report MSR-TR-2007-117 (August 2007).
Just Fast Keying in the Pi Calculus
[with Bruno Blanchet and Cédric Fournet]
ACM Transactions on Information and System Security 10, 3 (July 2007), 1-59.
© ACM.
Access
Control in a Core Calculus of Dependency
Computation,
Meaning, and Logic: Articles dedicated to Gordon Plotkin, Electronic Notes
in Theoretical Computer Science 172 (April 2007), 5-31.
© Elsevier Science.
Towards a Declarative Language and System
for Secure Networking
[with Boon Thau Loo]
Proceedings of the Third
International Workshop on Networking Meets Databases (NetDB
'07) (April 2007).
Authorizing Applications in
Singularity
[with Ted Wobber, Aydan Yumerefendi,
Andrew Birrell, and Daniel R. Simon]
Proceedings of the EuroSys 2007 Conference (March
2007), 355-368.
© ACM.
Deciding Knowledge in Security Protocols under
Equational Theories
[with Véronique Cortier]
Theoretical Computer Science 367, 1-2 (November 2006), 2-32.
© Elsevier Science.
XFI: Software Guards for
System Address Spaces
[with Mihai Budiu, Úlfar Erlingsson, George Necula, and Michael Vrable]
Proceedings of the 7th USENIX Symposium on Operating Systems Design and
Implementation (November 2006), 75-88.
Computational Secrecy by Typing for the Pi
Calculus
[with Ricardo Corin and Cédric Fournet]
Proceedings of the 4th ASIAN Symposium on Programming Languages and Systems,
Springer-Verlag (November 2006), 253-269.
© Springer-Verlag.
Architectural
Support for Software-Based Protection
[with Mihai Budiu and Úlfar Erlingsson]
Proceedings of the 1st Workshop on Architectural and System Support for
Improving Software Dependability, ASID 2006 (October 2006), 42-51.
© ACM.
Access Control in a Core Calculus of
Dependency
Proceedings of the 2006 ACM International Conference on Functional Programming
(September 2006), 263-273.
This is a preliminary version of a journal paper (see citation).
© ACM.
Formal Analysis of Dynamic, Distributed
File-System Access Controls
[with Avik Chaudhuri]
Formal Methods for Networked and Distributed Systems, FORTE 2006,
Springer-Verlag (September 2006), 99-114.
© Springer-Verlag.
Secrecy by Typing and File-Access Control
[with Avik Chaudhuri]
Proceedings of the 19th IEEE Computer Security Foundations Workshop (July
2006), 112-123.
© IEEE.
Guessing Attacks and the Computational
Soundness of Static Equivalence
[with Mathieu Baudet and Bogdan Warinschi]
Foundations of Software Science and Computation Structures, FOSSACS 2006,
Springer-Verlag (March 2006), 398-412.
This is a preliminary version of a journal paper (see citation).
© Springer-Verlag.
Types for Safe Locking: Static Race
Detection for Java
[with Cormac Flanagan and Stephen Freund]
ACM Transactions on Programming Languages and Systems 28, 2 (March 2006),
207-255.
© ACM.
Control-Flow Integrity: Principles, Implementations, and Applications
[with Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti]
Proceedings of the 12th ACM Symposium on Computer and Communications Security
(November 2005), 340-353.
This paper is subsumed by a journal paper (see citation).
© ACM.
Formal Security Analysis of Basic
Network-Attached Storage
[with Avik Chaudhuri]
Proceedings of the 2005 ACM Workshop on Formal Methods in Security Engineering
(November 2005), 43-52.
© ACM.
An
Overview of the Singularity Project
[with Galen C. Hunt, James R. Larus, Mark Aiken, Paul Barham, Manuel Fähndrich, Chris Hawblitzel, Orion Hodson, Steven
Levi, Nick Murphy, Bjarne Steensgaard, David Tarditi, Ted Wobber, and Brian Zill]
Microsoft Research Technical Report MSR-TR-2005-135 (October 2005).
Computer-Assisted Verification of a
Protocol for Certified Email
[with Bruno Blanchet]
Science of Computer Programming 58, 1-2 (October 2005), 3-27.
© Elsevier Science.
A Theory of Secure Control Flow
[with Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti]
Formal Methods and Software Engineering, 7th International Conference on Formal
Engineering Methods, ICFEM 2005, Springer-Verlag (July 2005), 111-124.
This paper is subsumed by a journal paper (see citation).
© Springer-Verlag.
Password-Based Encryption Analyzed
[with Bogdan Warinschi]
Automata, Languages and Programming: 25th International Colloquium, ICALP 2005,
Springer-Verlag (July 2005), 664-676.
© Springer-Verlag.
Access
Control in a World of Software Diversity
[with Andrew Birrell and Ted Wobber]
Tenth Workshop on Hot Topics in Operating Systems (HotOS
X) (June 2005), 127-132.
Automated Verification of Selected Equivalences
for Security Protocols
[with Bruno Blanchet and Cédric Fournet]
Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science
(June 2005), 331-340.
This is a preliminary version of a journal paper (see citation).
© IEEE.
Deciding Knowledge in Security Protocols
under (Many More) Equational Theories
[with Véronique Cortier]
Proceedings of the 18th IEEE Computer Security Foundations Workshop (June
2005), 62-76.
This paper is subsumed by a journal paper (see citation).
© IEEE.
Security Analysis of Cryptographically
Controlled Access to XML Documents
[with Bogdan Warinschi]
Proceedings of the 24th ACM Symposium on Principles of Database Systems (June
2005), 108-117.
This is a preliminary version of a journal paper (see citation).
© ACM.
Moderately Hard, Memory-bound Functions
[with Mike Burrows, Mark Manasse, and Edward Wobber]
ACM Transactions on Internet Technology 5, 2 (May 2005), 299-327.
© ACM.
BCiC: A System for Code Authentication and Verification
[with Nathan Whitehead]
Logic for Programming, Artificial Intelligence, and Reasoning, 11th
International Conference, Springer-Verlag (March 2005), 110-124.
© Springer-Verlag.
Language-Based Enforcement of Privacy Policies
[with Katia Hayati]
Privacy Enhancing Technologies, 4th International Workshop, PET 2004, Revised
Selected Papers, Springer-Verlag (2005), 302-313.
© Springer-Verlag.
Analyzing Security Protocols with
Secrecy Types and Logic Programs
[with Bruno Blanchet]
Journal of the ACM 52, 1 (January 2005), 102-146.
© ACM.
Private
Authentication
[with Cédric Fournet]
Theoretical Computer Science 322, 3 (September 2004), 427-476.
© Elsevier Science.
A
Logical Account of NGSCB
[with Ted Wobber]
Formal Techniques for Networked and Distributed Systems -- FORTE 2004,
Springer-Verlag (September 2004), 1-12.
© Springer-Verlag.
A Logic of Object-Oriented
Programs
[with K. Rustan M. Leino]
Verification: Theory and Practice, Springer-Verlag (2004), 11-41.
© Springer-Verlag.
On Access Control, Data
Integration, and Their Languages
Computer Systems: Theory, Technology and Applications, A Tribute to Roger
Needham, Springer-Verlag (2004), 9-14.
© Springer-Verlag.
Trusted Computing, Trusted Third Parties, and Verified Communications
Security and Protection in Information Processing Systems, IFIP 18th World
Computer Congress, TC11 19th International Information Security Conference, Kluwer
(August 2004), 291-308.
The on-line version contains additional detail.
© Kluwer.
Deciding Knowledge in Security
Protocols under Equational Theories
[with Véronique Cortier]
Automata, Languages and Programming: 31st International Colloquium, ICALP 2004,
Springer-Verlag (July 2004), 46-58.
This paper is subsumed by a journal paper (see citation).
© Springer-Verlag.
By Reason and Authority: A System for
Authorization of Proof-Carrying Code
[with Nathan Whitehead and George Necula]
Proceedings of the 17th IEEE Computer Security Foundations Workshop (June
2004), 236-250.
© IEEE.
Just Fast Keying in the Pi Calculus
[with Bruno Blanchet and Cédric Fournet]
Programming Languages and Systems: 13th European Symposium on Programming, ESOP
2004, Springer-Verlag (March 2004), 340-354.
This is a preliminary version of a journal paper (see citation).
© Springer-Verlag.
Choice in Dynamic Linking
[with Georges Gonthier and Benjamin Werner]
Foundations of Software Science and Computation Structures: Seventh
International Conference, FOSSACS 2004, Springer-Verlag (March 2004), 12-26.
© Springer-Verlag.
Bankable Postage for Network Services
[with Andrew Birrell, Mike Burrows, Frank Dabek, and
Ted Wobber]
Advances in Computing Science -- ASIAN 2003, Programming Languages and
Distributed Computation, 8th Asian Computing Science Conference, Springer-Verlag
(December 2003), 72-90.
© Springer-Verlag.
Built-in Object Security
Object-Oriented Programming -- ECOOP 2003, Springer-Verlag (July 2003), 1.
© Springer-Verlag.
Logic in Access Control
Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer
Science (June 2003), 228-233.
This is subsumed by a tutorial (see citation).
© IEEE.
Computer-Assisted Verification of a Protocol for Certified Email
[with Bruno Blanchet]
Static Analysis, 10th International Symposium, SAS 2003, Springer-Verlag (June
2003), 316-335.
This is a preliminary version of a journal paper (see citation).
© Springer-Verlag.
Moderately Hard, Memory-bound Functions
[with Mike Burrows, Mark Manasse, and Edward Wobber]
Proceedings of the 10th Annual Network and Distributed System Security
Symposium (February 2003), 25-39.
This is a preliminary version of a journal paper (see citation).
© Internet
Society.
Access Control based on Execution History
[with Cédric Fournet]
Proceedings of the 10th Annual Network and Distributed System Security
Symposium (February 2003), 107-121.
© Internet
Society.
Hiding Names: Private Authentication in the Applied Pi Calculus
[with Cédric Fournet]
Software Security -- Theories and Systems. Mext-NSF-JSPS
International Symposium (ISSS'02), Springer-Verlag (2003), 317-338.
This paper is subsumed by a journal paper (see citation).
© Springer-Verlag.
Secrecy Types for Asymmetric
Communication
[with Bruno Blanchet]
Theoretical Computer Science 298, 3 (2003), 387-415.
© Elsevier Science.
Reasoning about Secrecy for
Active Networks
[with Pankaj Kakkar and Carl A. Gunter]
Journal of Computer Security 11, 2 (2003), 245-287.
© IOS Press.
Private Authentication
Privacy Enhancing Technologies, Second International Workshop, PET 2002,
Revised Papers, Springer-Verlag (2003), 27-40.
This paper is subsumed by a journal paper (see citation).
© Springer-Verlag.
Reconciling Two Views of Cryptography (The
Computational Soundness of Formal Encryption)
[with Phillip Rogaway]
Journal of Cryptology 15, 2 (2002), 103-127.
© Springer-Verlag.
Certified Email with a Light On-Line Trusted Third Party: Design and
Implementation
[with Neal Glew, Bill Horne, and Benny Pinkas]
Proceedings of the Eleventh International World Wide Web Conference (May 2002),
387-395.
© ACM.
Secure Implementation of Channel
Abstractions
[with Cédric Fournet and Georges Gonthier]
Information and Computation 174, 1 (April 2002), 37-83.
The on-line version contains additional
detail.
© Academic Press.
Analyzing Security Protocols with Secrecy Types and
Logic Programs
[with Bruno Blanchet]
Proceedings of the 29th ACM Symposium on Principles of Programming Languages
(January 2002), 33-44.
This is a preliminary version of a journal paper (see citation).
© ACM.
Formal Eavesdropping and its Computational
Interpretation
[with Jan Jürjens]
Theoretical Aspects of Computer Software, Springer-Verlag (October 2001),
82-94.
© Springer-Verlag.
Leslie Lamport's
Properties and Actions
Proceedings of the Twentieth Annual ACM Symposium on Principles of Distributed
Computing (August 2001), 15.
© ACM.
Computing
Symbolic Models for Verifying Cryptographic Protocols
[with Marcelo Fiore]
Proceedings of the 14th IEEE Computer Security Foundations Workshop (June
2001), 160-173.
© IEEE.
Secrecy Types for Asymmetric Communication
[with Bruno Blanchet]
Foundations of Software Science and Computation Structures: Fourth
International Conference, FOSSACS 2001, Springer-Verlag (April 2001), 25-41.
This is a preliminary version of a journal paper (see citation).
Mobile Values, New Names, and
Secure Communication
[with Cédric Fournet]
Proceedings of the 28th ACM Symposium on Principles of Programming Languages
(January 2001), 104-115.
© ACM.
Reconciling Two Views of Cryptography (The Computational Soundness of Formal
Encryption)
[with Phillip Rogaway]
Theoretical Computer Science, Proceedings of the International Conference IFIP
TCS 2000, Springer-Verlag (August 2000), 3-22.
This is a preliminary version of a journal paper (see citation).
© Springer-Verlag.
Taming the Adversary
Advances in Cryptology -- CRYPTO 2000, Springer-Verlag (August 2000), 353-358.
© Springer-Verlag.
Security Protocols and their Properties
Foundations of Secure Computation, NATO Science Series, IOS Press (2000),
39-60. Volume for the 20th International Summer School on Foundations of Secure
Computation, held in Marktoberdorf, Germany (1999).
© IOS Press.
Reasoning about Secrecy for Active Networks
[with Pankaj Kakkar and Carl A. Gunter]
Proceedings of the 13th IEEE Computer Security Foundations Workshop (July
2000), 118-129.
This is a preliminary version of a journal paper (see citation).
TT-Closed Relations and Admissibility
Mathematical Structures in Computer Science 10, 3 (June 2000), 313-320.
© Cambridge University Press.
Authentication Primitives
and their Compilation
[with Cédric Fournet and Georges Gonthier]
Proceedings of the 27th ACM Symposium on Principles of Programming Languages
(January 2000), 302-315.
© ACM.
A Top-Down Look at a Secure Message
[with Cédric Fournet and Georges Gonthier]
Proceedings of the 19th International Conference on Foundations of Software
Technology and Theoretical Computer Science, Springer-Verlag (December 1999),
122-141.
This paper is partly subsumed by the journal paper Secure Implementation of
Channel Abstractions (see citation).
© Springer-Verlag.
Secrecy by Typing in Security Protocols
Journal of the ACM 46, 5 (September 1999), 749-786.
© ACM.
Object Types against Races
[with Cormac Flanagan]
CONCUR'99, Springer-Verlag (August 1999), 288-303.
Parts of this paper are subsumed by a journal paper (see citation).
© Springer-Verlag.
Secure Communications Processing for Distributed Languages
[with Cédric Fournet and Georges Gonthier]
Proceedings of the 1999 IEEE Symposium on Security and Privacy (May 1999),
74-88.
This paper is subsumed by the journal paper Secure Implementation of Channel
Abstractions (see citation).
© IEEE.
Secrecy in Programming-Language Semantics
Proceedings of MFPS XV (Mathematical Foundations of Programming Semantics,
Fifteenth Annual Conference), Electronic
Notes in Theoretical Computer Science 20 (April 1999).
Security Protocols and Specifications
Foundations of Software Science and Computation Structures: Second
International Conference, FOSSACS '99 Springer-Verlag (March 1999), 1-13.
This paper is subsumed by Security Protocols and their Properties (see citation).
© Springer-Verlag.
Types
for Safe Locking
[with Cormac Flanagan]
Programming Languages and Systems: 8th European Symposium on Programming, ESOP
'99, Springer-Verlag (March 1999), 91-108.
Parts of this paper are subsumed by a journal paper (see citation).
© Springer-Verlag.
A Core Calculus of Dependency
[with Anindya Banerjee, Nevin Heintze, and Jon G. Riecke]
Proceedings of the 26th Annual ACM Symposium on Principles of Programming
Languages (January 1999), 147-160.
© ACM.
A Type System for Java Bytecode Subroutines
[with Raymie Stata]
ACM Transactions on Programming Languages and Systems 21, 1 (January 1999),
90-137.
Also appeared as SRC Research Report 158 (June 1998).
© ACM.
A Calculus for Cryptographic Protocols: The Spi Calculus
[with Andrew D. Gordon]
Information and Computation 148, 1 (January 1999), 1-70.
© Academic Press.
An extended version of this paper appeared as SRC
Research Report 149 (January 1998), and, in preliminary form, as Technical
Report 414, University of Cambridge Computer Laboratory (January 1997).
Protection in Programming-Language
Translations
Automata, Languages and Programming: 25th International Colloquium, ICALP'98,
Springer-Verlag (July 1998), 868-883.
Also appeared as SRC Research Report 154 (April 1998).
© Springer-Verlag.
Secure Implementation of Channel Abstractions
[with Cédric Fournet and Georges Gonthier]
Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer
Science (June 1998), 105-116.
This paper is subsumed by a journal paper (see citation).
© IEEE.
Two Facets of Authentication
Proceedings of the 11th IEEE Computer Security Foundations Workshop (June
1998), 25-32.
Also appeared as SRC Technical Note 1998-007 (March 1998).
This paper is subsumed by Security Protocols and their Properties (see citation).
© IEEE.
Secure Web Tunneling
[with Andrew Birrell, Raymie Stata, and Edward Wobber]
Proceedings of the Seventh International World Wide Web Conference. Computer
Networks and ISDN Systems 30, 1-7 (April 1998), 531-539.
© Elsevier Science.
A Bisimulation Method for Cryptographic Protocols
[with Andrew D. Gordon]
Programming Languages and Systems: 7th European Symposium on Programming, ESOP
'98 (April 1998), 12-26.
This is a preliminary version of a journal paper (see citation).
A Bisimulation Method
for Cryptographic Protocols
[with Andrew D. Gordon]
Nordic Journal of Computing 5, 4 (Winter 1998), 267-303.
© Publishing Association Nordic Journal of
Computing.
A Type System for Java Bytecode Subroutines
[with Raymie Stata]
Proceedings of the 25th Annual ACM Symposium on Principles of Programming
Languages (January 1998), 149-160.
This is a preliminary version of a journal paper (see citation).
On SDSI's Linked Local Name Spaces
Journal of Computer Security 6, 1-2 (1998), 3-21.
(This paper is largely based on SDSI 1.1, by Rivest and Lampson; a copy of
their description of SDSI 1.1 is here.)
© IOS Press.
Strengthening Passwords
[with T. Mark A. Lomas and Roger Needham]
SRC Technical Note 1997-033 (September/December 1997).
(Also in html.)
Secrecy by Typing in Security Protocols
Theoretical Aspects of Computer Software, Springer-Verlag (September 1997),
611-638.
This is a preliminary version of a journal paper (see citation).
Reasoning about Cryptographic Protocols in the Spi
Calculus
[with Andrew D. Gordon]
CONCUR'97, Springer-Verlag (July 1997), 59-73.
This is a preliminary version of part of a journal paper (see citation).
On SDSI's Linked Local Name Spaces
Proceedings of the 10th IEEE Computer Security Foundations Workshop (June
1997), 98-108.
This is a preliminary version of a journal paper (see citation).
A Calculus for Cryptographic Protocols: The Spi
Calculus
[with Andrew D. Gordon]
Proceedings of the 4th ACM Conference on Computer and Communications Security
(April 1997), 36-47.
This is a preliminary version of part of a journal paper (see citation).
A Logic of Object-Oriented Programs
[with K. Rustan M. Leino]
TAPSOFT '97: Theory and Practice of Software Development, Springer-Verlag
(April 1997), 682-696.
© Springer-Verlag.
This is a preliminary version of a paper in a collection (see citation).
Explicit Communication Revisited: Two New
Attacks on Authentication Protocols
IEEE Transactions on Software Engineering 23, 3 (March 1997), 185-186.
© IEEE.
Formal, Informal, and Null Methods
Position statement for National Research Council workshop on Information
Systems Trustworthiness (January 1997).
A TLA Solution to the RPC-Memory
Specification Problem
[with Leslie Lamport and Stephan Merz]
Formal Systems Specification: The RPC-Memory Specification Case Study,
Springer-Verlag (December 1996), 21-66.
© Springer-Verlag.
On Subtyping and Matching
[with Luca Cardelli]
ACM Transactions on Programming Languages and Systems 18, 4 (July 1996),
401-423.
See A Theory of Objects.
Syntactic Considerations on Recursive Types
[with Marcelo Fiore]
Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science
(July 1996), 242-252.
© IEEE.
Secure Network Objects
[with Leendert van Doorn, Mike Burrows, and Edward Wobber]
Proceedings of the 1996 IEEE Symposium on Security and Privacy (May 1996),
211-221.
© IEEE.
Analysis and Caching of Dependencies
[with Jean-Jacques Lévy and Butler Lampson]
Proceedings of the 1996 ACM International Conference on Functional Programming
(May 1996), 83-91.
© ACM
A Theory of Primitive Objects:
Untyped and First-Order Systems
[with Luca Cardelli]
Information and Computation 125, 2 (March 1996), 78-102.
See A Theory of Objects.
An Interpretation of Objects and Object Types
[with Luca Cardelli and Ramesh Viswanathan]
Proceedings of the 23rd Annual ACM Symposium on Principles of
Programming Languages (January 1996), 396-409.
See A Theory of Objects.
Prudent Engineering Practice
for Cryptographic Protocols
[with Roger Needham]
IEEE Transactions on Software Engineering 22, 1 (January 1996),
6-15.
©
IEEE.
A Theory of Primitive Objects: Second-Order Systems
[with Luca Cardelli]
Science of Computer Programming 25, 2-3 (December 1995), 81-116.
See A Theory of Objects.
Methods as Assertions
[with John Lamping]
Theory and Practice of Object Systems 1, 1 (1995), 5-18.
©
John Wiley & Sons.
An Imperative Object Calculus
[with Luca Cardelli]
Theory and Practice of Object Systems 1, 3 (1995), 151-166.
See A Theory of Objects.
The Millicent Protocol for Inexpensive
Electronic Commerce
[with Steve Glassman, Mark Manasse, Paul Gauthier, and Patrick Sobalvarro]
World Wide Web Journal -- Fourth International World Wide Web Conference
Proceedings, O'Reilly & Associates, Inc. (December 1995), 603-618.
© O'Reilly & Associates.
An Abstract Account of Composition
[with Stephan Merz]
Mathematical Foundations of Computer Science, Springer-Verlag (August 1995),
499-508.
© Springer-Verlag.
On Subtyping and Matching
[with Luca Cardelli]
ECOOP '95 -- Object-Oriented Programming, Springer-Verlag (August 1995),
145-167.
See A Theory of Objects.
An Imperative Object Calculus
[with Luca Cardelli]
TAPSOFT '95: Theory and Practice of Software Development, Springer-Verlag (May
1995), 471-485.
This is a preliminary version of a journal paper (see citation).
See A Theory of Objects.
Conjoining Specifications
[with Leslie Lamport]
ACM Transactions on Programming Languages and Systems 17, 3 (May 1995),
507-534.
Also appeared as SRC Research Report 118.
© ACM.
A Model for Formal Parametric Polymorphism: A PER
Interpretation for System R
[with Roberto Bellucci and Pierre-Louis Curien]
Typed Lambda Calculi and Applications -- TLCA '95, Springer-Verlag (April
1995), 32-46.
© Springer-Verlag.
An Imperative Object Calculus: Basic Typing and Soundness
[with Luca Cardelli]
SIPL '95 - Proceedings of the Second ACM SIGPLAN Workshop on State in
Programming Languages, Technical Report UIUCDCS-R-95-1900, Department of
Computer Science, University of Illinois at Urbana-Champaign (January 1995),
19-32.
See A Theory of Objects.
Dynamic Typing in Polymorphic Languages
[with Luca Cardelli, Benjamin Pierce, and Didier Rémy]
Journal of Functional Programming 5, 1 (January 1995), 111-130.
Also appeared as SRC Research Report 120.
© Cambridge University Press.
An Old-Fashioned Recipe for Real Time
[with Leslie Lamport]
ACM Transactions on Programming Languages and Systems 16, 5 (September 1994),
1543-1571.
Also appeared as SRC Research Report 91.
© ACM.
On TLA as a Logic
[with Stephan Merz]
Deductive Program Design, NATO ASI Series, Springer-Verlag (1995), 235-271.
Proceedings of the NATO Advanced Study Institute on Deductive Program Design,
held in Marktoberdorf, Germany (1994).
© Springer-Verlag.
Open Systems in TLA
[with Leslie Lamport]
Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed
Computing (August 1994), 81-90.
This is subsumed by the journal paper Conjoining Specifications (see citation).
© ACM.
Methods as Assertions
[with John Lamping]
Object-Oriented Programming - Eighth European Conference, ECOOP '94,
Springer-Verlag (July 1994), 60-80.
This is a preliminary version of a journal paper (see citation).
A Semantics of Object Types
[with Luca Cardelli]
Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science
(July 1994), 332-341.
See A Theory of Objects.
Subtyping and
Parametricity
[with Gordon Plotkin and Luca Cardelli]
Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science
(July 1994), 310-319.
© IEEE.
Decidability and Expressiveness
for First-order Logics of Probability
[with Joe Halpern]
Information and Computation 112, 1 (July 1994), 1-36.
Also appeared as SRC Research Report 73.
© Academic Press.
Decomposing Specifications of Concurrent Systems
[with Leslie Lamport]
Programming Concepts, Methods and Calculi: Proceedings of the IFIP
TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and
Calculi, North-Holland (June 1994), 327-340.
This is subsumed by the journal paper Conjoining Specifications (see citation).
Prudent Engineering Practice for Cryptographic Protocols
[with Roger Needham]
Proceedings of the 1994 IEEE Symposium on Security and Privacy (May 1994),
122-136.
Also appeared as SRC Research Report 125.
This is a preliminary version of a journal paper (see citation).
Baby Modula-3 and a Theory of
Objects
Journal of Functional Programming 4, 2 (April 1994), 249-283.
Also appeared as SRC Research Report 95.
© Cambridge University Press.
A Theory of Primitive Objects: Second-Order Systems
[with Luca Cardelli]
Programming Languages and Systems -- ESOP '94, Springer-Verlag (April 1994),
1-25.
This is a preliminary version of a journal paper (see citation).
See A Theory of Objects.
A Theory of Primitive Objects: Untyped and First-Order Systems
[with Luca Cardelli]
Theoretical Aspects of Computer Software, Springer-Verlag (April 1994),
296-320.
This is a preliminary version of a journal paper (see citation).
See A Theory of Objects.
A Semantics for Static Type Inference in a
Nondeterministic Language
Information and Computation 109, 1-2 (February/March 1994), 300-306.
© Academic Press.
Extensible Syntax with Lexical Scoping
[with Luca Cardelli and Florian Matthes]
SRC Research Report 121 (February 1994).
Extensible Grammars for Language Specialization
[with Luca Cardelli and Florian Matthes]
Database Programming Languages (DBPL-4), Springer-Verlag (February 1994),
11-31.
This is a preliminary version of the report Extensible Syntax with Lexical
Scoping (see citation).
Authentication in the Taos Operating
System
[with Edward Wobber, Michael Burrows, and Butler Lampson]
ACM Transactions on Computer Systems 12, 1 (February 1994), 3-32.
Also appeared as SRC Research Report 117.
© ACM.
Formal Parametric Polymorphism
[with Luca Cardelli and Pierre-Louis Curien]
Theoretical Computer Science 121, 1-2, A Collection of Contributions in Honour of Corrado Boehm on the Occasion
of his 70th Birthday (December 1993), 9-58.
Also appeared as SRC Research Report 109.
© Elsevier Science.
Authentication in the Taos Operating System
[with Edward Wobber, Michael Burrows, and Butler Lampson]
Proceedings of the Fourteenth Symposium on Operating System Principles
(December 1993), 256-269.
This is a preliminary version of a journal paper (see citation).
Authentication and Delegation with
Smart-Cards
[with Michael Burrows, Charles Kaufman, and Butler Lampson]
Science of Computer Programming 21, 2 (October 1993), 93-113.
© Elsevier Science.
A Calculus for Access
Control in Distributed Systems
[with Michael Burrows, Butler Lampson, and Gordon Plotkin]
ACM Transactions on Programming Languages and Systems 15, 4 (September 1993),
706-734.
Also appeared as SRC Research Report 70.
© ACM.
A Logical View of
Composition
[with Gordon Plotkin]
Theoretical Computer Science 114, 1 (June 1993), 3-30.
Also appeared as SRC Research Report 86.
© Elsevier Science.
A Logic for Parametric Polymorphism
[with Gordon Plotkin]
Typed Lambda Calculi and Applications -- TLCA '93, Springer-Verlag (March
1993), 361-375.
© Springer-Verlag.
Formal Parametric Polymorphism
[with Luca Cardelli and Pierre-Louis Curien]
Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming
Languages (January 1993), 157-170.
This is a preliminary version of a journal paper (see citation).
Composing Specifications
[with Leslie Lamport]
ACM Transactions on Programming Languages and Systems 15, 1 (January 1993),
73-132.
Also appeared as SRC Research Report 66.
© ACM.
Authentication in Distributed Systems: Theory
and Practice
[with Butler Lampson, Michael Burrows, and Edward Wobber]
ACM Transactions on Computer Systems 10, 4 (November 1992), 265-310.
Also appeared as SRC Research Report 83.
© ACM.
Dynamic Typing in Polymorphic Languages
[with Luca Cardelli, Benjamin Pierce, and Didier Rémy]
ACM Sigplan Workshop on ML and its Applications,
Technical Report CMU-CS-93-105, School of Computer Science, Carnegie Mellon
University (June 1992), 92-103.
This is a preliminary version of a journal paper (see citation).
Linear Logic Without Boxes
[with Georges Gonthier and Jean-Jacques Lévy]
Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science
(June 1992), 223-234.
© IEEE.
The Geometry of Optimal Lambda Reduction
[with Georges Gonthier and Jean-Jacques Lévy]
Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming
Languages (January 1992), 15-26.
© ACM.
Preserving Liveness: Comments on `Safety and
Liveness from a Methodological Point of View'
[with Bowen Alpern, Krzysztof Apt, Nissim Francez, Shmuel Katz, Leslie Lamport, and Fred Schneider]
Information Processing Letters 40, 3 (November 1991), 141-142.
© Elsevier Science.
Authentication in Distributed Systems: Theory and Practice
[with Butler Lampson, Michael Burrows, and Edward Wobber]
Proceedings of the Thirteenth Symposium on Operating System Principles (October
1991), 165-182.
This is a preliminary version of a journal paper (see citation).
Explicit Substitutions
[with Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy]
Journal of Functional Programming 1, 4 (October 1991), 375-416.
Also appeared as SRC Research Report 54.
© Cambridge University Press.
Authentication and Delegation with Smart-Cards
[with Michael Burrows, Charles Kaufman, and Butler Lampson]
Theoretical Aspects of Computer Software, Springer-Verlag (September 1991),
326-345.
Also appeared as SRC Research Report 67.
This is a preliminary version of a journal paper (see citation).
A Calculus for Access Control in Distributed Systems
[with Michael Burrows, Butler Lampson, and Gordon Plotkin]
Advances in Cryptology -- CRYPTO '91, Springer-Verlag (August 1991), 1-23.
This is a preliminary version of a journal paper (see citation).
A Semantics for a Logic of Authentication
[with Mark Tuttle]
Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing
(August 1991), 201-216.
© ACM.
Faithful Ideal Models for Recursive
Polymorphic Types
[with Benjamin Pierce and Gordon Plotkin]
International Journal of Foundations of Computer Science 2, 1 (August 1991),
1-21.
© World Scientific Publishing.
An Old-Fashioned Recipe for Real Time
[with Leslie Lamport]
Real-Time: Theory in Practice, Springer-Verlag (June 1991), 1-27.
This is a preliminary version of a journal paper (see citation).
The Existence of Refinement Mappings
[with Leslie Lamport]
Theoretical Computer Science 82, 2 (May 1991), 253-284.
Also appeared as SRC Research Report 29.
© Elsevier Science.
Dynamic Typing in a Statically-Typed Language
[with Luca Cardelli, Benjamin Pierce, and Gordon Plotkin]
ACM Transactions on Programming Languages and Systems 13, 2 (April 1991),
237-268.
Also appeared as SRC Research Report 47.
© ACM.
A Logical View of Composition and Refinement
[with Gordon Plotkin]
Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming
Languages (January 1991), 323-332.
Part of this is a preliminary version of the journal paper A Logical View of
Composition (see citation).
© ACM.
An Axiomatization of Lamport's
Temporal Logic of Actions
CONCUR '90, Springer-Verlag (August 1990), 57-69.
Also appeared as SRC Research Report 65.
© Springer-Verlag.
A Per Model of Polymorphism and Recursive Types
[with Gordon Plotkin]
Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science
(June 1990), 355-365.
© IEEE.
Secure Circuit Evaluation: A Protocol Based
on Hiding Information from an Oracle
[with Joan Feigenbaum]
Journal of Cryptology 2, 1 (May 1990), 1-12.
© Springer-Verlag.
Nonclausal Deduction in First-order Temporal Logic
[with Zohar Manna]
Journal of the ACM 37, 2 (April 1990), 279-317.
Explicit Substitutions
[with Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy]
Proceedings of the Sixteenth Annual ACM Symposium on Principles of Programming
Languages (January 1990), 31-46.
This is a preliminary version of a journal paper (see citation).
A Logic of Authentication
[with Michael Burrows and Roger Needham]
Proceedings of the Royal Society, Series A, 426, 1871 (December 1989), 233-271.
Also appeared as SRC Research Report 39 and, in a shortened form, in ACM
Transactions on Computer Systems 8, 1 (February 1990), 18-36.
© Royal Society.
A Logic of Authentication
[with Michael Burrows and Roger Needham]
Proceedings of the Twelfth Symposium on Operating System Principles (December
1989), 1-13.
This is a preliminary version of a journal paper (see citation).
The Scope of a Logic of Authentication
[with Michael Burrows and Roger Needham]
Distributed Computing and Cryptography: Proceedings of a DIMACS Workshop
(October 1989), 119-126.
Also appeared as appendix to SRC Research Report 39.
© American Mathematical Society.
Decidability and Expressiveness for
First-order Logics of Probability
[with Joe Halpern]
Proceedings of the 30th Annual Symposium on the Foundations of Computer Science
(October 1989), 148-153.
This is a preliminary version of a journal paper (see citation).
Temporal Logic Programming
[with Zohar Manna]
Journal of Symbolic Computation 8, 3 (September 1989), 277-295.
On Hiding Information from an Oracle
[with Joan Feigenbaum and Joe Kilian]
Journal of Computer and System Sciences 39, 1 (August 1989), 21-50.
© John Wiley & Sons.
Realizable and Unrealizable Specifications of Reactive Systems
[with Leslie Lamport and Pierre Wolper]
Automata, Languages and Programming: 16th International Colloquium, ICALP'89,
Springer-Verlag (July 1989), 1-17.
© Springer-Verlag.
The Power
of Temporal Proofs
Theoretical Computer Science 65, 1 (June 1989), 35-84. See corrigendum in Theoretical
Computer Science 70 (1990), 275.
Also appeared as SRC Research Report 30.
Faithful Ideal Models for Recursive
Polymorphic Types
[with Benjamin Pierce and Gordon Plotkin]
Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science
(June 1989), 216-225.
This is a preliminary version of a journal paper (see citation).
Dynamic Typing in a Statically-Typed
Language
[with Luca Cardelli, Benjamin Pierce, and Gordon Plotkin]
Proceedings of the Sixteenth Annual ACM Symposium on Principles of Programming
Languages (January 1989), 213-227.
This is a preliminary version of a journal paper (see citation).
Composing Specifications
[with Leslie Lamport]
Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness,
Springer-Verlag (May 1989), 1-41.
This is a preliminary version of a journal paper (see citation).
On Generating Solved Instances of Computational
Problems
[with Eric Allender, Andrei Broder, Joan Feigenbaum, and Lane Hemachandra]
Advances in Cryptology -- CRYPTO '88, Springer-Verlag (August 1988), 297-310.
© Springer-Verlag.
The Existence of Refinement Mappings
[with Leslie Lamport]
Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science
(July 1988), 165-177.
This is a preliminary version of a journal paper (see citation).
Authentication: A Practical Study in Belief and Action
[with Michael Burrows and Roger Needham]
Proceedings of the 2nd Conference in Theoretical Aspects of Reasoning about
Knowledge, Morgan Kaufmann (March 1988), 325-342.
This paper is subsumed by the journal paper A Logic of Authentication (see citation).
A Simple Protocol for Secure Circuit Evaluation
[with Joan Feigenbaum]
STACS 88, Springer-Verlag (February 1988), 264-272.
This paper is subsumed by the journal paper Secure Circuit Evaluation: A
Protocol Based on Hiding Information from an Oracle (see citation).
Temporal Logic Programming
[with Zohar Manna]
Proceedings of the 1987 Symposium on Logic Programming (August 1987), 4-16.
This is a preliminary version of a journal paper (see citation).
The Power of Temporal Proofs
Proceedings of the IEEE Symposium on Logic in Computer Science (June 1987),
123-130.
This is a preliminary version of a journal paper (see citation).
On Hiding Information from an Oracle
[with Joan Feigenbaum and Joe Kilian]
Proceedings of the Nineteenth Annual ACM Symposium on the Theory of Computing
(May 1987), 195-203.
This is a preliminary version of a journal paper (see citation).
Temporal-Logic Theorem Proving
Doctoral Thesis, Stanford University (March 1987).
Modal Theorem Proving
[with Zohar Manna]
Proceedings of the 8th International Conference on Automated Deduction,
Springer-Verlag (July 1986) 172-189.
A Timely Resolution
[with Zohar Manna]
Proceedings of the IEEE Symposium on Logic in Computer Science (June 1986),
176-186.
This paper is subsumed by the journal paper Nonclausal
Deduction in First-order Temporal Logic (see citation).
Nonclausal Temporal Deduction
[with Zohar Manna]
Logics of Programs, Springer-Verlag (June 1985), 1-15.
This paper is subsumed by the journal paper Nonclausal
Deduction in First-order Temporal Logic (see citation).