**M. Nesi and R. Treinen** (editors),

Proceedings of
SecReT'07 -
*Second International Workshop on Security and Rewriting Techniques*.

An RDP'07 workshop associated to RTA, Paris, France, 29 June 2007.

**M. Nesi**,

Specification and Analysis of Security Protocols by Rewriting,

presented at the *First International Workshop on
Security and Rewriting Techniques -
SecReT'06*,

S. Servolo (Venice), July 2006.

**M. Nesi and G. Nocera**,

Deriving the Type Flaw Attacks in the Otway-Rees Protocol by Rewriting,

Nordic Journal of Computing,
2006, Vol. 13, pp. 78-97.

**M. Nesi and G. Nocera**,

Formalization and Verification of Security Protocols by Rewriting,

presented at the *17th Nordic Workshop on Programming Theory -
NWPT'05*,
Copenhagen, October 2005.

**M. Nesi and G. Rucci**,

Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol
by Rewriting,

in Proceedings of the *2nd Workshop on Automated Reasoning for Security
Protocol Analysis -
ARSPA'05*,

Lisbon, July 2005, *Electronic Notes in
Theoretical Computer Science*, 2005, Vol. 135, No. 1, pages 95--114.

**M. Nesi, G. Rucci and M. Verdesca**,

On Rewriting Protocol Specifications,

presented at the *International Workshop
on Security Analysis of Systems: Formalisms and Tools -
SASYFT2004*,
Orléans, 21-22 June 2004.

**P. Inverardi, F. Mancinelli and M. Nesi**,

A Declarative Framework for Adaptable Applications in
Heterogeneous Environments,

in Proceedings of the *ACM Symposium on Applied Computing -
SAC'04,
Mobile Computing and Applications (MCA Track)*,
Nicosia, Cyprus, March 2004.
(paper)

**B. Intrigila and M. Nesi**,

On Structural Properties of Eta-expansions of Identity,

*Information Processing Letters*, 2003, Vol. 87, No. 6, pp. 327-333.
(paper)

**M. Nesi, G. Rucci and M. Verdesca**,

A Rewriting Strategy for Protocol Verification,

*Electronic Notes in Theoretical Computer Science*, 2003, Vol. 86, No. 4.
(paper)

Preliminary version in Proceedings of the *3rd International Workshop
on Reduction Strategies in Rewriting and Programming -
WRS'03*,
Valencia, June 2003, pp. 65-78.

**M. Flammini, P. Inverardi, D. Mango and M. Nesi**,

On the Complexity of Deciding the Derivation Length in
Term Rewriting Systems,

in Proceedings of the *6th International Workshop on Termination -
WST'03*,

Valencia, June 2003.

** M. Nesi**,

Formalising a Value-Passing Calculus in HOL,

*Formal Aspects of Computing*, 1999, Vol. 11, pp. 160-199.

** P. Inverardi and M. Nesi**,

Adding sorts to TRSs: a result on modularity of termination,

in Proceedings of the *Joint Conference on Declarative Programming
APPIA-GULP-PRODE '99*,

M. C. Meo and M. Vilares-Ferro (eds.),
L'Aquila, September 1999, pp. 273-288.

Preliminary version presented at the *4th International Workshop on
Termination - WST'99*, Dagstuhl, May 1999.

Formalising Process Calculi in Higher Order Logic,

Ph.D. Thesis, Technical Report No. 411, Computer Laboratory, University of Cambridge, January 1997.

Abstract

**M. Nesi**,

Mechanising a Modal Logic for Value-Passing Agents in HOL,

*Electronic Notes in Theoretical Computer Science* **5**, 1997,

at http://www.elsevier.nl/locate/entcs/volume5.html.

Preliminary version in Proceedings of the *International Workshop
`Infinity' on
Verification of Infinite State Systems*, Pisa, August 1996.

**M. Nesi**,

Reasoning about Value-Passing Calculi in HOL,

in Proceedings of the 5th *Italian Conference on Theoretical
Computer Science*,

Ravello, Italy, November 1995,
World Scientific Publishing Company, 1996, pp. 434-450.

**P. Inverardi and M. Nesi**,

Infinite Normal Forms for Non-linear Term Rewriting Systems,

*Theoretical Computer Science*,
Elsevier Science Publishers B.V., 1995, Vol. 152, pp. 285-303.

**P. Inverardi and M. Nesi**,

Deciding Observational Congruence of Finite-State CCS Expressions by
Rewriting,

*Theoretical Computer Science*,
Elsevier Science Publishers B.V., 1995, Vol. 139, pp. 315-354.

**M. Nesi, V. de Paiva and E. Ritter**,

Rewriting Properties of Combinators for Rudimentary Linear Logic,

in Proceedings of the *International Workshop on Higher Order
Algebra, Logic and Term Rewriting*,

Amsterdam, September 1993,
Lecture Notes in Computer Science, Springer-Verlag, Vol. 816, 1994,
pp. 256-275.

**M. Nesi**,

Value-Passing CCS in HOL,

in Proceedings of the 6th *International Workshop on Higher Order Logic
Theorem Proving and its Applications*,

Vancouver, August 1993,
Lecture Notes in Computer Science, Springer-Verlag, Vol. 780, 1994,
pp. 352-365.

**P. Inverardi and M. Nesi**,

A Strategy to Deal with Divergent Rewrite Systems,

in Proceedings of the 3rd *International Workshop on
Conditional Term Rewriting Systems*,

Pont-a-Mousson, France, 1992,
Lecture Notes in Computer Science, Springer-Verlag, 1993,
Vol. 656, pp. 458-467.