Jump to Content
Martín Abadi

Martín Abadi

Martín Abadi has been at Google since November 2014. A list of publications (going back to 1985) and other information is in web pages at UC Santa Cruz (where he is now Emeritus).
Authored Publications
Google Publications
Other Publications
Sort By
  • Title
  • Title, descending
  • Year
  • Year, descending
    Dynamic Control Flow in Large-Scale Machine Learning
    Yuan Yu
    Eugene Brevdo
    Mike Burrows
    Tim Harley
    Peter Hawkins
    Manjunath Kudlur
    Rajat Monga
    Xiaoqiang Zheng
    Proceedings of EuroSys 2018
    Preview abstract Many recent machine learning models rely on fine-grained dynamic control flow for training and inference. In particular, models based on recurrent neural networks and on reinforcement learning depend on recurrence relations, data-dependent conditional execution, and other features that call for dynamic control flow. These applications benefit from the ability to make rapid control-flow decisions across a set of computing devices in a distributed system. For performance, scalability, and expressiveness, a machine learning system must support dynamic control flow in distributed and heterogeneous environments. This paper presents a programming model for distributed machine learning that supports dynamic control flow. We describe the design of the programming model, and its implementation in TensorFlow, a distributed machine learning system. Our approach extends the use of dataflow graphs to represent machine learning models, offering several distinctive features. First, the branches of conditionals and bodies of loops can be partitioned across many machines to run on a set of heterogeneous devices, including CPUs, GPUs, and custom ASICs. Second, programs written in our model support automatic differentiation and distributed gradient computations, which are necessary for training machine learning models that use control flow. Third, our choice of non-strict semantics enables multiple loop iterations to execute in parallel across machines, and to overlap compute and I/O operations. We have done our work in the context of TensorFlow, and it has been used extensively in research and production. We evaluate it using several real-world applications, and demonstrate its performance and scalability. View details
    A Computational Model for TensorFlow (An Introduction)
    1st ACM SIGPLAN Workshop on Machine Learning and Programming Languages (MAPL 2017) (2017)
    Preview abstract TensorFlow is a powerful, programmable system for machine learning. This paper aims to provide the basics of a conceptual framework for understanding the behavior of TensorFlow models during training and inference: it describes an operational semantics, of the kind common in the literature on programming languages. More broadly, the paper suggests that a programming-language perspective is fruitful in designing and in explaining systems such as TensorFlow. View details
    Adversarial Patch
    Tom Brown
    Dandelion Mane
    Aurko Roy
    Justin Gilmer
    NIPS Workshop (2017)
    Preview abstract We present a method to create universal, robust, targeted adversarial image patches in the real world. The patches are universal because they can be used to attack any scene, robust because they work under a wide variety of transformations, and targeted because they can cause a classifier to output any target class. These adversarial patches can be printed, added to any scene, photographed, and presented to image classifiers; even when the patches are small, they cause the classifiers to ignore the other items in the scene and report a chosen target class. View details
    Preview abstract We study the interaction of the programming construct ``new'', which generates statically scoped names, with communication via messages on channels. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. We define the applied pi calculus, a simple, general extension of the pi calculus in which values can be formed from names via the application of built-in functions, subject to equations, and be sent as messages. (In contrast, the pure pi calculus lacks built-in functions; its only messages are atomic names.) We develop semantics and proof techniques for this extended language and apply them in reasoning about security protocols. This paper essentially subsumes the conference paper that introduced the applied pi calculus in 2001. It fills gaps, incorporates improvements, and further explains and studies the applied pi calculus. Since 2001, the applied pi calculus has been the basis for much further work, described in many research publications and sometimes embodied in useful software, such as the tool ProVerif, which relies on the applied pi calculus to support the specification and automatic analysis of security protocols. Although this paper does not aim to be a complete review of the subject, it benefits from that further work and provides better foundations for some of it. In particular, the applied pi calculus has evolved through its implementation in ProVerif, and the present definition reflects that evolution. View details
    Semi-supervised Knowledge Transfer for Deep Learning from Private Training Data
    Nicolas Papernot
    Úlfar Erlingsson
    Ian Goodfellow
    Kunal Talwar
    Proceedings of the International Conference on Learning Representations (2017)
    Preview abstract Some machine learning applications involve training data that is sensitive, such as the medical histories of patients in a clinical trial. A model may inadvertently and implicitly store some of its training data; careful analysis of the model may therefore reveal sensitive information. To address this problem, we demonstrate a generally applicable approach to providing strong privacy guarantees for training data: Private Aggregation of Teacher Ensembles (PATE). The approach combines, in a black-box fashion, multiple models trained with disjoint datasets, such as records from different subsets of users. Because they rely directly on sensitive data, these models are not published, but instead used as “teachers” for a “student” model. The student learns to predict an output chosen by noisy voting among all of the teachers, and cannot directly access an individual teacher or the underlying data or parameters. The student’s privacy properties can be understood both intuitively (since no single teacher and thus no single dataset dictates the student’s training) and formally, in terms of differential privacy. These properties hold even if an adversary can not only query the student but also inspect its internal workings. Compared with previous work, the approach imposes only weak assumptions on how teachers are trained: it applies to any model, including non-convex models like DNNs. We achieve state-of-the-art privacy/utility trade-offs on MNIST and SVHN thanks to an improved privacy analysis and semi-supervised learning. View details
    Preview abstract Learning a natural language interface for database tables is a challenging task that involves deep language understanding and multi-step reasoning. The task is often approached by mapping natural language queries to logical forms or programs that provide the desired response when executed on the database. To our knowledge, this paper presents the first weakly supervised, end-to-end neural network model to induce such programs on a real-world dataset. We enhance the objective function of Neural Programmer, a neural network with built-in discrete operations, and apply it on WikiTableQuestions, a natural language question-answering dataset. The model is trained end-to-end with weak supervision of question-answer pairs, and does not require domain-specific grammars, rules, or annotations that are key elements in previous approaches to program induction. The main experimental result in this paper is that a single Neural Programmer model achieves 34.2% accuracy using only 10,000 examples with weak supervision. An ensemble of 15 models, with a trivial combination technique, achieves 37.2% accuracy, which is competitive to the current state-of-the-art accuracy of 37.1% obtained by a traditional natural language semantic parser. View details
    On the Protection of Private Information in Machine Learning Systems: Two Recent Approaches
    Úlfar Erlingsson
    Ian Goodfellow
    Nicolas Papernot
    Ilya Mironov
    Kunal Talwar
    Li Zhang
    Proceedings of 30th IEEE Computer Security Foundations Symposium (CSF) (2017), pp. 1-6
    Preview abstract The recent, remarkable growth of machine learning has led to intense interest in the privacy of the data on which machine learning relies, and to new techniques for preserving privacy. However, older ideas about privacy may well remain valid and useful. This note reviews two recent works on privacy in the light of the wisdom of some of the early literature, in particular the principles distilled by Saltzer and Schroeder in the 1970s. View details
    Preview abstract We ask whether neural networks can learn to use secret keys to protect information from other neural networks. Specifically, we focus on ensuring confidentiality properties in a multiagent system, and we specify those properties in terms of an adversary. Thus, a system may consist of neural networks named Alice and Bob, and we aim to limit what a third neural network named Eve learns from eavesdropping on the communication between Alice and Bob. We do not prescribe specific cryptographic algorithms to these neural networks; instead, we train end-to-end, adversarially. We demonstrate that the neural networks can learn how to perform forms of encryption and decryption, and also how to apply these operations selectively in order to meet confidentiality goals. View details
    TensorFlow: A system for large-scale machine learning
    Jianmin Chen
    Matthieu Devin
    Geoffrey Irving
    Manjunath Kudlur
    Rajat Monga
    Benoit Steiner
    Paul Tucker
    Vijay Vasudevan
    Pete Warden
    Yuan Yu
    Xiaoqiang Zheng
    12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), USENIX Association (2016), pp. 265-283
    Preview abstract TensorFlow is a machine learning system that operates at large scale and in heterogeneous environments. TensorFlow uses dataflow graphs to represent computation, shared state, and the operations that mutate that state. It maps the nodes of a dataflow graph across many machines in a cluster, and within a machine across multiple computational devices, including multicore CPUs, general-purpose GPUs, and custom-designed ASICs known as Tensor Processing Units (TPUs). This architecture gives flexibility to the application developer: whereas in previous “parameter server” designs the management of shared state is built into the system, TensorFlow enables developers to experiment with novel optimizations and training algorithms. TensorFlow supports a variety of applications, with a focus on training and inference on deep neural networks. Several Google services use TensorFlow in production, we have released it as an open-source project, and it has become widely used for machine learning research. In this paper, we describe the TensorFlow dataflow model and demonstrate the compelling performance that Tensor- Flow achieves for several real-world applications. View details
    Deep Learning with Differential Privacy
    Andy Chu
    Ian Goodfellow
    Ilya Mironov
    Kunal Talwar
    Li Zhang
    23rd ACM Conference on Computer and Communications Security (ACM CCS) (2016), pp. 308-318
    Preview abstract Machine learning techniques based on neural networks are achieving remarkable results in a wide variety of domains. Often, the training of models requires large, representative datasets, which may be crowdsourced and contain sensitive information. The models should not expose private information in these datasets. Addressing this goal, we develop new algorithmic techniques for learning and a refined analysis of privacy costs within the framework of differential privacy. Our implementation and experiments demonstrate that we can train deep neural networks with non-convex objectives, under a modest privacy budget, and at a manageable cost in software complexity, training efficiency, and model quality. View details
    Preview abstract TensorFlow is a machine learning system that operates at large scale and in heterogeneous environments. Its computational model is based on dataflow graphs with mutable state. Graph nodes may be mapped to different machines in a cluster, and within each machine to CPUs, GPUs, and other devices. TensorFlow supports a variety of applications, but it particularly targets training and inference with deep neural networks. It serves as a platform for research and for deploying machine learning systems across many areas, such as speech recognition, computer vision, robotics, information retrieval, and natural language processing. In this talk, we describe TensorFlow and outline some of its applications. We also discuss the question of what TensorFlow and deep learning may have to do with functional programming. Although TensorFlow is not purely functional, many of its uses are concerned with optimizing functions (during training), then with applying those functions (during inference). These functions are defined as compositions of simple primitives (as is common in functional programming), with internal data representations that are learned rather than manually designed. TensorFlow is joint work with many other people in the Google Brain team and elsewhere. More information is available at tensorflow.org. View details
    Preview abstract We describe the timely dataflow model for distributed computation and its implementation in the Naiad system. The model supports stateful iterative and incremental computations. It enables both low-latency stream processing and high-throughput batch processing, using a new approach to coordination that combines asynchronous and fine-grained synchronous execution. We describe two of the programming frameworks built on Naiad: GraphLINQ for parallel graph processing, and differential dataflow for nested iterative and incremental computations. We show that a general-purpose system can achieve performance that matches, and sometimes exceeds, that of specialized systems. View details
    Distributed Authorization With Distributed Grammars
    Mike Burrows
    Himabindu Pucha
    Adam Sadovsky
    Asim Shankar
    Ankur Taly
    Programming Languages with Applications to Biology and Security, Springer International Publishing Switzerland, Gewerbestrasse 11 CH-6330 Cham (ZG) Switzerland (2015), pp. 10-26
    Preview abstract While groups are generally helpful for the definition of authorization policies, their use in distributed systems is not straightforward. This paper describes a design for authorization in distributed systems that treats groups as formal languages. The design supports forms of delegation and negative clauses in authorization policies. It also considers the wish for privacy and efficiency in group-membership checks, and the possibility that group definitions may not all be available and may contain cycles. View details
    Preview abstract This paper studies timely dataflow, a model for data-parallel computing in which each communication event is associated with a virtual time. It defines and investigates the could-result-in relation which is central to this model, then the semantics of timely dataflow graphs. View details
    TensorFlow: Large-Scale Machine Learning on Heterogeneous Distributed Systems
    Ashish Agarwal
    Eugene Brevdo
    Craig Citro
    Matthieu Devin
    Ian Goodfellow
    Andrew Harp
    Geoffrey Irving
    Yangqing Jia
    Rafal Jozefowicz
    Lukasz Kaiser
    Manjunath Kudlur
    Dan Mané
    Rajat Monga
    Chris Olah
    Mike Schuster
    Jonathon Shlens
    Benoit Steiner
    Ilya Sutskever
    Kunal Talwar
    Paul Tucker
    Vijay Vasudevan
    Pete Warden
    Yuan Yu
    Xiaoqiang Zheng
    tensorflow.org (2015)
    Preview abstract TensorFlow is an interface for expressing machine learning algorithms, and an implementation for executing such algorithms. A computation expressed using TensorFlow can be executed with little or no change on a wide variety of heterogeneous systems, ranging from mobile devices such as phones and tablets up to large-scale distributed systems of hundreds of machines and thousands of computational devices such as GPU cards. The system is flexible and can be used to express a wide variety of algorithms, including training and inference algorithms for deep neural network models, and it has been used for conducting research and for deploying machine learning systems into production across more than a dozen areas of computer science and other fields, including speech recognition, computer vision, robotics, information retrieval, natural language processing, geographic information extraction, and computational drug discovery. This paper describes the TensorFlow interface and an implementation of that interface that we have built at Google. The TensorFlow API and a reference implementation were released as an open-source package under the Apache 2.0 license in November, 2015 and are available at www.tensorflow.org. View details
    Timely Rollback: Specification and Verification
    NFM (2015), pp. 19-34
    The Prophecy of Undo
    FASE (2015), pp. 347-361
    On the Flow of Data, Information, and Time
    POST (2015), pp. 73-92
    Foundations of Differential Dataflow
    Frank McSherry
    Gordon D. Plotkin
    FoSSaCS (2015), pp. 71-83
    Web PKI: Closing the Gap between Guidelines and Practices
    Antoine Delignat-Lavaud
    Andrew Birrell
    Ilya Mironov
    Ted Wobber
    Yinglian Xie
    Microsoft Research
    NDSS (2014)
    Understanding Typescript
    Gavin M. Bierman
    Mads Torgersen
    ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, pp. 257-281
    On Layout Randomization for Arrays and Functions
    Jérémy Planul
    POST (2013), pp. 167-185
    Global Authentication in an Untrustworthy World
    Andrew Birrell
    Ilya Mironov
    Ted Wobber
    Yinglian Xie
    HotOS (2013)
    SocialWatch: detection of online service abuse via large-scale social graphs
    Junxian Huang
    Yinglian Xie
    Fang Yu
    Qifa Ke
    Eliot Gillum
    Zhuoqing Morley Mao
    ASIACCS (2013), pp. 143-148
    Layout Randomization and Nondeterminism
    Jérémy Planul
    Gordon D. Plotkin
    Electr. Notes Theor. Comput. Sci., vol. 298 (2013), pp. 29-50
    Formal Analysis of a Distributed Algorithm for Tracking Progress
    Frank McSherry
    Derek Gordon Murray
    Thomas L. Rodeheffer
    FMOODS/FORTE (2013), pp. 5-19
    Early security classification of skype users via machine learning
    Anna Leontjeva
    Moisés Goldszmidt
    Yinglian Xie
    Fang Yu
    AISec (2013), pp. 35-44
    Naiad: a timely dataflow system
    Frank McSherry
    Rebecca Isaacs
    SOSP (2013), pp. 439-455
    Message-Locked Encryption for Lock-Dependent Messages
    Dan Boneh
    Ilya Mironov
    Ananth Raghunathan
    Gil Segev
    CRYPTO (1) (2013), pp. 374-391
    Host Fingerprinting and Tracking on the Web: Privacy and Security Implications
    Ting-Fang Yen
    Yinglian Xie
    Fang Yu
    Roger Peng Yu
    NDSS (2012)
    A Functional View of Imperative Information Flow
    Thomas H. Austin
    Cormac Flanagan
    APLAS (2012), pp. 34-49
    On Protection by Layout Randomization
    Gordon D. Plotkin
    ACM Trans. Inf. Syst. Secur., vol. 15 (2012), pp. 8
    Software Security: A Formal Perspective - (Notes for a Talk)
    FM (2012), pp. 1-5
    Innocent by association: early recognition of legitimate users
    Yinglian Xie
    Fang Yu
    Qifa Ke
    Eliot Gillum
    Krish Vitaldevaria
    Jason Walter
    Junxian Huang
    Zhuoqing Morley Mao
    ACM Conference on Computer and Communications Security (2012), pp. 353-364
    Semantics of transactional memory and automatic mutual exclusion
    Andrew Birrell
    Tim Harris 0001
    ACM Trans. Program. Lang. Syst., vol. 33 (2011), pp. 2
    Differential privacy with information flow control
    Frank McSherry
    PLAS (2011), pp. 2
    deSEO: Combating Search-Result Poisoning
    John P. John
    Fang Yu
    Yinglian Xie
    Arvind Krishnamurthy
    USENIX Security Symposium (2011)
    AC: composable asynchronous IO for native languages
    Tim Harris 0001
    Rebecca Isaacs
    OOPSLA (2011), pp. 903-920
    Heat-seeking honeypots: design and experience
    John P. John
    Fang Yu
    Yinglian Xie
    Arvind Krishnamurthy
    WWW (2011), pp. 207-216
    A Model of Cooperative Threads
    Gordon D. Plotkin
    Logical Methods in Computer Science, vol. 6 (2010)
    A model of dynamic separation for transactional memory
    Tim Harris 0001
    Katherine F. Moore
    Inf. Comput., vol. 208 (2010), pp. 1093-1117
    On Protection by Layout Randomization
    Gordon D. Plotkin
    CSF (2010), pp. 337-351
    How to tell an airport from a home: techniques and applications
    Andreas Pitsillidis
    Yinglian Xie
    Fang Yu
    Geoffrey M. Voelker
    Stefan Savage
    HotNets (2010), pp. 13
    The Fine Print of Security
    LICS (2010), pp. 110
    Searching the Searchers with SearchAudit
    John P. John
    Fang Yu
    Yinglian Xie
    Arvind Krishnamurthy
    USENIX Security Symposium (2010), pp. 127-142
    Guessing attacks and the computational soundness of static equivalence
    Mathieu Baudet
    Bogdan Warinschi
    Journal of Computer Security, vol. 18 (2010), pp. 909-968
    Logic in Access Control (Tutorial Notes)
    FOSAD (2009), pp. 145-165
    Perspectives on Transactional Memory
    Tim Harris 0001
    CONCUR (2009), pp. 1-14
    Unified Declarative Platform for Secure Netwoked Information Systems
    Wenchao Zhou
    Yun Mao
    Boon Thau Loo
    ICDE (2009), pp. 150-161
    A model of cooperative threads
    Gordon D. Plotkin
    POPL (2009), pp. 29-40
    Implementation and Use of Transactional Memory with Dynamic Separation
    Andrew Birrell
    Tim Harris 0001
    Johnson Hsieh
    CC (2009), pp. 63-77
    De-anonymizing the internet using unreliable IDs
    Yinglian Xie
    Fang Yu
    SIGCOMM (2009), pp. 75-86
    Control-flow integrity principles, implementations, and applications
    Mihai Budiu
    Úlfar Erlingsson
    Jay Ligatti
    ACM Trans. Inf. Syst. Secur., vol. 13 (2009)
    Transactional memory with strong atomicity using off-the-shelf memory protection hardware
    Tim Harris 0001
    Mojtaba Mehrara
    PPOPP (2009), pp. 185-196
    Models and Proofs of Protocol Security: A Progress Report
    Bruno Blanchet
    Hubert Comon-Lundh
    CAV (2009), pp. 35-49
    Code-Carrying Authorization
    Sergio Maffeis
    Cédric Fournet
    Andrew D. Gordon
    ESORICS (2008), pp. 563-579
    Variations in Access Control Logic
    DEON (2008), pp. 96-109
    Semantics of transactional memory and automatic mutual exclusion
    Andrew Birrell
    Tim Harris 0001
    POPL (2008), pp. 63-74
    A Modal Deconstruction of Access Control Logics
    Deepak Garg 0001
    FoSSaCS (2008), pp. 216-230
    A Model of Dynamic Separation for Transactional Memory
    Tim Harris 0001
    Katherine F. Moore
    CONCUR (2008), pp. 6-20
    Security analysis of cryptographically controlled access to XML documents
    Bogdan Warinschi
    J. ACM, vol. 55 (2008)
    The good, the bad, and the provable
    ACM Conference on Computer and Communications Security (2008), pp. 1
    Automatic Mutual Exclusion and Atomicity Checks
    Concurrency, Graphs and Models (2008), pp. 510-526
    Automated verification of selected equivalences for security protocols
    Bruno Blanchet
    Cédric Fournet
    J. Log. Algebr. Program., vol. 75 (2008), pp. 3-51
    Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
    Phillip Rogaway
    J. Cryptology, vol. 20 (2007), pp. 395
    Just fast keying in the pi calculus
    Bruno Blanchet
    Cédric Fournet
    ACM Trans. Inf. Syst. Secur., vol. 10 (2007)
    Policies and Proofs for Code Auditing
    Nathan Whitehead
    Jordan Johnson
    ATVA (2007), pp. 1-14
    Editorial
    Jens Palsberg
    ACM Trans. Program. Lang. Syst., vol. 29 (2007)
    Security Protocols: Principles and Calculi
    FOSAD (2007), pp. 1-23
    Towards a Declarative Language and System for Secure Networking
    Boon Thau Loo
    NetDB (2007)
    Authorizing applications in singularity
    Ted Wobber
    Aydan R. Yumerefendi
    Andrew Birrell
    Daniel R. Simon
    EuroSys (2007), pp. 355-368
    Access Control in a Core Calculus of Dependency
    Electr. Notes Theor. Comput. Sci., vol. 172 (2007), pp. 5-31
    Guessing Attacks and the Computational Soundness of Static Equivalence
    Mathieu Baudet
    Bogdan Warinschi
    FoSSaCS (2006), pp. 398-412
    Access control in a core calculus of dependency
    ICFP (2006), pp. 263-273
    Formal Analysis of Dynamic, Distributed File-System Access Controls
    Avik Chaudhuri
    FORTE (2006), pp. 99-114
    Computational Secrecy by Typing for the Pi Calculus
    Ricardo Corin
    Cédric Fournet
    APLAS (2006), pp. 253-269
    Secrecy by Typing and File-Access Control
    Avik Chaudhuri
    CSFW (2006), pp. 112-123
    Types for safe locking: Static race detection for Java
    Cormac Flanagan
    Stephen N. Freund
    ACM Trans. Program. Lang. Syst., vol. 28 (2006), pp. 207-255
    Deciding knowledge in security protocols under equational theories
    Véronique Cortier
    Theor. Comput. Sci., vol. 367 (2006), pp. 2-32
    Architectural support for software-based protection
    Mihai Budiu
    Úlfar Erlingsson
    ASID (2006), pp. 42-51
    XFI: Software Guards for System Address Spaces
    Úlfar Erlingsson
    Mihai Budiu
    George C. Necula
    OSDI (2006), pp. 75-88
    Computer-assisted verification of a protocol for certified email
    Bruno Blanchet
    Sci. Comput. Program., vol. 58 (2005), pp. 3-27
    Analyzing security protocols with secrecy types and logic programs
    Bruno Blanchet
    J. ACM, vol. 52 (2005), pp. 102-146
    Automated Verification of Selected Equivalences for Security Protocols
    Bruno Blanchet
    Cédric Fournet
    LICS (2005), pp. 331-340
    "Language-Based Security"
    Greg Morrisett
    Andrei Sabelfeld
    J. Funct. Program., vol. 15 (2005), pp. 129
    Access Control in a World of Software Diversity
    Andrew Birrell
    Ted Wobber
    HotOS (2005)
    Control-flow integrity
    Mihai Budiu
    Úlfar Erlingsson
    Jay Ligatti
    ACM Conference on Computer and Communications Security (2005), pp. 340-353
    Security analysis of cryptographically controlled access to XML documents
    Bogdan Warinschi
    PODS (2005), pp. 108-117
    A Theory of Secure Control Flow
    Mihai Budiu
    Úlfar Erlingsson
    Jay Ligatti
    ICFEM (2005), pp. 111-124
    Deciding Knowledge in Security Protocols under (Many More) Equational Theories
    Véronique Cortier
    CSFW (2005), pp. 62-76
    Moderately hard, memory-bound functions
    Michael M. Burrows
    Mark Manasse
    Ted Wobber
    ACM Transactions on Internet Technology, vol. 5 (2005), pp. 299-327
    Formal security analysis of basic network-attached storage
    Avik Chaudhuri
    FMSE (2005), pp. 43-52
    Password-Based Encryption Analyzed
    Bogdan Warinschi
    ICALP (2005), pp. 664-676
    A Logical Account of NGSCB
    Ted Wobber
    FORTE (2004), pp. 1-12
    Deciding Knowledge in Security Protocols Under Equational Theories
    Véronique Cortier
    ICALP (2004), pp. 46-58
    Just Fast Keying in the Pi Calculus
    Bruno Blanchet
    Cédric Fournet
    ESOP (2004), pp. 340-354
    Trusted Computing, Trusted Third Parties, and Verified Communications
    SEC (2004), pp. 291-308
    Language-Based Enforcement of Privacy Policies
    Katia Hayati
    Privacy Enhancing Technologies (2004), pp. 302-313
    Private authentication
    Cédric Fournet
    Theor. Comput. Sci., vol. 322 (2004), pp. 427-476
    BCiC: A System for Code Authentication and Verification
    Nathan Whitehead
    LPAR (2004), pp. 110-124
    Choice in Dynamic Linking
    Georges Gonthier
    Benjamin Werner
    FoSSaCS (2004), pp. 12-26
    By Reason and Authority: A System for Authorization of Proof-Carrying Code
    Nathan Whitehead
    George C. Necula
    CSFW (2004), pp. 236-250
    Access Control Based on Execution History
    Cédric Fournet
    NDSS (2003)
    Reasoning About Secrecy for Active Networks
    Pankaj Kakkar
    Carl A. Gunter
    Journal of Computer Security, vol. 11 (2003), pp. 245-287
    Bankable Postage for Network Services
    Andrew Birrell
    Michael Burrows
    Ted Wobber
    ASIAN (2003), pp. 72-90
    Computer-Assisted Verification of a Protocol for Certified Email
    Bruno Blanchet
    SAS (2003), pp. 316-335
    Logic in Access Control
    LICS (2003), pp. 228-
    Secrecy types for asymmetric communication
    Bruno Blanchet
    Theor. Comput. Sci., vol. 3 (2003), pp. 387-415
    A Logic of Object-Oriented Programs
    K. Rustan M. Leino
    Verification: Theory and Practice (2003), pp. 11-41
    Built-in Object Security
    ECOOP (2003), pp. 1
    Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
    Phillip Rogaway
    J. Cryptology, vol. 15 (2002), pp. 103-127
    Private Authentication
    Privacy Enhancing Technologies (2002), pp. 27-40
    Certified email with a light on-line trusted third party: design and implementation
    Neal Glew
    WWW (2002), pp. 387-395
    Analyzing security protocols with secrecy types and logic programs
    Bruno Blanchet
    POPL (2002), pp. 33-44
    Secure Implementation of Channel Abstractions
    Cédric Fournet
    Georges Gonthier
    Inf. Comput., vol. 174 (2002), pp. 37-83
    Editorial
    Leonid Libkin
    Frank Pfenning
    ACM Trans. Comput. Log., vol. 3 (2002), pp. 335-335
    Hiding Names: Private Authentication in the Applied Pi Calculus
    Cédric Fournet
    ISSS (2002), pp. 317-338
    Formal Eavesdropping and Its Computational Interpretation
    Jan Jürjens
    TACS (2001), pp. 82-94
    Secrecy Types for Asymmetric Communication
    Bruno Blanchet
    FoSSaCS (2001), pp. 25-41
    Mobile values, new names, and secure communication
    Cédric Fournet
    POPL (2001), pp. 104-115
    Computing Symbolic Models for Verifying Cryptographic Protocols
    Marcelo P. Fiore
    CSFW (2001), pp. 160-173
    Leslie Lamport's properties and actions
    PODC (2001), pp. 15
    Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
    Phillip Rogaway
    IFIP TCS (2000), pp. 3-22
    Taming the Adversary
    CRYPTO (2000), pp. 353-358
    Authentication Primitives and Their Compilation
    Cédric Fournet
    Georges Gonthier
    POPL (2000), pp. 302-315
    top-top-closed relations and admissibility
    Mathematical Structures in Computer Science, vol. 10 (2000), pp. 313-320
    Reasoning about Secrecy for Active Networks
    Pankaj Kakkar
    Carl A. Gunter
    CSFW (2000), pp. 118-129
    Protection in Programming-Language Translations
    Secure Internet Programming (1999), pp. 19-34
    A Core Calculus of Dependency
    Anindya Banerjee
    Jon G. Riecke
    POPL (1999), pp. 147-160
    Types for Safe Locking
    Cormac Flanagan
    ESOP (1999), pp. 91-108
    Security Protocols and Specifications
    FoSSaCS (1999), pp. 1-13
    Secrecy in Programming-Language Semantics
    Electr. Notes Theor. Comput. Sci., vol. 20 (1999), pp. 80-94
    A Top-Down Look at a Secure Message
    Cédric Fournet
    Georges Gonthier
    FSTTCS (1999), pp. 122-141
    Secure Network Objects
    Leendert van Doorn
    Michael Burrows
    Edward Wobber
    Secure Internet Programming (1999), pp. 395-412
    A Calculus for Cryptographic Protocols: The spi Calculus
    Andrew D. Gordon
    Inf. Comput., vol. 148 (1999), pp. 1-70
    Secure Communications Processing for Distributed Languages
    Cédric Fournet
    Georges Gonthier
    IEEE Symposium on Security and Privacy (1999), pp. 74-88
    A Type System for Java Bytecode Subroutines
    Raymie Stata
    ACM Trans. Program. Lang. Syst., vol. 21 (1999), pp. 90-137
    Object Types against Races
    Cormac Flanagan
    CONCUR (1999), pp. 288-303
    Panel Introduction: Varieties of Authentication
    Roberto Gorrieri
    Paul F. Syverson
    Riccardo Focardi
    Dieter Gollmann
    Gavin Lowe
    Catherine Meadows
    CSFW (1998), pp. 79-82
    Protection in Programming-Language Translations: Mobile Object Systems (Abstract)
    ECOOP Workshops (1998), pp. 291
    A Type System for Java Bytecode Subroutines
    Raymie Stata
    POPL (1998), pp. 149-160
    Secure Implementation of Channel Abstractions
    Cédric Fournet
    Georges Gonthier
    LICS (1998), pp. 105-116
    Secure Web Tunneling
    Andrew Birrell
    Raymie Stata
    Edward Wobber
    Computer Networks, vol. 30 (1998), pp. 531-539
    Protection in Programming-Language Translations
    ICALP (1998), pp. 868-883
    A Bisimulation Method for Cryptographic Protocols
    Andrew D. Gordon
    ESOP (1998), pp. 12-26
    A Bisimulation Method for Cryptographic Protocols
    Andrew D. Gordon
    Nord. J. Comput., vol. 5 (1998), pp. 267-
    On SDSI's Linked Local Name Spaces
    Journal of Computer Security, vol. 6 (1998), pp. 3-22
    Two Facets of Authentication
    CSFW (1998), pp. 27-32
    Explicit Communication Revisited: Two New Attacks on Authentication Protocols
    IEEE Trans. Software Eng., vol. 23 (1997), pp. 185-186
    A Calculus for Cryptographic Protocols: The Spi Calculus
    Andrew D. Gordon
    ACM Conference on Computer and Communications Security (1997), pp. 36-47
    Reasoning about Cryptographic Protocols in the Spi Calculus
    Andrew D. Gordon
    CONCUR (1997), pp. 59-73
    Secrecy by Typing inSecurity Protocols
    TACS (1997), pp. 611-638
    A Logic of Object-Oriented Programs
    K. Rustan M. Leino
    TAPSOFT (1997), pp. 682-696
    On SDSI's Linked Local Name Spaces
    CSFW (1997), pp. 98-108
    Secure Implementation of Channel Abstractions
    Cédric Fournet
    Georges Gonthier
    Electr. Notes Theor. Comput. Sci., vol. 10 (1997), pp. 202-203
    On TLA as a logic
    Stephan Merz
    NATO ASI DPD (1996), pp. 235-271
    Analysis and Caching of Dependencies
    Butler W. Lampson
    Jean-Jacques Lévy
    ICFP (1996), pp. 83-91
    On Subtyping and Matching
    Luca Cardelli
    ACM Trans. Program. Lang. Syst., vol. 18 (1996), pp. 401-423
    A Theory of Objects
    Luca Cardelli
    Springer (1996), I-XIII, 1-396
    Secure Network Objects
    Leendert van Doorn
    Michael Burrows
    Edward Wobber
    IEEE Symposium on Security and Privacy (1996), pp. 211-221
    Prudent Engineering Practice for Cryptographic Protocols
    Roger M. Needham
    IEEE Trans. Software Eng., vol. 22 (1996), pp. 6-15
    Syntactic Considerations on Recursive Types
    Marcelo P. Fiore
    LICS (1996), pp. 242-252
    A Theory of Primitive Objects: Untyped and First-Order Systems
    Luca Cardelli
    Inf. Comput., vol. 125 (1996), pp. 78-102
    An Interpretation of Objects and Object Types
    Luca Cardelli
    Ramesh Viswanathan
    POPL (1996), pp. 396-409
    On Subtyping and Matching
    Luca Cardelli
    ECOOP (1995), pp. 145-167
    An Abstract Account of Composition
    Stephan Merz
    MFCS (1995), pp. 499-508
    A Model for Formal Parametric Polymorphism: A PER Interpretation for System R
    Roberto Bellucci
    Pierre-Louis Curien
    TLCA (1995), pp. 32-46
    Conjoining Specifications
    Leslie Lamport
    ACM Trans. Program. Lang. Syst., vol. 17 (1995), pp. 507-534
    An Imperative Object Calculus (Invited Paper)
    Luca Cardelli
    TAPOS, vol. 1 (1995), pp. 151-166
    Methods as Assertions
    John Lamping
    TAPOS, vol. 1 (1995), pp. 5-18
    Dynamic Typing in Polymorphic Languages
    Luca Cardelli
    Benjamin C. Pierce
    Didier Rémy
    J. Funct. Program., vol. 5 (1995), pp. 111-130
    An Imperative Object Calculus
    Luca Cardelli
    TAPSOFT (1995), pp. 471-485
    A Theory of Primitive Objects: Second-Order Systems
    Luca Cardelli
    Sci. Comput. Program., vol. 25 (1995), pp. 81-116
    A Theory of Primitive Objects - Untyped and First-Order Systems
    Luca Cardelli
    TACS (1994), pp. 296-320
    Prudent engineering practice for cryptographic protocols
    Roger M. Needham
    IEEE Symposium on Security and Privacy (1994), pp. 122-136
    Decidability and Expressiveness for First-Order Logics of Probability
    Joseph Y. Halpern
    Inf. Comput., vol. 112 (1994), pp. 1-36
    A Semantics for Static Type Inference in a Nondeterministic Language
    Inf. Comput., vol. 109 (1994), pp. 300-306
    A Theory of Primitive Objects - Scond-Order Systems
    Luca Cardelli
    ESOP (1994), pp. 1-25
    An Old-Fashined Recipe for Real-Time
    Leslie Lamport
    ACM Trans. Program. Lang. Syst., vol. 16 (1994), pp. 1543-1571
    Authentication in the Taos Operating System
    Edward Wobber
    Michael Burrows
    ACM Trans. Comput. Syst., vol. 12 (1994), pp. 3-32
    Baby Modula-3 and a Theory of Objects
    J. Funct. Program., vol. 4 (1994), pp. 249-283
    Methods as Assertions
    John Lamping
    ECOOP (1994), pp. 60-80
    Open Systems in TLA
    Leslie Lamport
    PODC (1994), pp. 81-90
    A TLA Solution to the RPC-Memory Specification Problem
    Leslie Lamport
    Stephan Merz
    Formal Systems Specification (1994), pp. 21-66
    Subtyping and Parametricity
    Gordon D. Plotkin
    Luca Cardelli
    LICS (1994), pp. 310-319
    A Semantics of Object Types
    Luca Cardelli
    LICS (1994), pp. 332-341
    Decomposing Specifications of Concurrent Systems
    Leslie Lamport
    PROCOMET (1994), pp. 327-340
    A Logic for Parametric Polymorphism
    Gordon D. Plotkin
    TLCA (1993), pp. 361-375
    Authentification and Delegation with Smart-Cards
    Michael Burrows
    C. Kaufman
    Butler W. Lampson
    Sci. Comput. Program., vol. 21 (1993), pp. 93-113
    A Logical View of Composition
    Gordon D. Plotkin
    Theor. Comput. Sci., vol. 114 (1993), pp. 3-30
    A Calculus for Access Control in Distributed Systems
    Michael Burrows
    Butler W. Lampson
    Gordon D. Plotkin
    ACM Trans. Program. Lang. Syst., vol. 15 (1993), pp. 706-734
    Formal Parametric Polymorphism
    Luca Cardelli
    Pierre-Louis Curien
    Theor. Comput. Sci., vol. 121 (1993), pp. 9-58
    Formal Parametric Polymorphism
    Luca Cardelli
    Pierre-Louis Curien
    POPL (1993), pp. 157-170
    Composing Specifications
    Leslie Lamport
    ACM Trans. Program. Lang. Syst., vol. 15 (1993), pp. 73-132
    Extensible Grammars for Language Specialization
    Luca Cardelli
    Florian Matthes
    DBPL (1993), pp. 11-31
    Authentication in the Taos Operating System
    Edward Wobber
    Michael Burrows
    Butler W. Lampson
    SOSP (1993), pp. 256-269
    Authentication in Distributed Systems: Theory and Practice
    Butler W. Lampson
    Michael Burrows
    Edward Wobber
    ACM Trans. Comput. Syst., vol. 10 (1992), pp. 265-310
    Linear Logic Without Boxes
    Georges Gonthier
    Jean-Jacques Lévy
    LICS (1992), pp. 223-234
    The Geometry of Optimal Lambda Reduction
    Georges Gonthier
    Jean-Jacques Lévy
    POPL (1992), pp. 15-26
    Preserving Liveness: Comments on ``Safety and Liveness from a Methodological Point of View''
    Bowen Alpern
    Krzysztof R. Apt
    Nissim Francez
    Shmuel Katz
    Leslie Lamport
    Fred B. Schneider
    Inf. Process. Lett., vol. 40 (1991), pp. 141-142
    The Existence of Refinement Mappings
    Leslie Lamport
    Theor. Comput. Sci., vol. 82 (1991), pp. 253-284
    Authentication in Distributed Systems: Theory and Practice
    Butler W. Lampson
    Michael Burrows
    Edward Wobber
    SOSP (1991), pp. 165-182
    Faithful Ideal Models for Recursive Polymorphic Types
    Benjamin C. Pierce
    Gordon D. Plotkin
    Int. J. Found. Comput. Sci., vol. 2 (1991), pp. 1-21
    Dynamic Typing in a Statically Typed Language
    Luca Cardelli
    Benjamin C. Pierce
    Gordon D. Plotkin
    ACM Trans. Program. Lang. Syst., vol. 13 (1991), pp. 237-268
    A Calculus for Access Control in Distributed Systems
    Michael Burrows
    Butler W. Lampson
    Gordon D. Plotkin
    CRYPTO (1991), pp. 1-23
    Authentication and Delegation with Smart-cards
    Michael Burrows
    C. Kaufman
    Butler W. Lampson
    TACS (1991), pp. 326-345
    A Semantics for a Logic of Authentication (Extended Abstract)
    Mark R. Tuttle
    PODC (1991), pp. 201-216
    An Old-Fashioned Recipe for Real Time
    Leslie Lamport
    REX Workshop (1991), pp. 1-27
    Explicit Substitutions
    Luca Cardelli
    Pierre-Louis Curien
    Jean-Jacques Lévy
    J. Funct. Program., vol. 1 (1991), pp. 375-416
    A Logical View of Composition and Refinement
    Gordon D. Plotkin
    POPL (1991), pp. 323-332
    An Axiomatization of Lamport's Temporal Logic of Actions
    CONCUR (1990), pp. 57-69
    Corrigendum: The Power of Temporal Proofs
    Theor. Comput. Sci., vol. 70 (1990), pp. 275
    Nonclausal Deduction in First-Order Temporal Logic
    Zohar Manna
    J. ACM, vol. 37 (1990), pp. 279-317
    A Per Model of Polymorphism and Recursive Types
    Gordon D. Plotkin
    LICS (1990), pp. 355-365
    Rejoinder to Nessett
    Michael Burrows
    Roger M. Needham
    Operating Systems Review, vol. 24 (1990), pp. 39-40
    Secure Circuit Evaluation
    Joan Feigenbaum
    J. Cryptology, vol. 2 (1990), pp. 1-12
    A Logic of Authentication
    Michael Burrows
    Roger M. Needham
    ACM Trans. Comput. Syst., vol. 8 (1990), pp. 18-36
    Explicit Substitutions
    Luca Cardelli
    Pierre-Louis Curien
    Jean-Jacques Lévy
    POPL (1990), pp. 31-46
    Faithful Ideal Models for Recursive Polymorphic Types
    Benjamin C. Pierce
    Gordon D. Plotkin
    LICS (1989), pp. 216-225
    Decidability and Expressiveness for First-Order Logics of Probability (Extended Abstract)
    Joseph Y. Halpern
    FOCS (1989), pp. 148-153
    On Hiding Information from an Oracle
    Joan Feigenbaum
    Joe Kilian
    J. Comput. Syst. Sci., vol. 39 (1989), pp. 21-50
    Dynamic Typing in a Statically-Typed Language
    Luca Cardelli
    Benjamin C. Pierce
    Gordon D. Plotkin
    POPL (1989), pp. 213-227
    Temporal Logic Programming
    Zohar Manna
    J. Symb. Comput., vol. 8 (1989), pp. 277-295
    A Logic of Authentication
    Michael Burrows
    Roger M. Needham
    SOSP (1989), pp. 1-13
    Composing Specifications
    Leslie Lamport
    REX Workshop (1989), pp. 1-41
    Realizable and Unrealizable Specifications of Reactive Systems
    Leslie Lamport
    Pierre Wolper
    ICALP (1989), pp. 1-17
    The Power of Temporal Proofs
    Theor. Comput. Sci., vol. 65 (1989), pp. 35-83
    A Simple Protocol for Secure Circuit Evaluation
    Joan Feigenbaum
    STACS (1988), pp. 264-272
    The Existence of Refinement Mappings
    Leslie Lamport
    LICS (1988), pp. 165-175
    On Generating Solved Instances of Computational Problems
    Eric Allender
    Joan Feigenbaum
    Lane A. Hemachandra
    CRYPTO (1988), pp. 297-310
    Authentication: A Practical Study in Belief and Action
    Michael Burrows
    Roger M. Needham
    TARK (1988), pp. 325-342
    On hiding information from an oracle
    Joan Feigenbaum
    Joe Kilian
    Structure in Complexity Theory Conference (1987)
    Temporal Logic Programming
    Zohar Manna
    SLP (1987), pp. 4-16
    On Hiding Information from an Oracle (Extended Abstract)
    Joan Feigenbaum
    Joe Kilian
    STOC (1987), pp. 195-203
    The Power of Temporal Proofs
    LICS (1987), pp. 123-130
    A Timely Resolution
    Zohar Manna
    LICS (1986), pp. 176-186
    Modal Theorem Proving
    Zohar Manna
    CADE (1986), pp. 172-189
    Nonclausal Temporal Deduction
    Zohar Manna
    Logic of Programs (1985), pp. 1-15