Papers

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.


Falkirk Wheel: Rollback Recovery for Dataflow Systems
[with Ionel Gog and Michael Isard]
Proceedings of the 2021 ACM Symposium on Cloud Computing (November 2021), 373-387.

Smart Choices and the Selection Monad
[with Gordon Plotkin]
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (June/July 2021), 1-14.
The arXiv version contains minor corrections and additional details.

A Simple Differentiable Programming Language
[with Gordon Plotkin]
Proceedings of the ACM on Programming Languages (January 2020), 38:1-38:28.

Dynamic Control Flow in Large-Scale Machine Learning
[with Yuan Yu, Paul Barham, Eugene Brevdo, Mike Burrows, Andy Davis, Jeff Dean, Sanjay Ghemawat, Tim Harley, Peter Hawkins, Michael Isard, Manjunath Kudlur, Rajat Monga, Derek Murray, and Xiaoqiang Zheng]
Proceedings of the Thirteenth EuroSys Conference (April 2018), 18:1-18:15.

The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication
[with Bruno Blanchet and Cédric Fournet]
Journal of the ACM 65, 1 (January 2018), 1:1-1:41.

Adversarial Patch
[with Tom B. Brown, Dandelion Mané, Aurko Roy, and Justin Gilmer]
arXiv e-print (December 2017).

On the Protection of Private Information in Machine Learning Systems: Two Recent Approaches
[with Nicolas Papernot, Úlfar Erlingsson, Ian Goodfellow, H. Brendan McMahan, Ilya Mironov, Kunal Talwar, and Li Zhang]
Proceedings of the 30th IEEE Computer Security Foundations Symposium (August 2017), 1-6 (invited paper).

A Computational Model for TensorFlow (An Introduction)
[with Michael Isard and Derek G. Murray]
Proceedings of the 1st ACM SIGPLAN International Workshop on Machine Learning and Programming Languages (June 2017), 1-7.

Semi-supervised Knowledge Transfer for Deep Learning from Private Training Data
[with Nicolas Papernot, Úlfar Erlingsson, Ian Goodfellow, and Kunal Talwar]
Presented at the 5th International Conference on Learning Representations (April 2017).

Learning a Natural Language Interface with Neural Programmer
[with Arvind Neelakantan, Quoc V. Le, Andrew McCallum, and Dario Amodei]
Presented at 5th International Conference on Learning Representations (April 2017).

Learning to Protect Communications with Adversarial Neural Cryptography
[with David G. Andersen]
arXiv e-print (October 2016).

TensorFlow: A System for Large-Scale Machine Learning
[with Paul Barham, Jianmin Chen, Zhifeng Chen, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Geoffrey Irving, Michael Isard, Manjunath Kudlur, Josh Levenberg, Rajat Monga, Sherry Moore, Derek Gordon Murray, Benoit Steiner, Paul A. Tucker, Vijay Vasudevan, Pete Warden, Martin Wicke, Yuan Yu, and Xiaoqiang Zhang]
Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (November 2016), 265-283.

Deep Learning with Differential Privacy
[with Andy Chu, Ian Goodfellow, H. Brendan McMahan, Ilya Mironov, Kunal Talwar, and Li Zhang]
Proceedings of the 23rd ACM Conference on Computer and Communications Security (October 2016), 308-318.
The arXiv version contains minor corrections and additional details.

Incremental, Iterative Data Processing with Timely Dataflow
[with Derek G. Murray, Frank McSherry, Rebecca Isaacs, Michael Isard, and Paul Barham]
Communications of the ACM 59, 10 (October 2016), 75-83.

TensorFlow: Learning Functions at Scale
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (September 2016), 1.

TensorFlow: Large-Scale Machine Learning on Heterogeneous Distributed Systems
[with Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Rafal Jozefowicz, Yangqing Jia, Lukasz Kaiser, Manjunath Kudlur, Josh Levenberg, Dan Mané, Mike Schuster, Rajat Monga, Sherry Moore, Derek Murray, Chris Olah, Jonathon Shlens, Benoit Steiner, Ilya Sutskever, Kunal Talwar, Paul Tucker, Vincent Vanhoucke, Vijay Vasudevan, Fernanda Viégas, Oriol Vinyals, Pete Warden, Martin Wattenberg, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng]
Preliminary White Paper (November 2015).

