publications: - title: "Verified interoperable implementations of security protocols" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Stephen Tse" link: "https://researchr.org/alias/stephen-tse" year: "2008" doi: "http://doi.acm.org/10.1145/1452044.1452049" links: doi: "http://doi.acm.org/10.1145/1452044.1452049" tags: - "protocol" - "security" researchr: "https://researchr.org/publication/BhargavanFGT08" cites: 0 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "31" number: "1" kind: "article" key: "BhargavanFGT08" - title: "TulaFale: A Security Tool for Web Services" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Riccardo Pucella" link: "https://researchr.org/alias/riccardo-pucella" year: "2003" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3188&spage=197" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3188&spage=197" tags: - "web service" - "security" - "web services" researchr: "https://researchr.org/publication/BhargavanFGP03" cites: 0 citedby: 0 pages: "197-222" booktitle: "Formal Methods for Components and Objects, Second International Symposium, FMCO 2003, Leiden, The Netherlands, November 4-7, 2003, Revised Lectures" editor: - name: "Frank S. de Boer" link: "https://researchr.org/alias/frank-s.-de-boer" - name: "Marcello M. Bonsangue" link: "https://researchr.org/alias/marcello-m.-bonsangue" - name: "Susanne Graf" link: "https://researchr.org/alias/susanne-graf" - name: "Willem P. de Roever" link: "https://researchr.org/alias/willem-p.-de-roever" volume: "3188" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-22942-6" kind: "inproceedings" key: "BhargavanFGP03" - title: "Verified Interoperable Implementations of Security Protocols" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Stephen Tse" link: "https://researchr.org/alias/stephen-tse" year: "2006" doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.32" links: doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.32" tags: - "protocol" - "security" researchr: "https://researchr.org/publication/BhargavanFGT06" cites: 0 citedby: 0 pages: "139-152" booktitle: "19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006), 5-7 July 2006, Venice, Italy" publisher: "IEEE Computer Society" isbn: "0-7695-2615-2" kind: "inproceedings" key: "BhargavanFGT06" - title: "Ambient Groups and Mobility Types" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Giorgio Ghelli" link: "https://researchr.org/alias/giorgio-ghelli" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2000" doi: "http://link.springer.de/link/service/series/0558/bibs/1872/18720333.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1872/18720333.htm" researchr: "https://researchr.org/publication/CardelliGG00%3A1" cites: 0 citedby: 0 pages: "333-347" booktitle: "Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, International Conference IFIP TCS 2000, Sendai, Japan, August 17-19, 2000, Proceedings" editor: - name: "Jan van Leeuwen" link: "https://researchr.org/alias/jan-van-leeuwen" - name: "Osamu Watanabe" link: "https://researchr.org/alias/osamu-watanabe" - name: "Masami Hagiya" link: "https://researchr.org/alias/masami-hagiya" - name: "Peter D. Mosses" link: "https://pdmosses.github.io" - name: "Takayasu Ito" link: "https://researchr.org/alias/takayasu-ito" volume: "1872" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-67823-9" kind: "inproceedings" key: "CardelliGG00:1" - title: "A compositional theory for STM Haskell" author: - name: "Johannes Borgström" link: "https://researchr.org/alias/johannes-borgstr%C3%A3%C2%B6m" - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2009" doi: "http://doi.acm.org/10.1145/1596638.1596648" links: doi: "http://doi.acm.org/10.1145/1596638.1596648" tags: - "composition" - "Haskell" researchr: "https://researchr.org/publication/BorgstromBG09" cites: 0 citedby: 0 pages: "69-80" booktitle: "Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, Haskell 2009, Edinburgh, Scotland, UK, 3 September 2009" editor: - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-60558-508-6" kind: "inproceedings" key: "BorgstromBG09" - title: "A Type Discipline for Authorization Policies" author: - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Sergio Maffeis" link: "https://researchr.org/alias/sergio-maffeis" year: "2005" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3444&spage=141" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3444&spage=141" researchr: "https://researchr.org/publication/FournetGM05" cites: 0 citedby: 0 pages: "141-156" booktitle: "Programming Languages and Systems, 14th European Symposium on Programming,ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings" editor: - name: "Shmuel Sagiv" link: "https://researchr.org/alias/shmuel-sagiv" volume: "3444" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-25435-8" kind: "inproceedings" key: "FournetGM05" - title: "Types for Cryptographic Protocols" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2002" doi: "http://link.springer.de/link/service/series/0558/bibs/2421/24210099.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2421/24210099.htm" tags: - "protocol" researchr: "https://researchr.org/publication/Gordon02%3A3" cites: 0 citedby: 0 pages: "99-100" booktitle: "CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings" editor: - name: "Lubos Brim" link: "https://researchr.org/alias/lubos-brim" - name: "Petr Jancar" link: "https://researchr.org/alias/petr-jancar" - name: "Mojmír Kretínský" link: "https://researchr.org/alias/mojm%C3%ADr-kret%C3%ADnsk%C3%BD" - name: "Antonín Kucera" link: "https://researchr.org/alias/anton%C3%ADn-kucera" volume: "2421" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-44043-7" kind: "inproceedings" key: "Gordon02:3" - title: "Stack inspection: theory and variants" author: - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2002" doi: "http://doi.acm.org/10.1145/503272.503301" links: doi: "http://doi.acm.org/10.1145/503272.503301" researchr: "https://researchr.org/publication/FournetG02" cites: 0 citedby: 0 pages: "307-318" booktitle: "POPL" kind: "inproceedings" key: "FournetG02" - title: "Preface" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Andrew M. Pitts" link: "https://researchr.org/alias/andrew-m.-pitts" year: "1999" doi: "http://www.elsevier.com/gej-ng/31/29/23/50/23/show/Products/notes/index.htt#001" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/50/23/show/Products/notes/index.htt#001" researchr: "https://researchr.org/publication/GordonP99" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "26" pages: "1-2" kind: "article" key: "GordonP99" - title: "Types and effects for asymmetric cryptographic protocols" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Alan Jeffrey" link: "https://researchr.org/alias/alan-jeffrey" year: "2004" tags: - "protocol" researchr: "https://researchr.org/publication/GordonJ04" cites: 0 citedby: 0 journal: "Journal of Computer Security" volume: "12" number: "3-4" pages: "435-483" kind: "article" key: "GordonJ04" - title: "Design and Semantics of a Decentralized Authorization Language" author: - name: "Moritz Y. Becker" link: "https://researchr.org/alias/moritz-y.-becker" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2007" doi: "http://dx.doi.org/10.1109/CSF.2007.18" links: doi: "http://dx.doi.org/10.1109/CSF.2007.18" tags: - "semantics" - "language design" - "design" researchr: "https://researchr.org/publication/BeckerFG07" cites: 0 citedby: 0 pages: "3-15" booktitle: "20th IEEE Computer Security Foundations Symposium, CSF 2007, 6-8 July 2007, Venice, Italy" publisher: "IEEE Computer Society" kind: "inproceedings" key: "BeckerFG07" - title: "From Stack Inspection to Access Control: A Security Analysis for Libraries" author: - name: "Frédéric Besson" link: "https://researchr.org/alias/fr%C3%A9d%C3%A9ric-besson" - name: "Tomasz Blanc" link: "https://researchr.org/alias/tomasz-blanc" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2004" doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2004.11" links: doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2004.11" tags: - "analysis" - "security" - "access control" researchr: "https://researchr.org/publication/BessonBFG04" cites: 0 citedby: 0 pages: "61" booktitle: "17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004), 28-30 June 2004, Pacific Grove, CA, USA" publisher: "IEEE Computer Society" isbn: "0-7695-2169-X" kind: "inproceedings" key: "BessonBFG04" - title: "A Hybrid Expert System for IT Security Risk Assessment" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Ivan Belik" link: "https://researchr.org/alias/ivan-belik" - name: "Shahram Rahimi" link: "https://researchr.org/alias/shahram-rahimi" year: "2010" links: dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pdpta/GordonBR10" tags: - "security" researchr: "https://researchr.org/publication/GordonBR10" cites: 0 citedby: 0 pages: "430-434" booktitle: "Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2010, Las Vegas, Nevada, USA, July 12-15, 2010, 2 Volumes" editor: - name: "Hamid R. Arabnia" link: "https://researchr.org/alias/hamid-r.-arabnia" - name: "Steve C. Chiu" link: "https://researchr.org/alias/steve-c.-chiu" - name: "George A. Gravvanis" link: "https://researchr.org/alias/george-a.-gravvanis" - name: "Minoru Ito" link: "https://researchr.org/alias/minoru-ito" - name: "Kazuki Joe" link: "https://researchr.org/alias/kazuki-joe" - name: "Hiroaki Nishikawa" link: "https://researchr.org/alias/hiroaki-nishikawa" - name: "Ashu M. G. Solo" link: "https://researchr.org/alias/ashu-m.-g.-solo" publisher: "CSREA Press" isbn: "1-60132-158-9" kind: "inproceedings" key: "GordonBR10" - title: "Compilation and Equivalence of Imperative Objects" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Paul D. Hankin" link: "https://researchr.org/alias/paul-d.-hankin" - name: "Søren B. Lassen" link: "https://researchr.org/alias/s%C3%B8ren-b.-lassen" year: "1999" tags: - "meta-model" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/GordonHL99" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "9" number: "4" pages: "373-426" kind: "article" key: "GordonHL99" - title: "SecPAL: Design and semantics of a decentralized authorization language" author: - name: "Moritz Y. Becker" link: "https://researchr.org/alias/moritz-y.-becker" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2010" doi: "http://dx.doi.org/10.3233/JCS-2009-0364" abstract: "We present a declarative authorization language. Policies and credentials are expressed using predicates defined by logical clauses, in the style of constraint logic programming. Access requests are mapped to logical authorization queries, consisting of predicates and constraints combined by conjunctions, disjunctions, and negations. Access is granted if the query succeeds against the current database of clauses. Predicates ascribe rights to particular principals, with flexible support for delegation and revocation. At the discretion of the delegator, delegated rights can be further delegated, either to a fixed depth, or arbitrarily deeply. Our language strikes a careful balance between syntactic and semantic simplicity, policy expressiveness, and execution efficiency. The syntax is close to natural language, and the semantics consists of just three deduction rules. The language can express many common policy idioms using constraints, controlled delegation, recursive predicates, and negated queries. We describe an execution strategy based on translation to Datalog with Constraints, and table-based resolution. We show that this execution strategy is sound, complete, and always terminates, despite recursion and negation, as long as simple syntactic conditions are met." links: doi: "http://dx.doi.org/10.3233/JCS-2009-0364" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jcs/BeckerFG10" tags: - "programming languages" - "semantics" - "rule-based" - "translation" - "completeness" - "language design" - "constraints" - "rules" - "logic programming" - "programming" - "database" - "logic" - "access control policies" - "access control" - "Datalog" - "design" - "role-based access control" - "query language" researchr: "https://researchr.org/publication/BeckerFG10" cites: 0 citedby: 0 journal: "Journal of Computer Security" volume: "18" number: "4" pages: "619-665" kind: "article" key: "BeckerFG10" - title: "A Type and Effect Analysis of Security Protocols" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Alan Jeffrey" link: "https://researchr.org/alias/alan-jeffrey" year: "2001" doi: "http://link.springer.de/link/service/series/0558/bibs/2126/21260432.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2126/21260432.htm" tags: - "protocol" - "analysis" - "security" researchr: "https://researchr.org/publication/GordonJ01%3A1" cites: 0 citedby: 0 pages: "432" booktitle: "Static Analysis, 8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings" editor: - name: "Patrick Cousot" link: "https://researchr.org/alias/patrick-cousot" volume: "2126" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-42314-1" kind: "inproceedings" key: "GordonJ01:1" - title: "Branching Storylines in Virtual Reality Environments for Leadership Development" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Michael van Lent" link: "https://researchr.org/alias/michael-van-lent" - name: "Martin Van Velsen" link: "https://researchr.org/alias/martin-van-velsen" - name: "Paul Carpenter" link: "https://researchr.org/alias/paul-carpenter" - name: "Arnav Jhala" link: "https://researchr.org/alias/arnav-jhala" year: "2004" tags: - "Meta-Environment" researchr: "https://researchr.org/publication/GordonLVCJ04" cites: 0 citedby: 0 pages: "844-851" booktitle: "Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, July 25-29, 2004, San Jose, California, USA" editor: - name: "Deborah L. McGuinness" link: "https://researchr.org/alias/deborah-l.-mcguinness" - name: "George Ferguson" link: "https://researchr.org/alias/george-ferguson" publisher: "AAAI Press / The MIT Press" isbn: "0-262-51183-5" kind: "inproceedings" key: "GordonLVCJ04" - title: "Type Inference for Correspondence Types" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Hans Hüttel" link: "https://researchr.org/alias/hans-h%C3%A3%C2%BCttel" - name: "René Rydhof Hansen" link: "https://researchr.org/alias/ren%C3%A3%C2%A9-rydhof-hansen" year: "2009" doi: "http://dx.doi.org/10.1016/j.entcs.2009.07.079" abstract: "We present a correspondence type/effect system for authenticity in a π-calculus with polarized channels, dependent pair types and effect terms and show how one may, given a process P and an a priori type environment E, generate constraints that are formulae in the Alternating Least Fixed-Point (ALFP) logic. We then show how a reasonable model of the generated constraints yields a type/effect assignment such that P becomes well-typed with respect to E if and only if this is possible. The formulae generated satisfy a finite model property; a system of constraints is satisfiable if and only if it has a finite model. As a consequence, we obtain the result that type/effect inference in our system is polynomial-time decidable. " links: doi: "http://dx.doi.org/10.1016/j.entcs.2009.07.079" tags: - "type inference" - "meta-model" - "modeling" - "constraints" - "type system" - "e-science" - "logic" - "Meta-Environment" - "process modeling" researchr: "https://researchr.org/publication/GordonHH09" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "242" number: "3" pages: "21-36" kind: "article" key: "GordonHH09" - title: "Preface" author: - name: "Luca Aceto" link: "https://researchr.org/alias/luca-aceto" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2006" doi: "http://dx.doi.org/10.1016/j.entcs.2005.12.100" links: doi: "http://dx.doi.org/10.1016/j.entcs.2005.12.100" researchr: "https://researchr.org/publication/AcetoG06" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "162" pages: "1-2" kind: "article" key: "AcetoG06" - title: "Reasoning about Cryptographic Protocols in the Spi Calculus" author: - name: "Martín Abadi" link: "http://users.soe.ucsc.edu/~abadi/home.html" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1997" tags: - "protocol" researchr: "https://researchr.org/publication/AbadiG97%3A0" cites: 0 citedby: 0 pages: "59-73" booktitle: "CONCUR 97: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings" editor: - name: "Antoni W. Mazurkiewicz" link: "https://researchr.org/alias/antoni-w.-mazurkiewicz" - name: "Józef Winkowski" link: "https://researchr.org/alias/j%C3%B3zef-winkowski" volume: "1243" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-63141-0" kind: "inproceedings" key: "AbadiG97:0" - title: "Refinement Types for Secure Implementations" author: - name: "Jesper Bengtson" link: "https://researchr.org/alias/jesper-bengtson" - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Sergio Maffeis" link: "https://researchr.org/alias/sergio-maffeis" year: "2008" doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2008.27" links: doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2008.27" tags: - "refinement" researchr: "https://researchr.org/publication/BengtsonBFGM08" cites: 0 citedby: 0 pages: "17-32" booktitle: "Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, 23-25 June 2008" publisher: "IEEE Computer Society" isbn: "978-0-7695-3182-3" kind: "inproceedings" key: "BengtsonBFGM08" - title: "Bisimilarity as a Theory of Functional Programming" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1999" doi: "http://dx.doi.org/10.1016/S0304-3975(98)00353-3" links: doi: "http://dx.doi.org/10.1016/S0304-3975(98)00353-3" tags: - "functional programming" - "programming" researchr: "https://researchr.org/publication/Gordon99" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "228" number: "1-2" pages: "5-47" kind: "article" key: "Gordon99" - title: "A Chart Semantics for the Pi-Calculus" author: - name: "Johannes Borgström" link: "https://researchr.org/alias/johannes-borgstr%C3%B6m" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Andrew Phillips" link: "https://researchr.org/alias/andrew-phillips" year: "2008" doi: "http://dx.doi.org/10.1016/j.entcs.2007.11.002" links: doi: "http://dx.doi.org/10.1016/j.entcs.2007.11.002" tags: - "semantics" researchr: "https://researchr.org/publication/BorgstromGP08" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "194" number: "2" pages: "3-29" kind: "article" key: "BorgstromGP08" - title: "Verified implementations of the information card federated identity-management protocol" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Nikhil Swamy" link: "https://researchr.org/alias/nikhil-swamy" year: "2008" doi: "http://doi.acm.org/10.1145/1368310.1368330" links: doi: "http://doi.acm.org/10.1145/1368310.1368330" tags: - "protocol" researchr: "https://researchr.org/publication/BhargavanFGS08" cites: 0 citedby: 0 pages: "123-135" booktitle: "Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, ASIACCS 2008, Tokyo, Japan, March 18-20, 2008" editor: - name: "Masayuki Abe" link: "https://researchr.org/alias/masayuki-abe" - name: "Virgil D. Gligor" link: "https://researchr.org/alias/virgil-d.-gligor" publisher: "ACM" isbn: "978-1-59593-979-1" kind: "inproceedings" key: "BhargavanFGS08" - title: "Validating a Web service security abstraction by typing" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Riccardo Pucella" link: "https://researchr.org/alias/riccardo-pucella" year: "2002" doi: "http://doi.acm.org/10.1145/764792.764797" links: doi: "http://doi.acm.org/10.1145/764792.764797" tags: - "web service" - "security" - "abstraction" researchr: "https://researchr.org/publication/GordonP02" cites: 0 citedby: 0 pages: "18-29" booktitle: "Proceedings of the 2002 ACM Workshop on XML Security, Fairfax, VA, USA, November 22, 2002" editor: - name: "Michiharu Kudo" link: "https://researchr.org/alias/michiharu-kudo" publisher: "ACM" isbn: "1-58113-632-3" kind: "inproceedings" key: "GordonP02" - title: "Authenticity Types for Cryptographic Protocols" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2002" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2629&spage=3" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2629&spage=3" tags: - "protocol" researchr: "https://researchr.org/publication/Gordon02%3A1" cites: 0 citedby: 0 pages: "3" booktitle: "Formal Aspects of Security, First International Conference, FASec 2002, London, UK, December 16-18, 2002, Revised Papers" editor: - name: "Ali E. Abdallah" link: "https://researchr.org/alias/ali-e.-abdallah" - name: "Peter Ryan" link: "https://researchr.org/alias/peter-ryan" - name: "Steve Schneider" link: "https://researchr.org/alias/steve-schneider" volume: "2629" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-20693-0" kind: "inproceedings" key: "Gordon02:1" - title: "A Bisimulation Method for Cryptographic Protocols" author: - name: "Martín Abadi" link: "https://researchr.org/alias/mart%C3%ADn-abadi" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1998" tags: - "protocol" researchr: "https://researchr.org/publication/AbadiG98%3A0" cites: 0 citedby: 0 journal: "Nord. J. Comput." volume: "5" number: "4" pages: "267" kind: "article" key: "AbadiG98:0" - title: "Finite-Control Mobile Ambients" author: - name: "Witold Charatonik" link: "https://researchr.org/alias/witold-charatonik" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Jean-Marc Talbot" link: "https://researchr.org/alias/jean-marc-talbot" year: "2002" doi: "http://link.springer.de/link/service/series/0558/bibs/2305/23050295.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2305/23050295.htm" tags: - "mobile" researchr: "https://researchr.org/publication/CharatonikGT02" cites: 0 citedby: 0 pages: "295-313" booktitle: "Programming Languages and Systems, 11th European Symposium on Programming, ESOP 2002, held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings" editor: - name: "Daniel Le Métayer" link: "https://researchr.org/alias/daniel-le-m%C3%A9tayer" volume: "2305" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-43363-5" kind: "inproceedings" key: "CharatonikGT02" - title: "Service Combinators for Farming Virtual Machines" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Iman Narasamdya" link: "https://researchr.org/alias/iman-narasamdya" year: "2007" doi: "http://dx.doi.org/10.1007/978-3-540-78663-4_3" links: doi: "http://dx.doi.org/10.1007/978-3-540-78663-4_3" researchr: "https://researchr.org/publication/BhargavanGN07" cites: 0 citedby: 0 pages: "22" booktitle: "Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers" editor: - name: "Gilles Barthe" link: "https://researchr.org/alias/gilles-barthe" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" volume: "4912" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-78662-7" kind: "inproceedings" key: "BhargavanGN07" - title: "An Operational Semantics for I/O in a Lazy Functional Language" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1993" tags: - "laziness" - "semantics" - "operational semantics" researchr: "https://researchr.org/publication/Gordon93%3A2" cites: 0 citedby: 0 pages: "136-145" booktitle: "FPCA" kind: "inproceedings" key: "Gordon93:2" - title: "Modular verification of security protocol code by typing" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A3%C2%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2010" doi: "http://doi.acm.org/10.1145/1706299.1706350" links: doi: "http://doi.acm.org/10.1145/1706299.1706350" tags: - "protocol" - "security" researchr: "https://researchr.org/publication/BhargavanFG10" cites: 0 citedby: 0 pages: "445-456" booktitle: "Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010" editor: - name: "Manuel V. Hermenegildo" link: "https://researchr.org/alias/manuel-v.-hermenegildo" - name: "Jens Palsberg" link: "https://researchr.org/alias/jens-palsberg" publisher: "ACM" isbn: "978-1-60558-479-9" kind: "inproceedings" key: "BhargavanFG10" - title: "Model checking mobile ambients" author: - name: "Witold Charatonik" link: "https://researchr.org/alias/witold-charatonik" - name: "Silvano Dal-Zilio" link: "https://researchr.org/alias/silvano-dal-zilio" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Supratik Mukhopadhyay" link: "https://researchr.org/alias/supratik-mukhopadhyay" - name: "Jean-Marc Talbot" link: "https://researchr.org/alias/jean-marc-talbot" year: "2003" doi: "http://dx.doi.org/10.1016/S0304-3975(02)00832-0" links: doi: "http://dx.doi.org/10.1016/S0304-3975(02)00832-0" tags: - "model checking" - "meta-model" - "Meta-Environment" - "mobile" researchr: "https://researchr.org/publication/CharatonikDGMT03" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "308" number: "1-3" pages: "277-331" kind: "article" key: "CharatonikDGMT03" - title: "A semantics for web services authentication" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2005" doi: "http://dx.doi.org/10.1016/j.tcs.2005.03.005" links: doi: "http://dx.doi.org/10.1016/j.tcs.2005.03.005" tags: - "semantics" - "web service" - "web services" researchr: "https://researchr.org/publication/BhargavanFG05" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "340" number: "1" pages: "102-153" kind: "article" key: "BhargavanFG05" - title: "Verifying policy-based security for web services" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2004" doi: "http://doi.acm.org/10.1145/1030083.1030120" links: doi: "http://doi.acm.org/10.1145/1030083.1030120" tags: - "rule-based" - "web service" - "security" - "web services" researchr: "https://researchr.org/publication/BhargavanFG04" cites: 0 citedby: 0 pages: "268-277" booktitle: "Proceedings of the 11th ACM Conference on Computer and Communications Security, CCS 2004, Washingtion, DC, USA, October 25-29, 2004" editor: - name: "Vijayalakshmi Atluri" link: "https://researchr.org/alias/vijayalakshmi-atluri" - name: "Birgit Pfitzmann" link: "https://researchr.org/alias/birgit-pfitzmann" - name: "Patrick Drew McDaniel" link: "https://researchr.org/alias/patrick-drew-mcdaniel" publisher: "ACM" isbn: "1-58113-961-6" kind: "inproceedings" key: "BhargavanFG04" - title: "Preface" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Andrew M. Pitts" link: "https://researchr.org/alias/andrew-m.-pitts" - name: "Carolyn L. Talcott" link: "https://researchr.org/alias/carolyn-l.-talcott" year: "1997" doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#001" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#001" researchr: "https://researchr.org/publication/GordonPT97" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "10" pages: "1" kind: "article" key: "GordonPT97" - title: "Types for Cyphers: Thwarting Mischief and Malice with Type Theory" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2001" tags: - "type theory" researchr: "https://researchr.org/publication/Gordon01" cites: 0 citedby: 0 pages: "136" booktitle: "Proceedings of the 3rd international ACM SIGPLAN conference on Principles and practice of declarative programming, September 5-7, 2001, Florence, Italy" publisher: "ACM" isbn: "1-58113-388-X" kind: "inproceedings" key: "Gordon01" - title: "Typing correspondence assertions for communication protocols" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Alan Jeffrey" link: "https://researchr.org/alias/alan-jeffrey" year: "2003" doi: "http://dx.doi.org/10.1016/S0304-3975(02)00333-X" links: doi: "http://dx.doi.org/10.1016/S0304-3975(02)00333-X" tags: - "protocol" researchr: "https://researchr.org/publication/GordonJ03" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "300" number: "1-3" pages: "379-409" kind: "article" key: "GordonJ03" - title: "V for Virtual" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2006" doi: "http://dx.doi.org/10.1016/j.entcs.2006.01.030" links: doi: "http://dx.doi.org/10.1016/j.entcs.2006.01.030" researchr: "https://researchr.org/publication/Gordon06" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "162" pages: "177-181" kind: "article" key: "Gordon06" - title: "Types and Effects for Asymmetric Cryptographic Protocols" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Alan Jeffrey" link: "https://researchr.org/alias/alan-jeffrey" year: "2002" doi: "http://csdl.computer.org/comp/proceedings/csfw/2002/1689/00/16890077abs.htm" links: doi: "http://csdl.computer.org/comp/proceedings/csfw/2002/1689/00/16890077abs.htm" tags: - "protocol" researchr: "https://researchr.org/publication/GordonJ02" cites: 0 citedby: 0 pages: "77-91" booktitle: "15th IEEE Computer Security Foundations Workshop (CSFW-15 2002), 24-26 June 2002, Cape Breton, Nova Scotia, Canada" publisher: "IEEE Computer Society" isbn: "0-7695-1689-0" kind: "inproceedings" key: "GordonJ02" - title: "Preface for the Special Issue: Foundations of Software Science and Computation Structures" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2005" doi: "http://dx.doi.org/10.1016/j.tcs.2004.11.001" links: doi: "http://dx.doi.org/10.1016/j.tcs.2004.11.001" tags: - "e-science" researchr: "https://researchr.org/publication/Gordon05%3A0" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "333" number: "1-2" pages: "1" kind: "article" key: "Gordon05:0" - title: "Validating a web service security abstraction by typing" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Riccardo Pucella" link: "https://researchr.org/alias/riccardo-pucella" year: "2005" doi: "http://dx.doi.org/10.1007/s00165-004-0058-1" links: doi: "http://dx.doi.org/10.1007/s00165-004-0058-1" tags: - "web service" - "security" - "abstraction" researchr: "https://researchr.org/publication/GordonP05%3A0" cites: 0 citedby: 0 journal: "Formal Asp. Comput." volume: "17" number: "3" pages: "277-318" kind: "article" key: "GordonP05:0" - title: "The Formal Definition of a Synchronous Hardware-Description Language in Higher Order Logic" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1992" tags: - "logic" researchr: "https://researchr.org/publication/Gordon92a" cites: 0 citedby: 0 pages: "531-534" booktitle: "Proceedings 1991 IEEE International Conference on Computer Design: VLSI in Computer & Processors, ICCD 92, Cambridge, MA, USA, October 11-14, 1992" publisher: "IEEE Computer Society" isbn: "0-8186-3110-4" kind: "inproceedings" key: "Gordon92a" - title: "Mobility Types for Mobile Ambients" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Giorgio Ghelli" link: "https://researchr.org/alias/giorgio-ghelli" year: "1999" doi: "http://link.springer.de/link/service/series/0558/bibs/1644/16440230.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1644/16440230.htm" tags: - "mobile" researchr: "https://researchr.org/publication/CardelliGG99" cites: 0 citedby: 0 pages: "230-239" booktitle: "Automata, Languages and Programming, 26th International Colloquium, ICALP 99, Prague, Czech Republic, July 11-15, 1999, Proceedings" editor: - name: "Jirí Wiedermann" link: "https://researchr.org/alias/jir%C3%AD-wiedermann" - name: "Peter van Emde Boas" link: "https://researchr.org/alias/peter-van-emde-boas" - name: "Mogens Nielsen" link: "https://researchr.org/alias/mogens-nielsen" volume: "1644" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-66224-3" kind: "inproceedings" key: "CardelliGG99" - title: "Logical Properties of Name Restriction" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2001" doi: "http://link.springer.de/link/service/series/0558/bibs/2044/20440046.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2044/20440046.htm" researchr: "https://researchr.org/publication/CardelliG01%3A0" cites: 0 citedby: 0 pages: "46-60" booktitle: "Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings" editor: - name: "Samson Abramsky" link: "https://researchr.org/alias/samson-abramsky" volume: "2044" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-41960-8" kind: "inproceedings" key: "CardelliG01:0" - title: "Provable Implementations of Security Protocols" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2006" doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2006.43" links: doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2006.43" tags: - "protocol" - "security" researchr: "https://researchr.org/publication/Gordon06%3A2" cites: 0 citedby: 0 pages: "345-346" booktitle: "21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings" publisher: "IEEE Computer Society" kind: "inproceedings" key: "Gordon06:2" - title: "Typing Correspondence Assertions for Communication Protocols" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Alan Jeffrey" link: "https://researchr.org/alias/alan-jeffrey" year: "2001" doi: "http://www.elsevier.com/gej-ng/31/29/23/88/27/show/Products/notes/index.htt#009" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/88/27/show/Products/notes/index.htt#009" tags: - "protocol" researchr: "https://researchr.org/publication/GordonJ01" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "45" pages: "119-140" kind: "article" key: "GordonJ01" - title: "Guest Editors Foreword" author: - name: "Luca Aceto" link: "https://researchr.org/alias/luca-aceto" - name: "Mario Bravetti" link: "https://researchr.org/alias/mario-bravetti" - name: "Wan Fokkink" link: "http://www.cs.vu.nl/~wanf/" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2007" doi: "http://dx.doi.org/10.1016/j.jlap.2006.08.002" links: doi: "http://dx.doi.org/10.1016/j.jlap.2006.08.002" researchr: "https://researchr.org/publication/AcetoBFG07" cites: 0 citedby: 0 journal: "Journal of Logic and Algebraic Programming" volume: "70" number: "2" pages: "119-120" kind: "article" key: "AcetoBFG07" - title: "Mobile Ambients" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1998" doi: "http://link.springer.de/link/service/series/0558/bibs/1378/13780140.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1378/13780140.htm" tags: - "mobile" researchr: "https://researchr.org/publication/CardelliG98" cites: 0 citedby: 0 pages: "140-155" booktitle: "Foundations of Software Science and Computation Structure, First International Conference, FoSSaCS 98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings" editor: - name: "Maurice Nivat" link: "https://researchr.org/alias/maurice-nivat" volume: "1378" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-64300-1" kind: "inproceedings" key: "CardelliG98" - title: "Authenticity by Typing for Security Protocols" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Alan Jeffrey" link: "https://researchr.org/alias/alan-jeffrey" year: "2003" tags: - "protocol" - "security" researchr: "https://researchr.org/publication/GordonJ03%3A0" cites: 0 citedby: 0 journal: "Journal of Computer Security" volume: "11" number: "4" pages: "451-520" kind: "article" key: "GordonJ03:0" - title: "Deciding validity in a spatial logic for trees" author: - name: "Cristiano Calcagno" link: "https://researchr.org/alias/cristiano-calcagno" - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2003" doi: "http://doi.acm.org/10.1145/604174.604183" links: doi: "http://doi.acm.org/10.1145/604174.604183" tags: - "logic" researchr: "https://researchr.org/publication/CalcagnoCG03" cites: 0 citedby: 0 pages: "62-73" booktitle: "Proceedings of TLDI 03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, New Orleans, Louisiana, USA, January 18, 2003" editor: - name: "Zhong Shao" link: "https://researchr.org/alias/zhong-shao" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" publisher: "ACM" isbn: "1-58113-649-8" kind: "inproceedings" key: "CalcagnoCG03" - title: "A Sound Metalogical Semantics for Input/Output Effects" author: - name: "Roy L. Crole" link: "https://researchr.org/alias/roy-l.-crole" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1994" tags: - "semantics" researchr: "https://researchr.org/publication/CroleG94" cites: 0 citedby: 0 pages: "339-353" booktitle: "Computer Science Logic, 8th International Workshop, CSL 94, Kazimierz, Poland, September 25-30, 1994, Selected Papers" editor: - name: "Leszek Pacholski" link: "https://researchr.org/alias/leszek-pacholski" - name: "Jerzy Tiuryn" link: "https://researchr.org/alias/jerzy-tiuryn" volume: "933" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-60017-5" kind: "inproceedings" key: "CroleG94" - title: "XML Web Services: The Global Computer?" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2002" tags: - "XML" - "XML Schema" - "web service" - "web services" researchr: "https://researchr.org/publication/Gordon02%3A0" cites: 0 citedby: 0 pages: "355" booktitle: "Foundations of Information Technology in the Era of Networking and Mobile Computing, IFIP 17:::th::: World Computer Congress - TC1 Stream / 2:::nd::: IFIP International Conference on Theoretical Computer Science (TCS 2002), August 25-30, 2002, Montr&eacut" editor: - name: "Ricardo A. Baeza-Yates" link: "https://researchr.org/alias/ricardo-a.-baeza-yates" - name: "Ugo Montanari" link: "https://researchr.org/alias/ugo-montanari" - name: "Nicola Santoro" link: "https://researchr.org/alias/nicola-santoro" volume: "223" series: "IFIP Conference Proceedings" publisher: "Kluwer" isbn: "1-4020-7181-7" kind: "inproceedings" key: "Gordon02:0" - title: "A semantics for web services authentication" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2004" doi: "http://doi.acm.org/10.1145/964001.964018" abstract: "We consider the problem of specifying and verifying cryptographic security protocols for XML web services. The security specification WS-Security describes a range of XML security tokens, such as username tokens, public-key certificates, and digital signature blocks, amounting to a flexible vocabulary for expressing protocols. To describe the syntax of these tokens, we extend the usual XML data model with symbolic representations of cryptographic values. We use predicates on this data model to describe the semantics of security tokens and of sample protocols distributed with the Microsoft WSE implementation of WS-Security. By embedding our data model within Abadi and Fournet's applied pi calculus, we formulate and prove security properties with respect to the standard Dolev-Yao threat model. Moreover, we informally discuss issues not addressed by the formal model. To the best of our knowledge, this is the first approach to the specification and verification of security protocols based on a faithful account of the XML wire format. " links: doi: "http://doi.acm.org/10.1145/964001.964018" tags: - "semantics" - "rule-based" - "formal semantics" - "meta-model" - "XML" - "XML Schema" - "protocol" - "web service" - "data-flow" - "certification" - "security" - "web services" - "Meta-Environment" - "systematic-approach" researchr: "https://researchr.org/publication/BhargavanFG04%3A0" cites: 0 citedby: 0 pages: "198-209" booktitle: "Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004" editor: - name: "Neil D. Jones" link: "http://www.diku.dk/hjemmesider/ansatte/neil/" - name: "Xavier Leroy" link: "http://pauillac.inria.fr/~xleroy/" publisher: "ACM" isbn: "1-58113-729-X" kind: "inproceedings" key: "BhargavanFG04:0" - title: "Secrecy, Group Creation" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Giorgio Ghelli" link: "https://researchr.org/alias/giorgio-ghelli" year: "2000" doi: "http://www.elsevier.com/gej-ng/31/29/23/97/27/show/Products/notes/index.htt#006" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/97/27/show/Products/notes/index.htt#006" researchr: "https://researchr.org/publication/CardelliGG00" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "40" pages: "7" kind: "article" key: "CardelliGG00" - title: "Five Axioms of Alpha-Conversion" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Thomas F. Melham" link: "https://researchr.org/alias/thomas-f.-melham" year: "1996" researchr: "https://researchr.org/publication/GordonM96" cites: 0 citedby: 0 pages: "173-190" booktitle: "Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs 96, Turku, Finland, August 26-30, 1996, Proceedings" editor: - name: "Joakim von Wright" link: "https://researchr.org/alias/joakim-von-wright" - name: "Jim Grundy" link: "https://researchr.org/alias/jim-grundy" - name: "John Harrison" link: "https://researchr.org/alias/john-harrison" volume: "1125" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-61587-3" kind: "inproceedings" key: "GordonM96" - title: "Recognizing Expressions of Commonsense Psychology in English Text" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Abe Kazemzadeh" link: "https://researchr.org/alias/abe-kazemzadeh" - name: "Anish Nair" link: "https://researchr.org/alias/anish-nair" - name: "Milena Petrova" link: "https://researchr.org/alias/milena-petrova" year: "2003" doi: "http://acl.ldc.upenn.edu/acl2003/main/pdfs/Gordon.pdf" links: doi: "http://acl.ldc.upenn.edu/acl2003/main/pdfs/Gordon.pdf" researchr: "https://researchr.org/publication/GordonKNP03" cites: 0 citedby: 0 pages: "208-215" booktitle: "ACL" kind: "inproceedings" key: "GordonKNP03" - title: "The Complexity of Model Checking Mobile Ambients" author: - name: "Witold Charatonik" link: "https://researchr.org/alias/witold-charatonik" - name: "Silvano Dal-Zilio" link: "https://researchr.org/alias/silvano-dal-zilio" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Supratik Mukhopadhyay" link: "https://researchr.org/alias/supratik-mukhopadhyay" - name: "Jean-Marc Talbot" link: "https://researchr.org/alias/jean-marc-talbot" year: "2001" doi: "http://link.springer.de/link/service/series/0558/bibs/2030/20300152.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2030/20300152.htm" tags: - "model checking" - "meta-model" - "Meta-Environment" - "mobile" researchr: "https://researchr.org/publication/CharatonikDGMT01" cites: 0 citedby: 0 pages: "152-167" booktitle: "Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings" editor: - name: "Furio Honsell" link: "https://researchr.org/alias/furio-honsell" - name: "Marino Miculan" link: "https://researchr.org/alias/marino-miculan" volume: "2030" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-41864-4" kind: "inproceedings" key: "CharatonikDGMT01" - title: "Types for the Ambient Calculus" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Giorgio Ghelli" link: "https://researchr.org/alias/giorgio-ghelli" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2002" doi: "http://dx.doi.org/10.1006/inco.2001.3121" links: doi: "http://dx.doi.org/10.1006/inco.2001.3121" researchr: "https://researchr.org/publication/CardelliGG02" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "177" number: "2" pages: "160-194" kind: "article" key: "CardelliGG02" - title: "Secrecy and Group Creation" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Giorgio Ghelli" link: "https://researchr.org/alias/giorgio-ghelli" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2000" doi: "http://link.springer.de/link/service/series/0558/bibs/1877/18770365.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1877/18770365.htm" researchr: "https://researchr.org/publication/CardelliGG00%3A0" cites: 0 citedby: 0 pages: "365-379" booktitle: "CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings" editor: - name: "Catuscia Palamidessi" link: "https://researchr.org/alias/catuscia-palamidessi" volume: "1877" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-67897-2" kind: "inproceedings" key: "CardelliGG00:0" - title: "Secrecy Despite Compromise: Types, Cryptography, and the Pi-Calculus" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Alan Jeffrey" link: "https://researchr.org/alias/alan-jeffrey" year: "2005" doi: "http://dx.doi.org/10.1007/11539452_17" links: doi: "http://dx.doi.org/10.1007/11539452_17" researchr: "https://researchr.org/publication/GordonJ05" cites: 0 citedby: 0 pages: "186-201" booktitle: "CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings" editor: - name: "Martín Abadi" link: "https://researchr.org/alias/mart%C3%ADn-abadi" - name: "Luca de Alfaro" link: "https://researchr.org/alias/luca-de-alfaro" volume: "3653" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-28309-9" kind: "inproceedings" key: "GordonJ05" - title: "Verified Reference Implementations of WS-Security Protocols" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2006" doi: "http://dx.doi.org/10.1007/11841197_6" links: doi: "http://dx.doi.org/10.1007/11841197_6" tags: - "protocol" - "security" researchr: "https://researchr.org/publication/BhargavanFG06" cites: 0 citedby: 0 pages: "88-106" booktitle: "Web Services and Formal Methods, Third International Workshop, WS-FM 2006 Vienna, Austria, September 8-9, 2006, Proceedings" editor: - name: "Mario Bravetti" link: "https://researchr.org/alias/mario-bravetti" - name: "Manuel Núñez" link: "https://researchr.org/alias/manuel-n%C3%BA%C3%B1ez" - name: "Gianluigi Zavattaro" link: "https://researchr.org/alias/gianluigi-zavattaro" volume: "4184" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-38862-1" kind: "inproceedings" key: "BhargavanFG06" - title: "Equational Properties Of Mobile Ambients" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Luca Cardelli" link: "http://lucacardelli.name" year: "2003" tags: - "mobile" researchr: "https://researchr.org/publication/GordonC03" cites: 0 citedby: 0 journal: "Mathematical Structures in Computer Science" volume: "13" number: "3" pages: "371-408" kind: "article" key: "GordonC03" - title: "Anytime, Anywhere: Modal Logics for Mobile Ambients" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2000" doi: "http://doi.acm.org/10.1145/325694.325742" links: doi: "http://doi.acm.org/10.1145/325694.325742" tags: - "modal logic" - "logic" - "mobile" researchr: "https://researchr.org/publication/CardelliG00" cites: 0 citedby: 0 pages: "365-377" booktitle: "POPL" kind: "inproceedings" key: "CardelliG00" - title: "Region Analysis and a pi-Calculus wiht Groups" author: - name: "Silvano Dal-Zilio" link: "https://researchr.org/alias/silvano-dal-zilio" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2000" doi: "http://link.springer.de/link/service/series/0558/bibs/1893/18930001.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1893/18930001.htm" tags: - "analysis" researchr: "https://researchr.org/publication/Dal-ZilioG00" cites: 0 citedby: 0 pages: "1-20" booktitle: "Mathematical Foundations of Computer Science 2000, 25th International Symposium, MFCS 2000, Bratislava, Slovakia, August 28 - September 1, 2000, Proceedings" editor: - name: "Mogens Nielsen" link: "https://researchr.org/alias/mogens-nielsen" - name: "Branislav Rovan" link: "https://researchr.org/alias/branislav-rovan" volume: "1893" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-67901-4" kind: "inproceedings" key: "Dal-ZilioG00" - title: "A type discipline for authorization policies" author: - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Sergio Maffeis" link: "https://researchr.org/alias/sergio-maffeis" year: "2007" doi: "http://doi.acm.org/10.1145/1275497.1275500" links: doi: "http://doi.acm.org/10.1145/1275497.1275500" researchr: "https://researchr.org/publication/FournetGM07" cites: 0 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "29" number: "5" pages: "25" kind: "article" key: "FournetGM07" - title: "A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1993" researchr: "https://researchr.org/publication/Gordon93%3A0" cites: 0 citedby: 0 pages: "413-425" booktitle: "Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG 93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings" editor: - name: "Jeffrey J. Joyce" link: "https://researchr.org/alias/jeffrey-j.-joyce" - name: "Carl-Johan H. Seger" link: "https://researchr.org/alias/carl-johan-h.-seger" volume: "780" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-57826-9" kind: "inproceedings" key: "Gordon93:0" - title: "Typing One-to-One and One-to-Many Correspondences in Security Protocols" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Alan Jeffrey" link: "https://researchr.org/alias/alan-jeffrey" year: "2002" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2609&spage=263" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2609&spage=263" tags: - "protocol" - "security" researchr: "https://researchr.org/publication/GordonJ02%3A0" cites: 0 citedby: 0 pages: "263-282" booktitle: "Software Security -- Theories and Systems, Mext-NSF-JSPS International Symposium, ISSS 2002, Tokyo, Japan, November 8-10, 2002, Revised Papers" editor: - name: "Mitsuhiro Okada" link: "https://researchr.org/alias/mitsuhiro-okada" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Andre Scedrov" link: "https://researchr.org/alias/andre-scedrov" - name: "Hideyuki Tokuda" link: "https://researchr.org/alias/hideyuki-tokuda" - name: "Akinori Yonezawa" link: "https://researchr.org/alias/akinori-yonezawa" volume: "2609" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-00708-3" kind: "inproceedings" key: "GordonJ02:0" - title: "Secure sessions for Web services" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Ricardo Corin" link: "https://researchr.org/alias/ricardo-corin" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2007" doi: "http://doi.acm.org/10.1145/1237500.1237504" links: doi: "http://doi.acm.org/10.1145/1237500.1237504" tags: - "web service" - "web services" researchr: "https://researchr.org/publication/BhargavanCFG07" cites: 0 citedby: 0 journal: "ACM Trans. Inf. Syst. Secur." volume: "10" number: "2" pages: "8" kind: "article" key: "BhargavanCFG07" - title: "Guided Conversations about Leadership: Mentoring with Movies and Interactive Characters" author: - name: "Randall W. Hill Jr." link: "https://researchr.org/alias/randall-w.-hill-jr." - name: "Jay Douglas" link: "https://researchr.org/alias/jay-douglas" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Frederic H. Pighin" link: "https://researchr.org/alias/frederic-h.-pighin" - name: "Martin Van Velsen" link: "https://researchr.org/alias/martin-van-velsen" year: "2003" researchr: "https://researchr.org/publication/HillDGPV03" cites: 0 citedby: 0 pages: "101-108" booktitle: "Proceedings of the Fifteenth Conference on Innovative Applications of Artificial Intelligence, August 12-14, 2003, Acapulco, Mexico" editor: - name: "John Riedl" link: "https://researchr.org/alias/john-riedl" - name: "Randall W. Hill Jr." link: "https://researchr.org/alias/randall-w.-hill-jr." publisher: "AAAI" isbn: "1-57735-188-6" kind: "inproceedings" key: "HillDGPV03" - title: "Experience with Embedding Hardware Description Languages in HOL" author: - name: "Richard J. Boulton" link: "https://researchr.org/alias/richard-j.-boulton" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Michael J. C. Gordon" link: "https://researchr.org/alias/michael-j.-c.-gordon" - name: "John Harrison" link: "https://researchr.org/alias/john-harrison" - name: "John Herbert" link: "https://researchr.org/alias/john-herbert" - name: "John Van Tassel" link: "https://researchr.org/alias/john-van-tassel" year: "1992" tags: - "C++" researchr: "https://researchr.org/publication/BoultonGGHHT92" cites: 0 citedby: 0 pages: "129-156" booktitle: "Theorem Provers in Circuit Design, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, The Netherlands, 22-24 June 1992, Proceedings" editor: - name: "Victoria Stavridou" link: "https://researchr.org/alias/victoria-stavridou" - name: "Thomas F. Melham" link: "https://researchr.org/alias/thomas-f.-melham" - name: "Raymond T. Boute" link: "https://researchr.org/alias/raymond-t.-boute" volume: "A-10" series: "IFIP Transactions" publisher: "North-Holland" isbn: "0-444-89686-4" kind: "inproceedings" key: "BoultonGGHHT92" - title: "Types for Mobile Ambients" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1999" doi: "http://doi.acm.org/10.1145/292540.292550" links: doi: "http://doi.acm.org/10.1145/292540.292550" tags: - "mobile" researchr: "https://researchr.org/publication/CardelliG99" cites: 0 citedby: 0 pages: "79-92" booktitle: "POPL" kind: "inproceedings" key: "CardelliG99" - title: "Compilation and Equivalence of Imperative Objects" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Paul D. Hankin" link: "https://researchr.org/alias/paul-d.-hankin" - name: "Søren B. Lassen" link: "https://researchr.org/alias/s%C3%B8ren-b.-lassen" year: "1997" doi: "http://link.springer.de/link/service/series/0558/bibs/1346/13460074.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1346/13460074.htm" tags: - "meta-model" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/GordonHL97" cites: 0 citedby: 0 pages: "74-87" booktitle: "Foundations of Software Technology and Theoretical Computer Science, 17th Conference, Kharagpur, India, December 18-20, 1997, Proceedings" editor: - name: "S. Ramesh" link: "https://researchr.org/alias/s.-ramesh" - name: "G. Sivakumar" link: "https://researchr.org/alias/g.-sivakumar" volume: "1346" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-63876-8" kind: "inproceedings" key: "GordonHL97" - title: "Region analysis and a pi-calculus with groups" author: - name: "Silvano Dal-Zilio" link: "https://researchr.org/alias/silvano-dal-zilio" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2002" tags: - "analysis" researchr: "https://researchr.org/publication/Dal-ZilioG02" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "12" number: "3" pages: "229-292" kind: "article" key: "Dal-ZilioG02" - title: "A Type Discipline for Authorization in Distributed Systems" author: - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Sergio Maffeis" link: "https://researchr.org/alias/sergio-maffeis" year: "2007" doi: "http://dx.doi.org/10.1109/CSF.2007.7" links: doi: "http://dx.doi.org/10.1109/CSF.2007.7" tags: - "type system" researchr: "https://researchr.org/publication/FournetGM07%3A0" cites: 0 citedby: 0 pages: "31-48" booktitle: "20th IEEE Computer Security Foundations Symposium, CSF 2007, 6-8 July 2007, Venice, Italy" publisher: "IEEE Computer Society" kind: "inproceedings" key: "FournetGM07:0" - title: "Code-Carrying Authorization" author: - name: "Sergio Maffeis" link: "https://researchr.org/alias/sergio-maffeis" - name: "Martín Abadi" link: "https://researchr.org/alias/mart%C3%ADn-abadi" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2008" doi: "http://dx.doi.org/10.1007/978-3-540-88313-5_36" links: doi: "http://dx.doi.org/10.1007/978-3-540-88313-5_36" researchr: "https://researchr.org/publication/MaffeisAFG08" cites: 0 citedby: 0 pages: "563-579" booktitle: "Computer Security - ESORICS 2008, 13th European Symposium on Research in Computer Security, Málaga, Spain, October 6-8, 2008. Proceedings" editor: - name: "Sushil Jajodia" link: "https://researchr.org/alias/sushil-jajodia" - name: "Javier Lopez" link: "https://researchr.org/alias/javier-lopez" volume: "5283" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-88312-8" kind: "inproceedings" key: "MaffeisAFG08" - title: "Secure sessions for web services" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Ricardo Corin" link: "https://researchr.org/alias/ricardo-corin" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2004" doi: "http://doi.acm.org/10.1145/1111348.1111355" links: doi: "http://doi.acm.org/10.1145/1111348.1111355" tags: - "web service" - "web services" researchr: "https://researchr.org/publication/BhargavanCFG04" cites: 0 citedby: 0 pages: "56-66" booktitle: "Proceedings of the 1st ACM Workshop On Secure Web Services, SWS 2004, Fairfax, VA, USA, October 29, 2004" editor: - name: "Vijay Atluri" link: "https://researchr.org/alias/vijay-atluri" publisher: "ACM" isbn: "1-58113-973-X" kind: "inproceedings" key: "BhargavanCFG04" - title: "From Typed Process Calculi to Source-Based Security" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2005" doi: "http://dx.doi.org/10.1007/11547662_2" links: doi: "http://dx.doi.org/10.1007/11547662_2" tags: - "rule-based" - "source-to-source" - "security" - "open-source" researchr: "https://researchr.org/publication/Gordon05%3A1" cites: 0 citedby: 0 pages: "2" booktitle: "Static Analysis, 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings" editor: - name: "Chris Hankin" link: "https://researchr.org/alias/chris-hankin" - name: "Igor Siveroni" link: "https://researchr.org/alias/igor-siveroni" volume: "3672" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-28584-9" kind: "inproceedings" key: "Gordon05:1" - title: "A Calculus for Cryptographic Protocols: The Spi Calculus" author: - name: "Martín Abadi" link: "https://researchr.org/alias/mart%C3%ADn-abadi" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1997" doi: "http://doi.acm.org/10.1145/266420.266432" links: doi: "http://doi.acm.org/10.1145/266420.266432" tags: - "protocol" researchr: "https://researchr.org/publication/AbadiG97" cites: 0 citedby: 0 pages: "36-47" booktitle: "ACM Conference on Computer and Communications Security" kind: "inproceedings" key: "AbadiG97" - title: "Guest Editors Foreword" author: - name: "Luca Aceto" link: "https://researchr.org/alias/luca-aceto" - name: "Mario Bravetti" link: "https://researchr.org/alias/mario-bravetti" - name: "Wan Fokkink" link: "http://www.cs.vu.nl/~wanf/" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2007" doi: "http://dx.doi.org/10.1016/j.jlap.2007.02.001" links: doi: "http://dx.doi.org/10.1016/j.jlap.2007.02.001" researchr: "https://researchr.org/publication/AcetoBFG07a" cites: 0 citedby: 0 journal: "Journal of Logic and Algebraic Programming" volume: "72" number: "1" pages: "1-2" kind: "article" key: "AcetoBFG07a" - title: "A Concurrent Object Calculus: Reduction and Typing" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Paul D. Hankin" link: "https://researchr.org/alias/paul-d.-hankin" year: "1998" doi: "http://www.elsevier.com/gej-ng/31/29/23/40/26/show/Products/notes/index.htt#007" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/40/26/show/Products/notes/index.htt#007" tags: - "meta-model" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/GordonH98" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "16" number: "3" pages: "248-264" kind: "article" key: "GordonH98" - title: "Concurrent Haskell" author: - name: "Simon L. Peyton Jones" link: "http://research.microsoft.com/en-us/people/simonpj/" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Sigbjorn Finne" link: "https://researchr.org/alias/sigbjorn-finne" year: "1996" doi: "http://doi.acm.org/10.1145/237721.237794" links: doi: "http://doi.acm.org/10.1145/237721.237794" tags: - "Haskell" researchr: "https://researchr.org/publication/JonesGF96" cites: 0 citedby: 0 pages: "295-308" booktitle: "POPL" kind: "inproceedings" key: "JonesGF96" - title: "Mobile Ambients" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1997" doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#017" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/35/23/show/Products/notes/index.htt#017" tags: - "mobile" researchr: "https://researchr.org/publication/CardelliG97" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "10" pages: "198-201" kind: "article" key: "CardelliG97" - title: "Notes on Nominal Calculi for Security and Mobility" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2000" doi: "http://link.springer.de/link/service/series/0558/bibs/2171/21710262.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2171/21710262.htm" tags: - "security" researchr: "https://researchr.org/publication/Gordon00%3A4" cites: 0 citedby: 0 pages: "262-330" booktitle: "Foundations of Security Analysis and Design, Tutorial Lectures [revised versions of lectures given during the IFIP WG 1.7 International School on Foundations of Security Analysis and Design, FOSAD 2000, Bertinoro, Italy, September 2000]" editor: - name: "Riccardo Focardi" link: "https://researchr.org/alias/riccardo-focardi" - name: "Roberto Gorrieri" link: "https://researchr.org/alias/roberto-gorrieri" volume: "2171" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-42896-8" kind: "inproceedings" key: "Gordon00:4" - title: "Relating operational and denotational semantics for input/output effects" author: - name: "Roy L. Crole" link: "https://researchr.org/alias/roy-l.-crole" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1999" tags: - "semantics" - "denotational semantics" - "operational semantics" researchr: "https://researchr.org/publication/CroleG99" cites: 0 citedby: 0 journal: "Mathematical Structures in Computer Science" volume: "9" number: "2" pages: "125-158" kind: "article" key: "CroleG99" - title: "Deciding validity in a spatial logic for trees" author: - name: "Cristiano Calcagno" link: "https://researchr.org/alias/cristiano-calcagno" - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2005" doi: "http://dx.doi.org/10.1017/S0956796804005404" links: doi: "http://dx.doi.org/10.1017/S0956796804005404" tags: - "logic" researchr: "https://researchr.org/publication/CalcagnoCG05" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "15" number: "4" pages: "543-572" kind: "article" key: "CalcagnoCG05" - title: "Typing a multi-language intermediate code" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Don Syme" link: "https://researchr.org/alias/don-syme" year: "2001" doi: "http://doi.acm.org/10.1145/360204.360228" links: doi: "http://doi.acm.org/10.1145/360204.360228" researchr: "https://researchr.org/publication/GordonS01" cites: 0 citedby: 0 pages: "248-260" booktitle: "Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages" series: "POPL" publisher: "Association for Computing Machinery" kind: "inproceedings" key: "GordonS01" - title: "Verifying policy-based web services security" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2008" doi: "http://doi.acm.org/10.1145/1391956.1391957" links: doi: "http://doi.acm.org/10.1145/1391956.1391957" tags: - "rule-based" - "web service" - "security" - "web services" researchr: "https://researchr.org/publication/BhargavanFG08" cites: 0 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "30" number: "6" kind: "article" key: "BhargavanFG08" - title: "Equational Properties of Mobile Ambients" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Luca Cardelli" link: "http://lucacardelli.name" year: "1999" tags: - "mobile" researchr: "https://researchr.org/publication/GordonC99" cites: 0 citedby: 0 pages: "212-226" booktitle: "Foundations of Software Science and Computation Structure, Second International Conference, FoSSaCS 99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 99, Amsterdam, The Netherlands, March 22-28, 1999, Proceed" editor: - name: "Wolfgang Thomas" link: "https://researchr.org/alias/wolfgang-thomas" volume: "1578" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-65719-3" kind: "inproceedings" key: "GordonC99" - title: "Bisimilarity as a theory of functional programming" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1995" doi: "http://www.elsevier.com/gej-ng/31/29/23/26/23/show/Products/notes/index.htt#014" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/26/23/show/Products/notes/index.htt#014" tags: - "functional programming" - "programming" researchr: "https://researchr.org/publication/Gordon95%3A0" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "1" pages: "232-252" kind: "article" key: "Gordon95:0" - title: "Automating Type Soundness Proofs via Decision Procedures and Guided Reductions" author: - name: "Don Syme" link: "https://researchr.org/alias/don-syme" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2002" doi: "http://link.springer.de/link/service/series/0558/bibs/2514/25140418.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2514/25140418.htm" tags: - "type soundness" researchr: "https://researchr.org/publication/SymeG02" cites: 0 citedby: 0 pages: "418-434" booktitle: "Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Proceedings" editor: - name: "Matthias Baaz" link: "https://researchr.org/alias/matthias-baaz" - name: "Andrei Voronkov" link: "http://www.voronkov.com/" volume: "2514" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-00010-0" kind: "inproceedings" key: "SymeG02" - title: "Secrecy and group creation" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Giorgio Ghelli" link: "https://researchr.org/alias/giorgio-ghelli" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2005" doi: "http://dx.doi.org/10.1016/j.ic.2004.08.003" links: doi: "http://dx.doi.org/10.1016/j.ic.2004.08.003" researchr: "https://researchr.org/publication/CardelliGG05" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "196" number: "2" pages: "127-155" kind: "article" key: "CardelliGG05" - title: "A Calculus for Cryptographic Protocols: The spi Calculus" author: - name: "Martín Abadi" link: "https://researchr.org/alias/mart%C3%ADn-abadi" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1999" tags: - "protocol" researchr: "https://researchr.org/publication/AbadiG99" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "148" number: "1" pages: "1-70" kind: "article" key: "AbadiG99" - title: "Mobile ambients" author: - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2000" doi: "http://dx.doi.org/10.1016/S0304-3975(99)00231-5" links: doi: "http://dx.doi.org/10.1016/S0304-3975(99)00231-5" tags: - "mobile" researchr: "https://researchr.org/publication/CardelliG00%3A0" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "240" number: "1" pages: "177-213" kind: "article" key: "CardelliG00:0" - title: "Guest Editors Foreword" author: - name: "Luca Aceto" link: "https://researchr.org/alias/luca-aceto" - name: "Mario Bravetti" link: "https://researchr.org/alias/mario-bravetti" - name: "Wan Fokkink" link: "http://www.cs.vu.nl/~wanf/" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2008" doi: "http://dx.doi.org/10.1016/j.jlap.2007.06.001" links: doi: "http://dx.doi.org/10.1016/j.jlap.2007.06.001" researchr: "https://researchr.org/publication/AcetoBFG08" cites: 0 citedby: 0 journal: "Journal of Logic and Algebraic Programming" volume: "75" number: "1" pages: "1-2" kind: "article" key: "AcetoBFG08" - title: "Secure compilation of a multi-tier web language" author: - name: "Ioannis G. Baltopoulos" link: "https://researchr.org/alias/ioannis-g.-baltopoulos" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2009" doi: "http://doi.acm.org/10.1145/1481861.1481866" links: doi: "http://doi.acm.org/10.1145/1481861.1481866" researchr: "https://researchr.org/publication/BaltopoulosG09" cites: 0 citedby: 0 pages: "27-38" booktitle: "Proceedings of TLDI 08: 2008 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009" editor: - name: "Andrew Kennedy" link: "https://researchr.org/alias/andrew-kennedy" - name: "Amal Ahmed" link: "https://researchr.org/alias/amal-ahmed" publisher: "ACM" isbn: "978-1-60558-420-1" kind: "inproceedings" key: "BaltopoulosG09" - title: "An advisor for web services security policies" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Greg O Shea" link: "https://researchr.org/alias/greg-o-shea" year: "2005" doi: "http://doi.acm.org/10.1145/1103022.1103024" links: doi: "http://doi.acm.org/10.1145/1103022.1103024" tags: - "web service" - "security" - "web services" researchr: "https://researchr.org/publication/BhargavanFGO05" cites: 0 citedby: 0 pages: "1-9" booktitle: "Proceedings of the 2nd ACM Workshop On Secure Web Services, SWS 2005, Fairfax, VA, USA, November 11, 2005" editor: - name: "Ernesto Damiani" link: "https://researchr.org/alias/ernesto-damiani" - name: "Hiroshi Maruyama" link: "https://researchr.org/alias/hiroshi-maruyama" publisher: "ACM" isbn: "1-59593-234-8" kind: "inproceedings" key: "BhargavanFGO05" - title: "Stack inspection: Theory and variants" author: - name: "Cédric Fournet" link: "https://researchr.org/alias/c%C3%A9dric-fournet" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "2003" doi: "http://doi.acm.org/10.1145/641909.641912" links: doi: "http://doi.acm.org/10.1145/641909.641912" researchr: "https://researchr.org/publication/FournetG03" cites: 0 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "25" number: "3" pages: "360-399" kind: "article" key: "FournetG03" - title: "Service Combinators for Farming Virtual Machines" author: - name: "Karthikeyan Bhargavan" link: "https://researchr.org/alias/karthikeyan-bhargavan" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Iman Narasamdya" link: "https://researchr.org/alias/iman-narasamdya" year: "2008" doi: "http://dx.doi.org/10.1007/978-3-540-68265-3_3" links: doi: "http://dx.doi.org/10.1007/978-3-540-68265-3_3" researchr: "https://researchr.org/publication/BhargavanGN08" cites: 0 citedby: 0 pages: "33-49" booktitle: "Coordination Models and Languages, 10th International Conference, COORDINATION 2008, Oslo, Norway, June 4-6, 2008. Proceedings" editor: - name: "Doug Lea" link: "https://researchr.org/alias/doug-lea" - name: "Gianluigi Zavattaro" link: "https://researchr.org/alias/gianluigi-zavattaro" volume: "5052" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-68264-6" kind: "inproceedings" key: "BhargavanGN08" - title: "Authenticity by Typing for Security Protocols" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Alan Jeffrey" link: "https://researchr.org/alias/alan-jeffrey" year: "2001" doi: "http://csdl.computer.org/comp/proceedings/csfw/2001/1146/00/11460145abs.htm" links: doi: "http://csdl.computer.org/comp/proceedings/csfw/2001/1146/00/11460145abs.htm" tags: - "protocol" - "security" researchr: "https://researchr.org/publication/GordonJ01%3A0" cites: 0 citedby: 0 pages: "145-159" booktitle: "14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada" publisher: "IEEE Computer Society" isbn: "0-7695-1146-5" kind: "inproceedings" key: "GordonJ01:0" - title: "Bisimilarity for a First-Order Calculus of Objects with Subtyping" author: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Gareth D. Rees" link: "https://researchr.org/alias/gareth-d.-rees" year: "1996" doi: "http://doi.acm.org/10.1145/237721.237807" links: doi: "http://doi.acm.org/10.1145/237721.237807" tags: - "meta-model" - "subtyping" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/GordonR96" cites: 0 citedby: 0 pages: "386-395" booktitle: "POPL" kind: "inproceedings" key: "GordonR96" - title: "Semantic subtyping with an SMT solver" author: - name: "Gavin M. Bierman" link: "https://researchr.org/alias/gavin-m.-bierman" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "David E. Langworthy" link: "https://researchr.org/alias/david-e.-langworthy" year: "2010" doi: "http://doi.acm.org/10.1145/1863543.1863560" abstract: "We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variety of typing idioms; for example, intersection, union, negation, singleton, nullable, variant, and algebraic types are all derivable. We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on an SMT solver to compute subtyping efficiently. Moreover, interpreting types as formulas allows us to call the SMT solver at run-time to compute instances of types. " links: doi: "http://doi.acm.org/10.1145/1863543.1863560" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/BiermanGHL10" tags: - "semantics" - "model checking" - "meta-model" - "modeling language" - "refinement" - "language modeling" - "testing" - "subtyping" - "type checking" - " algebra" - "logic" - "type theory" - "Meta-Environment" - "domain-specific language" researchr: "https://researchr.org/publication/BiermanGHL10" cites: 0 citedby: 0 pages: "105-116" booktitle: "Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010" editor: - name: "Paul Hudak" link: "https://researchr.org/alias/paul-hudak" - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-60558-794-3" kind: "inproceedings" key: "BiermanGHL10" - title: "A Bisimulation Method for Cryptographic Protocols" author: - name: "Martín Abadi" link: "http://users.soe.ucsc.edu/~abadi/home.html" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" year: "1998" doi: "http://link.springer.de/link/service/series/0558/bibs/1381/13810012.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1381/13810012.htm" tags: - "protocol" researchr: "https://researchr.org/publication/AbadiG98" cites: 0 citedby: 0 pages: "12-26" booktitle: "Programming Languages and Systems - ESOP 98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings" editor: - name: "Chris Hankin" link: "https://researchr.org/alias/chris-hankin" volume: "1381" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-64302-8" kind: "inproceedings" key: "AbadiG98" - title: "Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings" year: "2003" tags: - "e-science" researchr: "https://researchr.org/publication/fossacs%3A2003" cites: 0 citedby: 0 booktitle: "Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings" conference: "fossacs" editor: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" volume: "2620" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-00897-7" kind: "proceedings" key: "fossacs:2003" - title: "Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings" year: "2010" doi: "http://dx.doi.org/10.1007/978-3-642-11957-6" links: doi: "http://dx.doi.org/10.1007/978-3-642-11957-6" tags: - "programming languages" - "programming" researchr: "https://researchr.org/publication/esop-2010" cites: 0 citedby: 0 booktitle: "Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings" conference: "ESOP" editor: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" volume: "6012" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-11956-9" kind: "proceedings" key: "esop-2010" - title: "Proceedings of the 2006 ACM workshop on Formal methods in security engineering, FMSE 2006, Alexandria, VA, USA, November 3, 2006" year: "2006" tags: - "security" researchr: "https://researchr.org/publication/ccs%3A2006fmse" cites: 0 citedby: 0 booktitle: "Proceedings of the 2006 ACM workshop on Formal methods in security engineering, FMSE 2006, Alexandria, VA, USA, November 3, 2006" editor: - name: "Marianne Winslett" link: "https://researchr.org/alias/marianne-winslett" - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" - name: "David Sands" link: "https://researchr.org/alias/david-sands" publisher: "ACM" isbn: "1-59593-550-9" kind: "proceedings" key: "ccs:2006fmse"