Please also consult Andre Scedrov's dblp Computer Science Bibliography, Google Scholar, and MathSciNet entries.
Time-Bounded Resilience (with
Tajana Ban Kirigin, Jesse Comer, Max Kanovich, and Carolyn Talcott).
In: K. Ogata and N. Martí-Oliet, eds.,
Rewriting Logic and Its Applications. 15th International Workshop,
WRLA 2024, Luxembourg, April 6-7, 2024.
Springer LNCS, Volume 14953. Springer, Cham,
pp. 22 - 44. First Online: 02 August 2024.
[DOI].
Helle Hvid Hansen, Andre Scedrov, and Ruy J.G.B. de Queiroz, eds., Logic,
Language, Information, and Computation. 29th International Workshop,
WoLLIC 2023, Halifax, NS, Canada, July 11-14, 2023, Proceedings.
Springer Lecture Notes in Computer Science, Volume 13923, Springer Cham,
xxxviii + 395 pp. Published 30 August 2023.
[DOI].
Explorations in Subexponential Non-associative Non-commutative Linear Logic. (with Eben Blaisdell, Max Kanovich, Stepan L.
Kuznetsov, and Elaine Pimentel).
In: M. Moortgat and M. Sadrzadeh, eds.,
Proceedings Modalities in substructural logics: Applications at the
interfaces of logic,
language and computation, Ljubljana, Slovenia, August 7-8, 2023.
Electronic Proceedings in Theoretical Computer Science EPTCS 381, pp. 4 - 19.
Published: 7th August 2023.
[DOI].
On the Formalization and Computational Complexity of Resilience Problems for
Cyber-Physical Systems (with Musab A. Alturki, Max Kanovich,
Tajana Ban Kirigin, Vivek Nigam, and Carolyn Talcott).
In: H. Seidl, Z. Liu, and C. Pasareanu, eds.,
Theoretical Aspects of Computing - ICTAC 2022,
19th International Colloquium, Tbilisi, Georgia,
September 27-29, 2022, Proceedings.
Springer LNCS Volume 13572, Springer, pp. 96 - 113.
First Online 03 October 2022.
[DOI].
Language Models for Some Extensions of the Lambek Calculus
(with Max Kanovich and Stepan Kuznetsov). Information and Computation,
Volume 287, September 2022, 104760. Special Issue: Selected Papers from WoLLIC
2019, the 26th Workshop on Logic, Language, Information and Computation.
Edited by Ruy J.G.B. de Queiroz.
[DOI].
Non-associative, non-commutative multi-modal linear logic (with Eben
Blaisdell, Max Kanovich, Stepan L. Kuznetsov, and Elaine Pimentel).
In: J. Blanchette, L. Kovacs, and D. Pattinson, eds.,
Automated Reasoning, 11th International Joint Conference, IJCAR 2022,
Haifa, Israel, August 8-10, 2022, Proceedings. Springer LNAI Volume 13385,
Springer, pp. 449 - 467. First Online 01 August 2022.
[DOI].
On the Security and Complexity of Periodic Systems
(with Musab A. Alturki,
Tajana Ban Kirigin, Max Kanovich, Vivek Nigam, and Carolyn Talcott).
SN Computer Science 3, 356 (2022). Published online 02 July 2022.
[SharedIt].
[DOI].
Extended abstract under the title "On Security Analysis of Periodic Systems:
Expressiveness and Complexity" in: P. Mori, G. Lenzini, and S. Furnell, eds.,
Proceedings of the 7th International Conference on Information
Systems Security and Privacy - Volume 1: ICISSP 2021, February 11-13,
2021, SCITEPRESS Digital Library, 2021, pp. 43 - 54.
On the Complexity of Verification of Time-Sensitive Distributed
Systems (with Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, and Carolyn
Talcott).
In: D. Dougherty, J. Meseguer, S.A. Mödersheim, and P. Rowe, eds.,
Protocols, Strands, and Logic. Essays Dedicated to Joshua Guttman on the
Occasion of his 66.66th Birthday.
Springer LNCS Volume 13066, Springer-Verlag, pp. 251 - 275. First Online
19 November 2021.
[DOI].
Decidable Fragments of Calculi used in CatLog
(with Max I. Kanovich, Stepan G. Kuznetsov, and Stepan L. Kuznetsov).
In: R. Loukanova, ed.,
Natural Language Processing in Artificial Intelligence - NLPinAI 2021,
Springer Studies in Computational Intelligence, Volume 999, pp. 1 - 24. First
online 2 November 2021.
[DOI].
Resource and Timing Aspects of Security Protocols
(with Abraão Aires Urquiza, Musab A. Alturki, Max Kanovich,
Tajana Ban Kirigin, Vivek Nigam, and Carolyn Talcott). Journal of Computer
Security 29(3) (2021) 299 - 340.
[DOI].
Extended abstract under the title
"Resource-Bounded Intruders in Denial of Service Attacks"
in: S. Delaune and L. Jia, eds.,
32nd IEEE Computer Security Foundations Symposium (CSF 2019),
Hoboken, New Jersey, USA, June 2019, IEEE Computer Society Press, 2019,
pp. 382 - 396.
The Multiplicative-Additive Lambek Calculus with Subexponential and Bracket
Modalities (with Max Kanovich and Stepan Kuznetsov). Journal of Logic,
Language and Information 30 (2021) 31 - 88.
[DOI].
Extended abstract under the title
"Undecidability of a newly proposed calculus for CatLog3"
in: R. Bernardi, G. Kobele, and S. Pogodalla, eds.,
The 24th Conference on Formal Grammar (FG 2019),
Riga, Latvia, August 2019, Springer LNCS Volume 11668, Springer-Verlag, 2019,
pp. 67 - 83.
Soft Subexponentials and Multiplexing
(with Max Kanovich, Stepan Kuznetsov, and Vivek Nigam).
In: N. Peltier and V. Sofronie-Stokkermans, eds.,
Automated Reasoning, 10th International Joint
Conference, IJCAR 2020, July 1-4, 2020, Proceedings,
Part I, Springer LNAI Volume 12166, Springer-Verlag, 2020,
pp. 500 - 517.
[DOI].
Reconciling Lambek's
restriction, cut-elimination, and substitution in the presence of exponential
modalities
(with Max Kanovich and Stepan Kuznetsov).
Journal of Logic and Computation 30(1) (2020) 239 - 256.
[DOI].
Extended abstract under the title "On Lambek's restriction
in the presence of exponential modalities" in: S. Artemov and A. Nerode, eds.,
Symposium
on Logical Foundations Of Computer Science (LFCS 2016),
Deerfield Beach, Florida, USA, January 2016. Springer LNCS Volume 9537,
Springer-Verlag, 2016, pp. 146 - 158.
Subexponentials in non-commutative linear logic
(with Max Kanovich, Stepan Kuznetsov, and Vivek Nigam).
Mathematical Structures in Computer Science 29(8) (2019) 1217 - 1249.
[DOI].
A special issue on structural proof theory, automated reasoning and
computation in celebration of Dale Miller's 60th birthday.
The Complexity of
Multiplicative-Additive Lambek Calculus: 25 Years Later
(with Max Kanovich and Stepan Kuznetsov).
In: R. Iemhoff, M. Moortgat, and R. de Queiroz, eds.,
26th Workshop on Logic,
Language, Information and Computation (WoLLIC 2019),
Utrecht, The Netherlands, July 2019, Springer LNCS Volume 11541,
Springer-Verlag, 2019, pp. 356 - 372.
A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of
Security Protocols
(with Musab A. Alturki, Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, and
Carolyn Talcott).
In: J.D. Guttman et al., eds., Foundations of Security, Protocols,
and Equational Reasoning. Essays Dedicated to Catherine A. Meadows.
Springer LNCS Volume 11565, Springer-Verlag, 2019, pp. 192 - 213.
Automated Analysis of Cryptographic Assumptions in Generic Group Models
(with G. Barthe, E. Fagerholm, D. Fiore, J.C. Mitchell and B. Schmidt).
Journal of Cryptology 32(2) (2019) 324-360.
[DOI].
Extended abstract in: J. Garay and R. Gennaro, eds.,
34th
International Cryptology Conference (CRYPTO 2014), Proceedings, Part I,
Santa Barbara, California, USA, August 2014. Springer LNCS Volume 8616,
Springer-Verlag, 2014, pp. 95 - 112.
ePrint
Archive: Report 2014/458.
Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn
Family of Protocols
(with Musab A. Alturki, Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, and
Carolyn Talcott).
In: A. Rashid and N.O. Tippenhauer, eds.,
Proceedings of the 2018
ACM Workshop on Cyber-Physical Systems Security & Privacy (CPS-SPC 2018),
Toronto, Ontario, Canada, October 19, 2018, ACM, New York, NY, 2018,
pp. 60 - 71.
Bracket induction for Lambek calculus with bracket modalities
(with Glyn Morrill, Stepan Kuznetsov, and Max Kanovich).
In: A. Foret et al., eds.,
The 23rd Conference on Formal Grammar
(FG 2018),
Sofia, Bulgaria, August 11-12, 2018. Springer LNCS Volume 10950,
Springer-Verlag, 2018, pp. 84 - 101.
A Logical Framework with Commutative and Non-Commutative
Subexponentials
(with Max Kanovich, Stepan Kuznetsov, and Vivek Nigam).
In: D. Galmiche et al., eds.,
9th International Joint
Conference on Automated Reasoning (IJCAR 2018),
Oxford, UK, July 14-17, 2018.
Springer LNCS Volume 10900,
Springer-Verlag, 2018, pp. 228 - 245.
V. Itsykson, A. Scedrov, and V. Zakharov, eds.,
Tools
and Methods of Program Analysis. 4th International Conference,
TMPA 2017,
Moscow, Russia, March 3-4, 2017.
Communications in
Computer and Information Science, Volume 779,
Springer International Publishing, 2018, xviii + 209 pp.
Undecidability of the Lambek Calculus with Subexponential and Bracket
Modalities
(with Max Kanovich and Stepan Kuznetsov). In: R. Klasing and M. Zeitoun, eds.,
21st International Symposium on
Fundamentals of Computation Theory (FCT 2017),
Bordeaux, France, September 11-13, 2017. Springer LNCS Volume 10472,
Springer-Verlag, 2017, pp. 326 - 340.
Technical report in
arXiv:1608.04020.
A polynomial-time algorithm for the Lambek calculus with brackets of
bounded order
(with Max Kanovich, Stepan Kuznetsov, and Glyn Morrill).
In: D. Miller, ed.,
Second International Conference on
Formal Structures for Computation and Deduction (FSCD 2017),
Oxford, UK, September 3-9, 2017. Leibniz International Proceedings in
Informatics (LIPIcs) Volume 84, Schloss Dagstuhl - Leibniz Center for
Informatics,, 2017, pp. 22:1 - 22:17.
Technical report in
arXiv:1705.00694.
Time, Computational Complexity, and Probability in the Analysis of Distance-Bounding Protocols
(with M. Kanovich, T. Ban Kirigin, V. Nigam, and C. Talcott). J. of Computer
Security 25(6) (2017) 585-630.
[.pdf].
Extended abstract under the title "Discrete vs. Dense Times in the
Verification of Cyber-Physical Security Protocols"
in: R. Focardi and A. Myers, eds.,
4th Conference on
Principles of Security and Trust (POST 2015),
London, UK, April, 2015. Springer LNCS Volume 9036,
Springer-Verlag, 2015, pp. 259 - 279.
A Rewriting Framework and Logic for Activities Subject to Regulations
(with M.I. Kanovich, T. Ban Kirigin, V. Nigam, C.L. Talcott, and
R. Perovic). Mathematical Structures in Computer Science 27(3) (2017) 332-375.
Published online 02 June 2015
[DOI].
Extended abstract under the title
"A Rewriting Framework for Activities Subject to Regulations"
in: A. Tiwari, ed.,
23-rd International
Conference on Rewriting Techniques and Applications (RTA 2012).
Nagoya, Japan, May 28 -June 2, 2012.
Leibniz International Proceedings in
Informatics Volume 15, Schloss Dagstuhl - Leibniz Center for
Informatics, 2012, pp. 305 - 322.
[.pdf].
Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds
(with G. Barthe, E. Fagerholm, D. Fiore, B. Schmidt, and M. Tibouchi).
IET Information Security 10(6) (2016) 358-371.
Published online 26 April 2016
[DOI].
Extended abstract in: J. Katz, ed.,
18th IACR International Conference on Practice and Theory of Public-Key Cryptography (PKC 2015),
Gaithersburg, Maryland, USA, March 30 - April 1, 2015.
Springer LNCS Volume 9020, Springer-Verlag, 2015, pp. 355 - 376.
ePrint
Archive: Report 2015/019.
Timed Multiset Rewriting and the Verification of Time-Sensitive
Distributed Systems
(with M. Kanovich, T. Ban Kirigin, V. Nigam, and C. Talcott). In:
M. Fraenzle and N. Markey, eds.,
Formal
Modeling and Analysis of Timed Systems, 14th International Conference,
FORMATS 2016, Quebec, QC, Canada, August 24-26, 2016.
Springer LNCS Volume 9884, Springer-Verlag, 2016, pp. 228 - 244.
Technical report in
arXiv:1606.07886.
Undecidability of the Lambek calculus with a relevant modality
(with Max Kanovich and Stepan Kuznetsov). In: A. Foret et al., eds.,
Formal
Grammar, 20th and 21st International Conferences, FG 2015, Barcelona,
Spain, August 2015, Revised Selected Papers. FG 2016, Bozen, Italy,
August 2016, Proceedings. Springer LNCS Volume 9804,
Springer-Verlag, 2016, pp. 240 - 256. Preliminary version in
arXiv:1601.06303.
Bounded Memory Protocols
(with M. Kanovich, T. Ban Kirigin, and V. Nigam).
Computer Languages, Systems and Structures 40(3-4) (2014) 137 - 154
[.pdf].
Extended abstract under the title "Bounded Memory Protocols and Progressing
Collaborative Systems" in: J. Crampton, S. Jajodia and K. Mayes, eds.,
The 18th European Symposium on
Research in Computer Security (ESORICS 2013),
Egham, UK, September 2013. Springer LNCS Volume 8134,
Springer-Verlag, 2013, pp. 309 - 326.
Bounded Memory Dolev-Yao Adversaries in Collaborative Systems
(with M. Kanovich, T. Ban Kirigin, and V. Nigam).
Information and Computation 238 (2014) 233-261.
Extended abstract in: P. Degano et al., eds.,
The 7th International Workshop on
Formal Aspects of Security & Trust (FAST2010), Pisa, Italy, September
2010. Springer LNCS Volume 6561, Springer-Verlag, 2011, pp. 18-33.
[.pdf].
A Reduction-based Approach Towards Scaling Up Formal Analysis of Internet Configurations
(with A. Wang, A.J.T. Gurney, X. Han, J. Cao, B. Thau Loo, and C. Talcott).
In: G. Bianchi, Y. Fang, and X. Shen, eds.,
33rd Annual IEEE
International Conference on Computer Communications (INFOCOM 2014),
Toronto, Canada, April 27 - May 2, 2014, IEEE, 2014, pp. 637 - 645.
When Not All Bits Are Equal: Worth-Based Information Flow
(with M.S. Alvim and F.B. Schneider).
In: M. Abadi and S. Kremer, eds.,
3rd Conference on Principles
of Security and Trust (POST 2014),
Grenoble, France, April 2014. Springer LNCS Volume 8414,
Springer-Verlag, 2014, pp. 120 - 139.
Technical Report.
Automated Synthesis of Reactive Controllers for Software-Defined Networks
(with A. Wang, S. Moarref, B. Thau Loo, and U. Topcu).
In:
3rd International Workshop on Rigorous Protocol Engineering
(WRiPE 2013), 21st IEEE International Conference on Network Protocols
(ICNP 2013), Goettingen, Germany, October 2013.
IEEE Xplore Digital Library 2013.
[.pdf].
FSR: Formal Analysis and Implementation Toolkit for Safe
Inter-domain Routing
(with A. Wang, L. Jia, W. Zhou, Y. Ren, B. Thau Loo, J. Rexford,
V. Nigam, and C. Talcott).
IEEE/ACM Transactions on Networking 20(6) (2012) 1814-1827.
Reduction-based analysis of BGP systems with BGPVerif
(with A. Wang, A.J.T. Gurney, X. Han, J. Cao, C.L. Talcott, and B. Thau Loo).
Demo in: L. Eggert, J. Ott, V.N. Padmanabhan, G. Varghese, eds.,
ACM SIGCOMM 2012 Conference on Applications, Technologies,
Architectures, and Protocols for Computer Communication.
Helsinki, Finland, August 2012. ACM Press, 2012, pp. 89-90.
[.pdf].
Brief Announcement: A Calculus of Policy-Based Routing Systems
(with A. Wang, C.L. Talcott, A.J.T. Gurney, and B. Thau Loo).
In: A. Panconesi, ed.,
31-st Annual ACM SIGACT-SIGOPS
Symposium on Principles of Distributed Computing (PODC 2012).
Madeira, Portugal, July 2012. ACM Press, 2012, pp. 343 - 344.
[.pdf].
Reduction-based Formal Analysis BGP Instances
(with A. Wang, C.L. Talcott, A.J.T. Gurney, and B. Thau Loo).
In: C. Flanagan and B. Koenig, eds.,
18th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS 2012). Tallinn, Estonia, March 2012.
Springer LNCS Volume 7214, Springer-Verlag, 2012, pp. 283 - 298.
Technical Report.
Declarative privacy policy: Finite models and
attribute-based encryption
(with P.E. Lam, J.C. Mitchell, S. Sundaram, and F. Wang). In: C.C. Yang, ed.,
2nd ACM SIGHIT International Health Informatics Symposium (IHI 2012).
Miami, Florida, USA, January 2012. ACM Digital Library, 2012,
pp. 323-332.
[.pdf].
Towards an Automated Assistant for Clinical Investigations
(with V. Nigam, T. Ban Kirigin, C. Talcott, M. Kanovich, and R. Perovic).
In: C.C. Yang, ed.,
2nd ACM SIGHIT International Health Informatics Symposium (IHI 2012).
Miami, Florida, USA, January 2012. ACM Digital Library, 2012,
pp. 773-778.
[.pdf].
Maintaining Distributed Logic Programs Incrementally
(with V. Nigam, L. Jia, and B. Thau Loo).
Computer Languages, Systems and Structures 38 (2012) 158-180.
Extended abstract in: M. Hanus, ed.,
13th International ACM SIGPLAN
Symposium on Principles and Practice of Declarative Programming (PPDP 2011).
Odense, Denmark, July 2011. ACM Press, 2011, pp. 125-136.
[.pdf].
Analyzing BGP Instances in Maude
(with A. Wang, C.L. Talcott, L. Jia, and B. Thau Loo).
In: R. Bruni and J. Dingel, eds., Formal Techniques for Distributed Systems.
Joint 13th IFIP International Conference on Formal Methods
for Open Object-based Distributed Systems and
31st IFIP International Conference on FORmal TEchniques for Networked and
Distributed Systems (FMOODS & FORTE 2011), Reykjavik, Iceland, June 2011,
Proceedings. Springer LNCS Volume 6722, Springer-Verlag, 2011, pp. 334 - 348.
Technical report
[.pdf].
Cryptographically Sound Security Proofs for Basic and Public-Key
Kerberos
(with M. Backes, I. Cervesato, A.D. Jaggard, and J.-K. Tsay).
International Journal of Information Security 10(2) (2011) 107-133
[.pdf]. Extended astract in:
D. Gollmann, J. Meier, and A. Sabelfeld, eds.,
"Computer Security - ESORICS 2006,
11-th European Symposium On Research In Computer Security",
Hamburg, Germany, September 2006. Springer LNCS
Volume 4189, Springer-Verlag, 2006, pp. 362 - 383.
Collaborative Planning with Confidentiality
(with M. Kanovich and P. Rowe). Journal of Automated Reasoning
46 (3-4) (2011) 389-421.
[.pdf].
Extended abstract under the title
"Collaborative Planning with Privacy"
in: A. Sabelfeld, ed.,
"20-th IEEE Computer Security Foundations Symposium (CSF)",
Venice, Italy, July 2007. IEEE Computer Society Press, 2007, pp. 265-278.
An Operational Semantics for Network Datalog
(with V. Nigam, L. Jia, A. Wang, and B. Thau Loo).
In: B. Mueller (Farwer), ed.,
Third
International Workshop on Logics, Agents, and Mobility (LAM'10).
[.pdf].
Policy Compliance in Collaborative Systems
(with M. Kanovich and P. Rowe).
[.pdf].
In: J. Mitchell, ed.,
"22-nd IEEE Computer Security Foundations Symposium (CSF)",
Port Jefferson, New York, USA, July 2009. IEEE Computer Society Press, 2009,
pp. 218-233.
Refining Computationally Sound
Mechanized Proofs for Kerberos
(with B. Blanchet, A.D. Jaggard, J. Rao, and J.-K. Tsay).
In: R. Kuesters, ed.,
"Workshop on Formal and Computational Cryptography (FCC 2009)",
Port Jefferson, New York, USA, July 2009.
Relating State-Based and Process-Based Concurrency through Linear
Logic
(with I. Cervesato). Information and Computation 207(10) (2009) 1044-1077.
[.pdf].
Extended abstract in: R. de Queiroz and G. Mints, eds.,
"13-th Workshop on Logic, Language, Information and Computation",
Stanford, California, July 2006. ENTCS Volume 165, Elsevier, 2006,
pp. 145-176.
Soundness and completeness of formal encryption: The cases of key-cycles and
partial information leakage
(with P. Adão, G. Bana, and J. Herzog). Journal of Computer Security
17(5) (2009) 737-797.
[.pdf]. Extended abstract under the title
"Soundness of formal encryption in the presence of key-cycles"
in: S. De Capitani di Vimercati, P. Syverson, and D. Gollmann, eds.,
"
10-th European Symposium on Research in Computer Security
(ESORICS 2005)",
Milan, Italy, September 2005. Springer LNCS Volume 3679,
Springer-Verlag, 2005, pp. 374-396.
Analysis of EAP-GPSK Authentication Protocol
(with J.C. Mitchell, P. Rowe, and A. Roy).
In: S. Bellovin and R. Gennaro, eds.,
"6-th International Conference on Applied Cryptography and Network Security
(ACNS'08)",
New York, June 2008. Springer LNCS Volume 5037, Springer-Verlag, 2008,
pp. 309 - 327.
[.pdf].
Computationally Sound
Mechanized Proofs for Basic and Public-Key Kerberos
(with B. Blanchet, A.D. Jaggard, and J.-K. Tsay).
In: V. Gligor and M. Abe, eds.,
"ACM Symposium on Information, Computer and
Communications Security (ASIACCS '08)",
Tokyo, Japan, March 2008. ACM Press, 2008, pp. 87-99.
ACM Portal link.
Key-dependent Message Security under Active Attacks -
BRSIM/UC-Soundness of Dolev-Yao-style Encryption with Key Cycles
(with M. Backes and B. Pfitzmann).
Journal of Computer Security 16(5) (2008) 497-530.
Extended abstract under the title
"Key-dependent Message Security under Active Attacks -
BRSIM/UC-Soundness of Symbolic Encryption with Key Cycles"
in: A. Sabelfeld, ed.,
"20-th IEEE Computer Security Foundations Symposium (CSF)",
Venice, Italy, July 2007. IEEE Computer Society Press, 2007, pp. 112-124.
Preliminary version in:
Cryptology ePrint Archive: Report 2005/421.
Breaking and fixing public-key Kerberos
(with I. Cervesato, A.D. Jaggard, J.-K. Tsay, and C. Walstad).
Information and Computation 206(2-4) (2008) 402-424.
Extended abstract in: M. Okada, I. Satoh, eds.,
Advances in Computer Science - ASIAN 2006,
Tokyo, Japan, December 2006. Springer LNCS Volume 4435,
Springer-Verlag, 2008. Preliminary version
[.pdf].
The work of Dean Rosenzweig: A Tribute to a Scientist and an Innovator.
In:
"Foundations of Software Engineering.
6-th Joint Meeting
of the European Software Engineering Conference and the 14-th ACM SIGSOFT
Symposium on Foundations of Software Engineering (ESEC/FSE 2007)",
Dubrovnik, Croatia, September 2007, ACM Press, 2007, pp. 371-374.
ACM Portal link.
Software Quality and Infrastructure Protection for Diffuse Computing
(with J. Feigenbaum, J.Y. Halpern, P.D. Lincoln, J.C. Mitchell, J.M.
Smith, and P. Syverson. In: C. Wang, S. King et al., eds.,
"Information Security Research", Wiley, 2007. ISBN: 978-0-471-78756-3.
Formal Analysis of Kerberos 5
(with F. Butler, I. Cervesato, A.D. Jaggard, and C. Walstad).
[.pdf].
Theoretical Computer Science 367(1-2) (2006) 57-87.
Games and the Impossibility of Realizable Ideal Functionality
(with A. Datta, A. Derek, J.C. Mitchell, and A. Ramanathan).
In: S. Halevi and T. Rabin, eds.,
"
3-rd Theory of Cryptography Conference
(TCC 2006)",
New York, NY, March 2006. Springer LNCS Volume 3876,
Springer-Verlag, 2006, pp. 360-379.
Revised version in
Cryptology ePrint Archive: Report 2005/211.
A probabilistic polynomial-time process calculus for the analysis
of cryptographic protocols
(with J.C. Mitchell, A. Ramanathan, and V. Teague).
Theoretical Computer Science 353 (2006) 118-164.
[.pdf]
[.ps]
[.ps.gz]
Computational and information-theoretic
soundness and completeness of formal encryption
(with P. Adão and G. Bana). In: J. Guttman, ed.,
"
18-th IEEE Computer Security Foundations Workshop (CSFW)",
Aix-en-Provence, France, June 2005. IEEE Computer Society Press,
2005, pp. 170-184.
[.pdf]
[.ps]
[.ps.gz]
Specifying Kerberos 5 cross-realm authentication
(with I. Cervesato, A. Jaggard, and C. Walstad). In:
C. Meadows, ed.,
"Proceedings of the 2005 workshop on Issues in the theory of security
(WITS'05)", Long Beach, California, January 2005.
ACM Digital Library, ACM Press, New York, 2005, pp. 12-26.
[.pdf]
Formal analysis of multi-party contract signing
(with R. Chadha and S. Kremer). Journal of Automated Reasoning
36(1-2) (2006) pp. 39-83.
[.pdf]
[.ps]
[.ps.gz]
Preliminary report in:
R. Focardi, ed.,
"
17-th IEEE Computer Security
Foundations Workshop (CSFW)",
Pacific Grove, California, June 2004.
IEEE Computer Society Press, 2004, pp. 266-279.
[.pdf]
[.ps]
[.ps.gz]
A formal analysis of some properties of Kerberos 5 using MSR
(with F. Butler, I. Cervesato, and A. Jaggard).
University of Pennsylvania Department of Computer and Information Science
Technical Report MS-CIS-04-04, April 2004, 59 pages.
[.pdf]
[.ps]
[.ps.gz]
Verifying Confidentiality and Authentication in Kerberos 5
(with F. Butler, I. Cervesato, and A. Jaggard).
In: K. Futatsugi, F. Mizoguchi, N. Yonezaki, eds.,
"Software Security - Theories and Systems
Second Mext-NSF-JSPS International Symposium,
ISSS 2003, Tokyo, Japan, November 4-6, 2003"
Springer LNCS Volume 3233, Springer-Verlag, 2004, pp. 1-24.
Probabilistic bisimulation and equivalence for security analysis
of network protocols
(with A. Ramanathan, J. Mitchell, and V. Teague). In:
I. Walukiewicz, ed.,
"Foundations of Software Science and
Computation Structures, 7-th International Conference,
FOSSACS 2004",
Springer LNCS Volume 2987, Springer-Verlag, 2004, pp. 468-483.
Full, revised version
[.pdf]
[.ps]
[.ps.gz]
Composition of cryptographic protocols
in a probabilistic polynomial-time process calculus
(with P. Mateus and J.C. Mitchell). In: R. Amadio and D. Lugiez, eds.,
"CONCUR 2003 - Concurrency Theory,
14-th International Conference, Marseille, France, September 2003",
Springer LNCS Volume 2761, Springer-Verlag, 2003, pp. 327-349.
[.pdf]
[.ps]
[.ps.gz]
Contract signing, optimism, and advantage
(with R. Chadha, J.C. Mitchell, and V. Shmatikov).
Journal of Logic and Algebraic Programming,
Special issue on Modelling and Verification of Cryptographic Protocols,
R.M. Amadio, ed., 64(2), 2005, pp. 189-218.
[.pdf]
[.ps]
[.ps.gz]
Extended abstract in: R. Amadio and D. Lugiez, eds.,
"CONCUR 2003 - Concurrency Theory,
14-th International Conference, Marseille, France, September 2003",
Springer LNCS Volume 2761, Springer-Verlag, 2003, pp. 366-382.
A revised comparison between strand spaces and multiset rewriting
for security protocol analysis
(with I. Cervesato, N.A. Durgin, P.D. Lincoln, and J.C. Mitchell).
Journal of Computer Security 13(2) (2005) 265-316.
[.pdf]
Extended abstract
in: M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, eds.,
"Software Security - Theories and Systems. Mext-NSF-JSPS International
Symposium, ISSS 2002, Tokyo, Japan, November 8-10, 2002, Revised Papers",
Springer LNCS Volume 2609, Springer-Verlag, 2003, pp. 356-383.
Revised and expanded version
of the preliminary report under the title
"Relating strands and multiset rewriting for security protocol analysis"
from: P. Syverson, ed.,
"13-th IEEE Computer Security Foundations Workshop,
Cambridge, England, July, 2000", IEEE Computer Society Press,
2000, pp. 35-51.
A formal analysis of some properties of Kerberos 5 using MSR
(with F. Butler, I. Cervesato, and A. Jaggard). In:
S. Schneider, ed.,
"15-th IEEE Computer Security Foundations Workshop,
Cape Breton, Nova Scotia, Canada, June, 2002", IEEE Computer Society Press,
2002, pp. 175-190. Preliminary version
[.pdf]
[.ps]
[.ps.gz].
Multiset rewriting and the complexity of bounded security protocols
(with N. Durgin, P. Lincoln, and J. Mitchell).
Journal of Computer Security 12(2), 2004, pp. 247-311.
[.pdf]
[.ps]
[.ps.gz].
Preliminary report under the title
Undecidability of bounded security protocols
in:
"Workshop on Formal Methods and Security Protocols (FMSP'99)",
The 1999 Federated Logic Conference (FLoC'99),
Trento, Italy, July, 1999.
A probabilistic polynomial-time calculus
for analysis of cryptographic protocols
(with J. Mitchell, A. Ramanathan, and V. Teague).
Preliminary report, 2001, 25 pages.
[.pdf]
[.ps]
[.ps.gz].
In: S. Brookes, M. Mislove, eds.,
"17-th Annual Conference on the Mathematical Foundations
of Programming Semantics", Arhus, Denmark, 2001,
Electronic Notes in Theoretical Computer Science, Volume 45 (2001).
Inductive methods and contract-signing protocols
(with R. Chadha and M.I. Kanovich). In:
P. Samarati, ed.,
"8-th ACM Conference on Computer and Communications Security,
Philadelphia, Pennsylvania, November, 2001",
ACM Press, 2001, pp. 176-185. Extended version
[.pdf]
[.ps]
[.ps.gz].
Interpreting strands in linear logic
(with I. Cervesato, N.A. Durgin, and M.I. Kanovich). In:
"2000 Workshop on Formal Methods and Computer Security",
12th International Conference on Computer Aided Verification
(CAV 2000) Satellite Workshop, Chicago, Illinois, July,
2000.
Probabilistic polynomial-time equivalence and security analysis
(with P.D. Lincoln, J.C. Mitchell, and M. Mitchell). In: J.M. Wing,
J. Woodcock, J. Davies (Eds.), FM'99 - Formal Methods World Congress
on Formal Methods in the Development of Computing Systems, Toulouse,
France, September 1999. Proceedings, Volume I,
Springer Lecture Notes in Computer Science, vol. 1708,
1999, pp. 776-793.
Revised version.
A meta-notation for protocol analysis
(with I. Cervesato, N.A. Durgin, P.D. Lincoln, and J.C. Mitchell). In:
P. Syverson, ed.,
"12-th IEEE Computer Security Foundations Workshop,
Mordano, Italy, June, 1999", IEEE Computer Society Press,
1999, pp. 55-69.
A probabilistic poly-time framework for protocol analysis
(with P.D. Lincoln, J.C. Mitchell, and M. Mitchell). In:
M. Reiter, ed.,
"5-th ACM Conference on Computer and Communications Security,
San Francisco, California, November, 1998",
ACM Press, 1998, pp. 112-121.
A linguistic characterization of bounded oracle computation
and probabilistic polynomial time
(with J.C. Mitchell and M. Mitchell). In: R. Motwani, ed.,
"39-th Annual IEEE Symposium on Foundations of Computer Science (FOCS)",
Palo Alto, California, November, 1998", IEEE Computer Society Press, 1998,
pp. 725-733.
Specifying Real-Time Finite-State Systems in Linear Logic
(with M.I. Kanovich and M. Okada). In:
"2-nd International Workshop on
Constraint Programming for Time-Critical Applications and Multi-Agent
Systems
(COTIC)", Nice, France, September, 1998,
Electronic Notes in Theoretical Computer Science,
Volume 16 Issue 1 (1998) 15 pp.
Phase Semantics for Light Linear Logic (with M.I. Kanovich
and M. Okada).
Theoretical Computer
Science Volume 294 Issue 3 (2003) pp. 525-549.
Extended abstract
in: "13-th Annual Conference on the Mathematical Foundations
of Programming Semantics", Pittsburgh, Pennsylvania, March, 1997,
Electronic Notes in Theoretical Computer Science, Volume 6 (1997)
12 pp.
Optimization Complexity of Linear Logic Proof Games
(with P.D. Lincoln and J.C. Mitchell).
Theoretical Computer
Science 227 (1999) pp. 299-331.
Extended abstract under the title
"The Complexity of Local Proof Search in Linear Logic"
in: "Proceedings Linear Logic
'96, Tokyo Meeting",
Electronic Notes in Theoretical Computer Science, Volume 3 (1996)
10 pp.
Linear Logic Proof Games and Optimization,
(with P.D. Lincoln and J.C. Mitchell).
Bulletin of Symbolic Logic 2 (1996) pp. 322-338.
The Undecidability of Second Order Multiplicative Linear Logic,
(with Y. Lafont).
Information and Computation
125 (1996) pp. 46-51.
LMD Marseille Preprint 95-17, March, 1995.
Decision Problems for Second Order Linear Logic,
(with P. Lincoln and N. Shankar). In: "Logic and Scientific Methods",
ed. by M.L. Dalla Chiara et al., Kluwer Academic Publishers, 1997,
pp. 127-143.
Extended abstract in: "10-th Annual IEEE Symposium on
Logic in Computer Science", San Diego, California, June, 1995,
IEEE Computer Society Press, 1995, pp. 476-485.
Stochastic Interaction and Linear Logic,
(with P. Lincoln and J.C. Mitchell).
In: "Advances in Linear Logic",
ed. by J.-Y. Girard, Y. Lafont, and L. Regnier,
London Mathematical Society Lecture Notes Series, Volume 222,
Cambridge University Press, 1995, pp. 147-166.
Linear Logic and Computation: A Survey.
In: "Proof and Computation", ed. by H. Schwichtenberg,
NATO Advanced Science Institutes, Series F, Volume 139, Springer-Verlag,
Berlin, 1995, pp. 379-395.
First Order Linear Logic Without Modalities is NEXPTIME-Hard,
(with P. Lincoln).
Theoretical Computer
Science
135 (1994) pp. 139-154.
An Extension of System F with Subtyping,
(with L. Cardelli, J.C. Mitchell, and S. Martini).
Information and Computation
109 (1994) pp. 4-56.
Notes on Sconing and Relators,
(with J.C. Mitchell). In: "Computer Science Logic '92, Selected Papers",
ed. by E. Boerger et al., Springer LNCS 702, 1993, pp. 352-378.
A Brief Guide to Linear Logic. In:
"Current Trends in Theoretical Computer Science",
ed. by G. Rozenberg and A. Salomaa,
World Scientific Publishing Co., 1993, pp. 377-394.
Linearizing Intuitionistic Implication,
(with P. Lincoln and N. Shankar).
Annals of Pure and Applied Logic 60 (1993) pp. 151-177.
Grothendieck Topoi Representing Models of Set Theory,
(with A. Blass).
Annals of Pure and Applied Logic 57 (1992) pp. 1-26.
Decision Problems for Propositional Linear Logic,
(with P. Lincoln, J.C. Mitchell, and N. Shankar).
Annals of Pure and Applied Logic 56 (1992) pp. 239-311,
Special Volume dedicated to the memory of John Myhill.
Bounded Linear Logic: A Modular Approach to Polynomial Time Computability
, (with J.-Y. Girard and P.J. Scott).
Theoretical Computer Science 97 (1992) pp. 1-66.
Normal Forms and Cut-Free Proofs as Natural Transformations,
(with J.-Y. Girard and P.J. Scott).
In: "Logic From Computer Science, Mathematical Sciences Research Institute
Workshop, Berkeley, November, 1989", ed. by Y.N. Moschovakis, MSRI
Publications, Vol. 21, Springer-Verlag, 1992, pp. 217-241.
Inheritance as Implicit Coercion,
(with V. Breazu-Tannen, T. Coquand, and C.A. Gunter).
Information and Computation 93 (1991) pp. 172-221.
Uniform Proofs as a Foundation for Logic Programming,
(with D. Miller, G. Nadathur, and F. Pfenning).
Annals of Pure and Applied Logic 51 (1991) pp. 125-157.
Functorial Polymorphism,
(with E.S. Bainbridge, P.J. Freyd, P.J. Scott).
Theoretical Computer Science 70 (1990) pp. 35-64.
"Categories, Allegories", (with P.J. Freyd).
North-Holland Mathematical Library, North-Holland,
Amsterdam, 1990, xviii + 296 pp.