Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Andre Scedrov's Selected Publications
Andre Scedrov's Selected Publications
The following list contains selected publications of
Andre Scedrov,
partially supported by Office of Naval Research, by National Science
Foundation, by a Centennial Research Fellowship from the American
Mathematical Society, and by a Senior Fellowship from the Japan Society
for the Promotion of Science.
Any opinions, findings, and conclusions or recommendations expressed in
these publications are those of the authors and do not necessarily reflect
the views of the funding agencies.
The files are
also available from an ftp directory.
Most of the papers available from this document appear in print and the
corresponding copyright is held by the publisher. While the papers may be
used for personal use, redistribution or reprinting for commercial purposes
is not allowed.
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].
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,
accepted for publication. 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.
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.
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]
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,
accepted for publication. 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.
[.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]
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].
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).
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.
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.
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.
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.