FET-Global Computing
MyThS
|
Models and Types for Security in Mobile Distributed Systems Contract IST-2001-32617 (MyThS) |
EU proactive initiative
FET-Global Computing
| [1] |
P. Baldan, A. Bracciali, and R. Bruni.
Bisimulation by unification.
In H. Kirchner and C. Ringeissen, editors, Proceedings of AMAST
'02, volume 2422 of LNCS, pages 254-270. Springer-Verlag, 2002. [ bib | .pdf ] |
| [2] |
A. Bossi, R. Focardi, C. Piazza, and S. Rossi.
Transforming processes to check and ensure Information Flow
Security.
In H. Kirchner and C. Ringeissen, editors, Proc. of Int.
Conference on Algebraic Methodology And Software Technology, volume 2422 of
LNCS, pages 271-286. Springer-Verlag, 2002. [ bib | .pdf ] |
| [3] |
A. Bossi, R. Focardi, C. Piazza, and S. Rossi.
A Proof System for Information Flow Security.
In M. Leuschel, editor, Proc. of Int. Workshop on Logic Based
Program Development and Transformation, LNCS 2664, 199-218.
Springer-Verlag, 2003. [ bib | .pdf ] |
| [4] |
C. Braghin, A. Cortesi, and R. Focardi.
Control Flow Analysis of Mobile Ambients with Security
Boundaries.
In Bart Jacobs and Arend Rensink, editors, Proc. of Fifth IFIP
International Conference on Formal Methods for Open Object-Based Distributed
Systems (FMOODS'02), pages 197-212. Kluwer Academic Publisher,
2002. [ bib | .pdf ] |
| [5] |
C. Braghin, A. Cortesi, and R. Focardi.
Security Boundaries in Mobile Ambients.
Computer Languages, 28(1):101-127, Nov 2002. [ bib | .pdf ] |
| [6] |
C. Braghin, A. Cortesi, R. Focardi, and S. van Bakel.
Boundary Inference for Enforcing Security Policies in
Mobile Ambients.
In Ricardo Baeza-Yates, Ugo Montanari, and Nicola Santoro, editors,
Proc. of The 2nd IFIP International Conference on Theoretical Computer
Science (TCS'02), pages 383-395. Kluwer Academic Publisher, 2002. [ bib | .pdf ] |
| [7] |
M. Bugliesi, S. Crafa, M. Merro, and V. Sassone.
Communication interference in mobile boxed ambients.
In M. Agrawal and A. Seth, editors, FSTTCS'02: Int. Conf. on
Foundations of Software Technology and Theoretical Computer Science, number
2556 in LNCS, pages 71-84. Springer-Verlag, 2002. [ bib | .pdf ] |
| [8] |
M. Bugliesi, R. Focardi, Maffei M., and F. Tudone.
Principles for entity authentication.
Technical Report 16, Università Ca' Foscari, Venezia, 2002. [ bib | .pdf ] |
| [9] |
G. Castagna and F. Zappa Nardelli.
The Seal Calculus revisited: contextual equivalence and
bisimilarity.
In M. Agrawal and A. Seth, editors, FST&TCS '02, 22th
Conference on the Foundations of Software Technology and Theoretical Computer
Science, volume 2556 of Lecture Notes in Computer Science. Springer,
Kanpur, India, December 2002. [ bib | .ps.gz] |
| [10] |
S. Crafa, M. Bugliesi, and G. Castagna.
Information flow security for boxed ambients.
In F-WAN: Int. Workshop on Foundations of Wide Area Networks,
number 66(3) in ENTCS, 2002. [ bib | .pdf ] |
| [11] |
M. Dezani-Ciancaglini, A. Frisch, E. Giovannetti, and Y. Motohama.
The relevance of semantic subtyping', Workshop on Intersection Types
and Related Systems.
Number 70(1) in ENTCS, 2002. [ bib| .ps.gz ] |
| [12] |
R. Focardi and S. Rossi.
Information Flow Security in Dynamic Contexts.
In Proc. of the IEEE Computer Security Foundations Workshop,
pages 307-319. IEEE Computer Society Press, 2002. [ bib | .pdf ] |
| [13] |
A. Frisch, G. Castagna, and V. Benzaken.
Semantic subtyping.
In 17th IEEE Symposium on Logic in Computer Science, pages
137-146. IEEE Computer Society Press, 2002. [ bib | .ps.gz ] |
| [14] |
J. C. Godskesen, T. Hildebrandt, and V. Sassone.
A calculus of mobile resources.
In Int. Conf. on Concurrency Theory, CONCUR 02, volume 2421 of
LNCS, pages 272-287. Springer-Verlag, 2002. [ bib | .ps.gz] |
| [15] |
Matthew Hennessy, Massimo Merro, and Julian Rathke.
Towards a behavioural theory of access and mobility control in
distributed systems.
Technical Report 2002:01, COGS, University of Sussex, 2002. [ bib | .ps.gz] |
| [16] |
M. Merro and V. Sassone.
Typing and Subtyping Mobility in Boxed Ambients.
In Proceedings of Concur'02, volume 2421 of LNCS, pages
304-320. Springer-Verlag, 2002. [ bib | .ps.gz] |
| [17] |
F. Barbanera, M. Bugliesi, M. Dezani-Ciancaglini, and V. Sassone.
A Calculus of Bounded Capacities.
In ASIAN'03, Eighth Asian Computing Science Conference, number
2896 in Lecture Notes in Computer Science, pages 205--223, 2003.
[ bib | .pdf ] |
| [18] |
V. Benzaken, M. Burelle, and G. Castagna.
Information flow security for XML transformations.
In ASIAN '03, 8th Asian Computing Science Conference, LNCS.
Springer, December 2003.
[ bib | .ps.gz ] |
| [19] |
A. Bossi, R. Focardi, C. Piazza, and S. Rossi.
Bisimulation and Unwinding for Verifying Possibilistic
Security Properties.
In L. D. Zuck, P. C. Attie, A. Cortesi, and S. Mukhopadhyay, editors,
Proc. of Int. Conference on Verification, Model Checking, and Abstract
Interpretation (VMCAI'03), volume 2575 of LNCS, pages 223--237.
Springer-Verlag, 2003.
[ bib | .pdf ] |
| [20] |
A. Bossi, R. Focardi, C. Piazza, and S. Rossi.
Refinement Operators and Information Flow Security.
In Proc. of the 1st IEEE Int. Conference on Software Engineering
and Formal Methods (SEFM'03), pages 44--53. IEEE Computer Society Press,
2003.
[ bib | .pdf ] |
| [21] |
A. Bossi, D. Macedonio, C. Piazza, and S. Rossi.
Compositional Action Refinement and Information Flow
Security.
Technical Report CS-2003-13, Dipartimento di Informatica,
Università Ca' Foscari di Venezia, Italy, 2003.
[ bib | .ps.gz ] |
| [22] |
A. Bossi, D. Macedonio, C. Piazza, and S. Rossi.
Information Flow Security and Recursive Systems.
In Proc. of the Italian Conference on Theoretical Computer
Science (ICTCS'03), volume 2841 of LNCS, pages 369--382.
Springer-Verlag, 2003.
[ bib | .ps.gz ] |
| [23] |
A. Bossi, D. Macedonio, C. Piazza, and S. Rossi.
Secure Contexts for Confidential Data.
In Proc. of the IEEE Computer Security Foundations Workshop
(CSFW'03), pages 14--28. IEEE Computer Society Press, 2003.
[ bib | .pdf ] |
| [24] |
C. Braghin, C. Cortesi, and R. Focardi.
Freshness Analysis for Authentication Protocols in Mobile Ambients.
Unpublished, October 2003.
[ bib | .pdf ] |
| [25] |
C. Braghin and C. Piazza.
Checking Integrity via CoPS and BANANA: the E-Commerce Case Study.
Electronic Notes in Computer Science, 99. Elsevier 2004.
[ bib | .pdf ] |
| [26] |
R. Bruni, J. Meseguer, U. Montanari, and V. Sassone.
Functorial Models for Contextual Pre-Nets.
In Proceedings of Italian Conference on Theoretical Computer
Science, Lecture Notes in Computer Science n. 2841, 256--270,
Springer, 2003.
[ bib | .ps.gz ] |
| [27] |
M. Bugliesi, G. Castagna, and S. Crafa.
Access Control for Mobile Agents: the Calculus of Boxed Ambients.
ACM Transactions on Programming Languages and Systems (TOPLAS),
26(1):57 -- 124, Jan 2004.
[ bib | .ps.gz ] |
| [28] |
M. Bugliesi, A. Ceccato, and S. Rossi.
Context-Sensitive Equivalences for Non-Interference based Protocol
Analysis.
In FCT'03, International Symposium on Fundamentals of
Computing, volume 2751 of LNCS, pages 364--375. Springer--Verlag,
2003.
[ bib | .pdf ] |
| [29] |
M. Bugliesi, S. Crafa, Prelic A., and V. Sassone.
Secrecy in Untrusted Networks.
In ICALP'03, Int. Colloquium on Automata Languages and
Programming, number 2719 in Lecture Notes in Computer Science, pages
969--983. Springer--Verlag, 2003.
[ bib | .ps.gz ] |
| [30] |
M. Bugliesi, S. Crafa, M. Merro, and V. Sassone.
Communication and Mobility Control in Boxed Ambients.
Information and Computation, 2004.
To appear.
[ bib | .ps.gz ] |
| [31] |
M. Bugliesi, R. Focardi, and M. Maffei.
Principles for Entity Authentication.
In PSI 2003, Perspectives of Systems Informatics, 5th
International Andrei Ershov Memorial Conference, number 2890 in Lecture
Notes in Computer Science, pages 294--306. Springer--Verlag, 2003.
[ bib | .pdf ] |
| [32] |
M. Bugliesi, R. Focardi, and M. Maffei.
Compositional Analysis of Entity Authentication Protocols.
In ESOP'04, European Symposium on Programming, Lecture
Notes in Computer Science, 2986, 140-154. Springer 2004.
[ bib | .pdf ] |
| [33] |
M. Bugliesi and S. Rossi.
Non Interference Proof Techniques for the Analysis of Cryptographic
Protocols. Journal of Computer Security, 13-1, pages 87-113, 2005.
[ bib | .pdf ] |
| [34] |
M. Carbone, M. Nielsen, and V. Sassone.
A Formal Model for Trust in Dynamic Networks,
In Proceedings of Int. Conf. on Software Engineering and Formal
Methods, SEFM03, 54--61, IEEE Computer Society Press, 2003.
[ bib | .pdf ] |
| [35] |
G. Castagna, J. Vitek, and F. Zappa Nardelli.
The Seal Calculus.
Information and Computation, 2004.
To appear.
[ bib | .ps.gz ] |
| [36] |
R. Focardi and M. Maffei.
The rho-spi calculus at work: Authentication Case Studies.
Electronic Notes in Computer Science, 99. Elsevier 2004.
[ bib | .pdf ] |
| [37] |
M. Hennessy, M. Merro, and J. Rathke.
Towards a Behavioural Theory of Access and Mobility Control in
Distributed Systems.
In FoSSaCS 2003, Sixth Int. Conference on Foundations of
Software Science and Computation Structures, volume 2620 of Lecture
Notes in Computer Science, pages 282 -- 298. Springer, 2003.
[ bib | .pdf ] |
| [38] |
M. Hennessy, M. Merro, and J. Rathke.
Towards a behavioural theory of access and mobility control in
distributed systems.
Theoretical Computer Science, 2004.
Volume 322 (2004) 615-669
[ bib | .pdf ] |
| [39] |
M. Hennessy, J. Rathke, and N. Yoshida.
SafeDpi: a language for controlling mobile code.
In FoSSaCS'04, Seventh Int. Conference on Foundations of
Software Science and Computation Structures, Lecture Notes in
Computer Science, 2987, 2004, pages 241-256. Also available as
Sussex Technical Report cs02:2003
[ bib | .ps.gz ] |
| [40] |
S. Hym.
Non-interférence dans les calculs de processus.
Master's thesis, DEA Programmation, Université Paris 7, September
2003.
[ bib | .ps.gz ] |
| [41] |
C. Lhoussaine.
Type inference for a distributed pi-calculus.
In Proceedings of European Symposium on Programming, ESOP'03,
volume 2618 of Lecture Notes in Computer Science, pages 253--268.
Springer-Verlag, 2003.
[ bib | .pdf ] |
| [42] |
C. Lhoussaine.
Type inference for a distributed pi-calculus.
Science of Computer Programming, 50, 1-3, pages 225-252.
Elsevier North-Holland, Inc., 2004.
[ bib | .pdf ] |
| [43] |
C. Lhoussaine and V. Sassone.
A dependently typed ambient calculus.
In Proceedings of European Symposium on Programming, ESOP'04,
Lecture Notes in Computer Science, Springer, 2004.
To appear.
[ bib | .pdf ] |
| [44] |
M. Merro and F. Zappa Nardelli.
Bisimulation Proof Methods for Mobile Ambients.
In ICALP'03, Int. Colloquium on Automata Languages and
Programming, number 2719 in Lecture Notes in Computer Science, pages
584--598. Springer--Verlag, 2003.
[ bib | .ps.gz ] |
| [45] |
V. Sassone and P. Sobocinski.
Locating Reactions using 2-Categories.
Theoretical Computer Science, Elsevier, 2004. To appear.
[ bib | .pdf ] |
| [46] |
D. Varacca, H. Völzer, and G. Winskel.
Proceedings of 15th CONCUR,
LNCS 3170,481-496, Springer 2004.
[ bib | .pdf ] |
| [47] |
V. Benzaken, G. Castagna and C. Miachon.
CQL: a pattern-based query language for XML.
In Bases de données advancées. 2004. [ bib | .pdf ] |
| [48] |
V. Benzaken, G. Castagna, and C. Miachon. A full pattern-based paradigm for XML query
processing. In PADL'05, 7th International Symposium on Practical Aspects of Declarative
Languages, LNCS, Springer, 2005. [ bib | .ps.gz ] |
| [49] |
A. Bossi, R. Focardi, C. Piazza, and S. Rossi. Verifying Persistent Security Properties. Computer
Languages, Systems and Structures, volume 30, n. 3-4 231–258, Elsevier 2004. [ bib | .ps.gz ] |
| [50] |
A. Bossi, C. Piazza, and S. Rossi. Modelling Downgrading in Information Flow Security Proc.
of the 17th IEEE Computer Security Foundations Workshop, CSFW'04, 187–201, IEEE
Computer Society Press, June 2004. [ bib | .ps.gz ] |
| [51] |
C. Braghin, D. Gorla, and V. Sassone. A distributed calculus for role-based access control.
In Proc. of 17th Computer Security Foundations Workshop (CSFW’04), pages 48–60. IEEE
Computer Society, 2004. [ bib | .pdf ] |
| [52] |
C. Braghin, D. Gorla, and V. Sassone. A Distributed Calculus of Role-Based Access Control
(full version). Submitted 2004. [ bib | .pdf ] |
| [53] |
R. Bruni, U. Montanari, and V. Sassone. Observational congruences for dynamically reconfigurable
tile systems. Theoretical Computer Science, 2005. To appear. [ bib | .pdf ] |
| [54] |
A. Bucciarelli and A. Salibra, The Sensible Graph Theories of Lambda Calculus. 19th IEEE
Symposium on Logic in Computer Science (LICS'04). IEEE Computer Society, July 2004. [ bib | .pdf ] |
| [55] |
M. Bugliesi, G. Castagna, S. Crafa, R. Focardi and V. Sassone. Name-passing calculi and
crypto-primitives: a survey. In Foundations of Security Analysis and Design. Lecture Notes in
Computer Science 2946, 91–138, Springer, 2004. [ bib | .pdf ] |
| [56] |
M. Bugliesi, D. Colazzo and S. Crafa. Type based Discretionary Access Control.
In Proceedings of CONCUR'04, LNCS 3170, 225–239, Springer 2004.
[ bib | .pdf ] |
| [57] |
M. Bugliesi, R. Focardi, and M. Maffei. Authenticity by tagging and typing. In 2nd ACM
Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE'04),
2004. Affiliated to CCS, October 29, 2004, Washington DC. [ bib | .pdf ] |
| [58] |
M. Carbone, M. Nielsen, and V. Sassone. A Calculus of Trust Management. In Proceedings of
the 24th Conference on Foundations of Software Technology and Theoretical Computer Science,
FST&TCS'04, LNCS 3328, 161–173, Springer, 2004. [ bib | .pdf ] |
| [59] |
G. Castagna and A. Frisch. A gentle introduction to semantic subtyping. In Second workshop
on Programmable Structured Documents, Hakone, Japan, 2004. [ bib | .ps.gz ] |
| [60] |
G. Castagna, R. De Nicola and D. Varacca. Semantic subtyping for the pi-calculus.
In 20th IEEE Symposium on Logic in Computer Science (LICS'05).
IEEE Computer Society, 2005. [ bib | .pdf ] |
| [61] |
R. Chadha, D. Macedonio, and V. Sassone. A Hybrid Intuitionistic Logic:
Semantics and Decidability. Submitted 2004. [ bib | .pdf ] |
| [62] |
G. Conforti, D. Macedonio, and V. Sassone. BiLogics: Spatial-Nominal Logics for Bigraphs.
Submitted 2004. [ bib | .pdf ] |
| [63] |
G. Conforti, D. Macedonio, and V. Sassone. Bigraphical Logics for XML. Submitted 2004. [ bib | .pdf ] |
| [64] |
R. Focardi, M. Maffei, and F. Placella. Inferring authentication tags. In Proc. of 2005 IFIP
WG 1.7, ACM SIGPLAN and GI FoMSESS Workshop on Issues in the Theory of Security
(WITS’05), January 10–11, 2005. (co-located with POPL’05). [ bib | .pdf ] |
| [65] |
A. Frisch. Regular tree language recognition with static information. In Proceedings of IFIP
Conference on Theoretical Computer Science (TCS'04), Kluver 2004. [ bib | .pdf ] |
| [66] |
A. Frisch and L. Cardelli. Greedy regular expression matching. In Proceedings of International
Conference on Automata, Languages Programming, (ICALP'04), LNCS, Springer 2004. [ bib | .pdf ] |
| [67] |
D. Gorla, M. Hennessy, and V. Sassone. Security Policies as Membranes in Systems for Global
Computing. In Foundations of Global Ubiquitous Computing, FGUC, ENTCS, Elsevier 2004. [ bib | .pdf ] |
| [68] |
H. Hosoya. Regular expression filters for XML. In Programming Language Technologies for
XML (PLAN-X’04), 13–27, 2004. [ bib | .ps.gz ] |
| [69] |
H. Hosoya, A. Frisch and G. Castagna. – Parametric polymorphism for XML. In POPL’05,
32nd ACM Symposium on Principles of Programming Languages, ACM Press, 2005. [ bib | .ps.gz ] |
| [70] |
K. Krukow, M. Nielsen, and V. Sassone. A Formal Framework for Concrete Reputation Systems.
Submitted 2004. [ bib | .pdf ] |
| [71] |
M. Kwiatkowska, R. Milner and V. Sassone. Science for Global Ubiquitous Computing, Proposal
of a Grand Challenge for the UK Computing Research Councils programme. Bulletin of
the EATCS vol. 82, 325–333, 2004. [ bib | .pdf ] |
| [72] |
M. Kwiatkowska and V. Sassone. Science for Global Ubiquitous Computing.
In Grand Challenges in Computing Proceedings. The British Computer Society 2005. To appear. [ bib | .pdf ] |
| [73] |
J. Laird. A Game Semantics of Local Names and Good Variables. In Proceedings of FOSSACS'04,
LNCS 2987, 289–303, Springer 2004. [ bib | .pdf ] |
| [74] |
J. Laird. A Calculus of Coroutines. In Proceedings of ICALP'04, LNCS 3142, 882–893,
Springer 2004. [ bib | .pdf ] |
| [75] |
J. Laird. A Calculus of Coroutines, Theoretical Computer Science,
Elsevier 2005. To appear. [ bib | .pdf ] |
| [76] |
J. Laird. A game semantics of the asynchronous pi-calculus and its dual. In Proceedings of
Games for Logic and Programming Languages, 2005. To appear. [ bib | .pdf ] |
| [77] |
M. Maffei. Tags for Multi-Protocol Authentication. In 2nd Workshop on Security Issues in
Coordination Models, Languages and Systems (SECCO'04). ENTCS, Elsevier 2004. [ bib | .pdf ] |
| [78] |
G. Milicia and V. Sassone. Temporal Constraints for Concurrent Object Synchronisation. Concurrency
and Computation: Practice and Experience, vol. 16:1–34, 2004. [ bib | .pdf ] |
| [79] |
G. Milicia and V. Sassone. The Inheritance Anomaly: Ten years after. In Proceedings of Object
Oriented Programming Languages and Systems, OOPS'04, special track at the 19th ACM
Symposium on on Applied Computing, SAC ’04, 1267–1274, ACM Press, 2004. [ bib | .pdf ] |
| [80] |
N. Nguyen and J. Rathke. A typed static analysis for a concurrent policy-based resource access
control. Submitted 2005. [ bib | .pdf ] |
| [81] |
C. Piazza, E. Pivato, S. Rossi. CoPS - Checker of Persistent Security. Proc. of the Tenth International
Conference on Tools and Algorithms for the Construction and Analysis of Systems,
TACAS'04. LNCS 2988, 144–152, Springer, March 2004. [ bib | .ps.gz ] |
| [82] |
V. Sassone and P. Sobociński. A Congruence for Petri Nets. In International Workshop
on Petri Nets and Graph Transformations, ENTCS 496, 2004. [ bib | .pdf ] |
| [83] |
V. Sassone and P. Sobociński. Reactive Systems over Cospans.
In 20th IEEE Symposium on Logic in Computer Science (LICS'05).
IEEE Computer Society, 2005. [ bib | .pdf ] |
| [84] |
G. Winskel and F. Zappa Nardelli. new-HOPLA – a higher-order process language with name
generation. In Proceedings of IFIP Conference on Theoretical Computer Science (TCS'04),
Kluver, 2004. [ bib | .pdf ] |
| [85] |
A. Bossi, C. Piazza, and S. Rossi.
Compositional Information Flow Security for Concurrent Programs.
Technical Report CS-2005-4, Dipartimento di Informatica,
Università Ca' Foscari di Venezia, Italy, 2005. [ bib | .pdf ] |
| [86] |
M. Bugliesi and M. Giunti.
Type Based Security Policies in Untyped Contexts.
In preparation, 2005
[ bib | .pdf ] |
| [87] |
M. Bugliesi, R. Focardi, and M. Maffei.
Analysis of type-based analyses of authentication protocols.
In 18th IEEE Computer Security Foundation Workshop (CSFW18), 2005.
To appear. [ bib | .pdf ] |
| [88] |
S. Crafa and S. Rossi.
A Theory of Noninterference for the pi-calculus.
In Proceedings of TGC 2005, Symposium on Trustworthy Global
Computing, LNCS series. Springer 2005. To appear. [ bib | .pdf ] |
| [89] |
R. Focardi, S. Rossi, and A. Sabelfeld.
Bridging Language-Based and Process Calculi Security.
In Foundations of Software Science and Computation Structure
(FoSSaCS 2005), LNCS 3441, 299--315,
Springer, 2005. [ bib | .pdf ] |