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, accepted for publication.
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, accepted for publication.
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].
A Rewriting Framework for Activities Subject to Regulations
(with M.I. Kanovich, T. Ban Kirigin, V. Nigam, C.L. Talcott, and
R. Perovic). 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].
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.
Bounded Memory Dolev-Yao Adversaries in Collaborative Systems
(with M. Kanovich, T. Ban Kirigin, and V. Nigam).
Information and Computation, accepted for publication.
Extended abstract in: P. Degano et al., eds.,
The 7th International Workshop on Formal Aspects of Security & Trust (FAST2010). Springer LNCS Volume 6561,
Springer-Verlag, 2011, pp. 18-33.
[.pdf].
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.