Distributed Authorization with Distributed Grammars
[with Mike Burrows, Himabindu Pucha, Adam Sadovsky, Asim Shankar, and Ankur Taly]
Programming Languages with Applications to Biology and Security -- Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday, Springer-Verlag (October 2015), 10-26.
© Springer-Verlag.

Timely Dataflow: A Model
[with Michael Isard]
Formal Methods for Networked and Distributed Systems, FORTE 2015, Springer-Verlag (June 2015), 131-145.
The on-line version includes an additional appendix.

Timely Rollback: Specification and Verification
[with Michael Isard]
7th NASA Formal Methods Symposium, Springer-Verlag (April 2015), 19-34.
The on-line version includes an additional appendix.

On the Flow of Data, Information, and Time
[with Michael Isard]
Principles of Security and Trust -- Fourth International Conference, POST 2015, Springer-Verlag (April 2015), 73-92.
The on-line version includes an additional appendix.

The Prophecy of Undo
18th International Conference on Fundamental Approaches to Software Engineering, FASE 2015, Springer-Verlag (April 2015), 347-361.
The on-line version includes an additional appendix.

Foundations of Differential Dataflow
[with Frank McSherry and Gordon Plotkin]
Foundations of Software Science and Computation Structures, FOSSACS 2015, Springer-Verlag (April 2015), 71-83.
The on-line version includes an additional appendix.

Understanding TypeScript
[with Gavin Bierman and Mads Torgersen]
Object-Oriented Programming -- ECOOP 2014, Springer-Verlag (July 2014), 257-281.
© Springer-Verlag.

Layout Randomization and Nondeterminism
[with Jérémy Planul and Gordon Plotkin]
Horizons of the Mind. A Tribute to Prakash Panangaden -- Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday, Springer-Verlag (June 2014), 1-39.
© Springer-Verlag.

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.

Early Security Classification of Skype Users via Machine Learning
[with Anna Leontjeva, Moises Goldszmidt, Yinglian Xie, and Fang Yu]
2013 ACM Workshop on Artificial Intelligence and Security  (November 2013).
© ACM.

Message-Locked Encryption for Lock-Dependent Messages
[with Dan Boneh, Ilya Mironov, Ananth Raghunathan, and Gil Segev]
Advances in Cryptology -- CRYPTO 2013, Springer-Verlag (August 2013), 374-391.
© Springer-Verlag.

Formal Analysis of a Distributed Algorithm for Tracking Progress
[with Frank McSherry, Derek G. Murray, and Thomas L. Rodeheffer]
2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems, Springer-Verlag (June 2013), 5-19.
© Springer-Verlag.

Layout Randomization and Nondeterminism
[with Jérémy Planul and Gordon Plotkin]
Mathematical Foundations of Programming Semantics---Twenty-ninth Conference, Electronic Notes in Computer Science 298 (November 2013), 29-50.
This is a preliminary version of a longer work (see citation).
© Elsevier Science.

Global Authentication in an Untrustworthy World
[with Andrew Birrell, Ilya Mironov, Ted Wobber, and Yinglian Xie]
HotOS XIV: Fourteenth Workshop on Hot Topics in Operating Systems (May 2013).

SocialWatch: Detection of Online Service Abuse via Large-Scale Social Graphs
[with Junxian Huang, Yinglian Xie, Fang Yu, Qifa Ke, Eliot Gillum, and Z. Morley Mao]
Proceedings of the 8th ACM Symposium on Information, Computer and Communications Security (ASIACCS 2013) (May 2013).
© ACM.

On Layout Randomization for Arrays and Functions
[with Jérémy Planul]
Principles of Security and Trust -- Second International Conference, POST 2013, Springer-Verlag (March 2013), 167-185.
© Springer-Verlag.

A Functional View of Imperative Information Flow
[with Thomas Austin and Cormac Flanagan]
Proceedings of the Tenth ASIAN Symposium on Programming Languages and Systems -- APLAS 2012, Springer-Verlag (December 2012), 34-49.
© Springer-Verlag.

Innocent by Association: Early Recognition of Legitimate Users
[with Yinglian Xie, Fang Yu, Qifa Ke, Eliot Gillum, Krish Vitaldevaria, Jason Walter, Junxian Huang, and Z. Morley Mao]
Proceedings of the 19th ACM Conference on Computer and Communications Security (October 2012), 353-364.
© ACM.

Software Security: A Formal Perspective (Notes for a Talk)
FM 2012: 18th International Symposium on Formal Methods, Springer-Verlag (August 2012), 1-5.
© Springer-Verlag.

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).


Martín Abadi