Bibliography

1

Abramsky, S., Jagadeesan, R. and Malacaria, P., Full Abstraction for PCF. Info. & Comp. 163 (2000), 409-470.

2

Abadi, M. and Gordon, A. A calculus of cryptographic protocols, Information and computation, 1999.

3

Abadi,M. and Fournet,C. Mobile Values, New Names, and Secure Communication. POPL'01, ACM Press, 2001.

4

Abadi,M. and Fournet,C. Hiding Names: private authentication in the applied pi-calculus, ISSS02, LNCS 2609, 317-338.

5

Abadi, M. and Blanchet, B. Analyzing Security Protocols with Secrecy Types and Logic Programs. POPL'2002, 33-44, ACM, 2002.

6

Abadi, M., Banerjee, A., Heintze, N. and Riecke, J., A core calculus of dependency, POPL'99, ACM, 1999.

7

Abramsky, S., Honda, K. and McCusker, G., A Fully Abstract Game Semantics for General References. LICS'98 IEEE, 1998.

8

Amtoft, T., Nielson, F., and Nielson, H., Type and Effect Systems: Behaviours for Concurrency, IC Press, 1999.

9

Ball et al. Automatic predicate abstraction of C programs. PLDI'01, ACM, 2001.

10

Bhargavan, K., Fornet, C. and Gordon, A., A Semantics for Web Services Authentication, to appear in POPL'04. ACM.

11

Berger, M., Honda, K. and Yoshida, N., Genericity and the $\pi$-Calculus, Proc. of 6th International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2003), LNCS 2620, Springer, 2003.

12

Berger, M., Honda, K. and Yoshida, N., Sequentiality and the $\pi$-Calculus, TLCA01, LNCS 2044, Springer, 2001.

13

Berger, M. and Honda, K., The Two-Phase Commitment Protocol in an Extended pi-Calculus, Proc. EXPRESS'00, Electronic Notes in Theoretical Computer Science, Elsevier Science, August, 2000.

14

Boudol, G., Asynchrony and the pi-calculus, INRIA Research Report 1702, 1992.

15

Bodei, C. et al, Control Flow Analysis for the pi-calculus. Proceedings of CONCUR'98, LNCS 1466:84-98, Springer.

16

Bodei, C., et al., Techniques for Security Checking: Non-Interference vs Control Flow Analysis. Proceedings of the Final Workshop Tosca 2001. ENTCS 62, 2001.

17

Clark D., Hankin C. and Hunt S., Information Flow Analsyis for Algol-like Languages, Computer Languages, Elsevier Science, to appear 2002.

18

Clark D., Hunt S., and Malacaria P.
Quantitative analysis of leakage of confidential data.
In QAPL 2001, volume 59 of ENTCS, 2002.

19

Clarke, E. et al. Model Checking, MIT Press.

20

Denning, D. and Denning, P., Certification of programs for secure information flow. Communication of ACM, ACM, 20:504-513, 1997.

21

Di Pierro A. and Wiklicky H., Probabilistic Concurrent Constraint Programming: Towards a Fully Abstract Model, MFCS98, LNCS 1450, Springer-Verlag, 1998.

22

Di Pierro A. and Wiklicky H., Measuring the Precision of Abstract Interpretations, LOPSTR00, LNCS 2042, Springer, 1998.

23

Di Pierro A. and Wiklicky H., Concurrent Constraint Programming: Towards Probabilistic Abstract Interpretation, Proc PPDP00, ACM SIGPLAN, 2000.

24

Di Pierro A., Hankin C. and Wiklicky H.,
Analysing Approximative Confinement under Uniform Attacks.
In Proceedings of SAS'02 LNCS 2477, 2002. Springer Verlag.

25

Di Pierro A., Hankin C. and Wiklicky H.,
Approximate non-interference.
In I. Cervesato, editor, CSFW'02 IEEE, 2002.

26

Di Pierro A., Hankin C. and Wiklicky H.,
Approximate non-interference.
In Journal of Computer Security, 2003.

27

Di Pierro A., Hankin C. and Wiklicky H.,
Measuring the Confinement of Concurrent Probabilistic Systems.
In Proceedings of WITS'03 Workshop on Issues in the Theory of Security, 2003.

28

Di Pierro A., Hankin C. and Wiklicky H.,
Quantitative Relations and Approximate Process Equivalences.
In Proceedings of CONCUR'03, LNCS 2761, 2003. Springer Verlag.

29

Fiore, M. and Honda, K., Recursive types in games: Axiomatics and process representation. LICS'98, 13th Annual IEEE Symposium on Logic in Computer Science, 345-356, IEEE, 1998.

30

Flanagan, C. et al. Extended Static Checking for Java, PLDI'02.

31

Flanagan, C., Freund, S. and Qadeer, S., Thread-Modular Verification for Shared-Memory Programs, ESOP'02, LNCS 2305, 262-277, Springer, 2002.

32

Girard, J.-Y., Linear Logic, TCS, Vol. 50, 1-102, 1987.

33

Gordon, A. and Jeffrey, A., Authenticity by typing for security protocols, IEEE CSFW 2001, 2001.

34

Harper, Morrisett and Shneider. Language-Based Security. LNCS 2000, Springer Verlag.

35

Hennessy, M., Rathke, J. and Yoshida, N., SafeDpi: a language for controlling mobile code. 65 pages. To appear as a technical report at Sussex University. Oct, 2003.

36

Hennessy, M. and Riely, J., Information flow vs resource access in the asynchronous pi-calculus, ICALP00, LNCS 1853, 415-427, 2000.

37

Herescu, M and Palamidessi, C., Probabilistic asynchronous $\pi$-calculus. FOSSACS'00, LNCS 1784, 146-160. Springer-Verlag, 2000.

38

Honda, K. Composing Processes. POPL'96, January 1996.

39

Honda, K. Elementary Structures for Process Theory (1): Sets with Renaming. MSCS, 2001.

40

Honda, K. and Tokoro, M., An Object Calculus for Asynchronous Communication. ECOOP'91, LNCS 512, Springer 1991.

41

Honda, K., Vasconcelos, V. and Yoshida, N, Secure Information Flow as Typed Process Behaviour, ESOP'00, LNCS 1782, 2000.

42

Honda, K. and Yoshida, N., On Reduction-based Process Semantics. TCS, No. 151, North-Holland, 1995.

43

Honda, K. and Yoshida, N., Combinatory Representation of Mobile Processes, POPL'94, ACM, 1994.

44

Honda, K. and Yoshida, N., Game-Theoretic Analysis of Call-by-Value Computation, TCS, Vol. 221 (1999), North-Holland, 1999.

45

Honda, K. and Yoshida, N., A uniform type structure for secure information flow. POPL'02, ACM Press, 2002. The full version is available as Dcs Technical Report at www.dcs.qmul.ac.uk/ $\tilde{\mbox{ }}$kohei.

46

Honda, K. and Yoshida, N., Noninterference through Flow-Analysis, 45pp, submitted for a journal publication, 2003. Available as Dcs Technical Report at www.dcs.qmul.ac.uk/ $\tilde{\mbox{ }}$kohei.

47

Hyland, M. and Ong, L., "On Full Abstraction for PCF": I, II and III. Info. & Comp. 163 (2000), 285-408.

48

Jensen, T. et al. Security and Dynamic Class Loading in Java: A Formalisation. Proc. International Conference on Computer Languages, IEEE, 1999

49

Kocher P.C.
Cryptanalysis of Diffie-Hellman, RSA, DSS, and other cryptosystems using timing attacks.
In CRYPTO '95, LNCS 963,

50

Myers, A. and Liskov, B., A decentralized model for information flow control. SOSP'97, 129-142, ACM, 1997.

51

Malacaria P. and Hankin C., Non-deterministic Games and Program Analysis: An application to security, LICS'99, IEEE Press, 1999.

52

Myers, A. JFlow: Practical Mostly-Static Information Flow Control. POPL'99, ACM Press. 1999.

53

Milner, R., Functions as Processes, MSCS. 2(2):119-141, 1992,

54

Milner, R., Parrow, J.G. and Walker, D., A Calculus of Mobile Processes. Information and Computation, 100(1):1-77, 1992.

55

Myers A. and Sabelfeld A., Language-based information flow security, IEEE Journal on Selected Areas in Communications.

56

Nielson, F., Nielson H.R., and Hankin C., Principles of Program Analysis, Springer-Verlag, 1999.

57

Palsberg, J., Type-based analysis and applications, 2001, available at: http://www.cs.purdue.edu/homes/palsberg.

58

Pottier, F. and Simonet, V. Information Flow Inference for ML. POPL'02, ACM, 2002.

59

Riely, J. and Hennessy, M., Trust and partial typing in open systems of mobile agents. POPL'99, ACM Press, 1999.

60

Riecke, J. Fully Abstract Translations between Functional Languages. MSCS, CUP, 1993.

61

Skoglund and Wrigstad. A mode system for read-only references in Java. A typescript, 10pp, 2001.

62

Smith, G., A New Type System for Secure Information Flow, CSFW'01, IEEE, 2001.

63

Smith, G. and Volpano, D., Secure information flow in a multi-threaded imperative language, POPL'98, ACM, 1998.

64

SecSafe, A European FET Open project, http://www.doc.ic.ac.uk/ $\tilde{\mbox{ }}$siveroni/secsafe.

65

Volpano, D., Smith, G. and Irvine, C., A Sound type system for secure flow analysis. J. Computer Security, 4(2,3):167-187, 1996.

66

VerifiCard, a European Project for Smart Card Verification, http://www.verificard.org.

67

Volpano, D. and Smith, G., Verifying Secrets and Relative Secrecy, POPL'00, 268-276, 2000, ACM Press.

68

Yoshida, N., Channel Dependency Types for Higher-Order $\pi$-Calculus, To appear in POPL04, ACM Press, 2004.

69

Yoshida, N., Optimal Reduction in Weak lambda-calculus with Shared Environments: FPCA'93, Functional Programming and Computer Architecture, ACM SIGACT-SIGPLAN, June, 1993.

70

Yoshida, N., Graph Types for Monadic Mobile Processes. Proc. of 16th FST/TCS, LNCS 1180, 1996.

71

Yoshida, N., Minimality and Separation Results on Asynchronous Mobile Processes: Representability Theorems by Concurrent Combinators, TCS, 2002, North Holland.

72

Yoshida, N., Berger, M. and Honda, K., Strong Normalisation in the $\pi$-Calculus, Proc. LICS '01. IEEE, June, 2001. The full version in Info. & Comp.

73

Yoshida, N. and Hennessy, M., Subtyping and Locality in Distributed Higher Order Processes. CONCUR'99, LNCS 1664, Springer, 1999.

74

Yoshida, N. and Hennessy, M., Assigning Types to Processes, LICS '00, IEEE, 2000, Full version to appear in Info. & Comp.

75

Yoshida, N., Honda, K. and Berger, M. Linearity and Bisimulation, Proc. of 5th International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2002), LNCS 2303, Springer, 2002.

76

Zdancewic, S. and Myers, A., Secure Information Flow and CPS, ESOP01, LNCS 2028, 46-62, Springer, 2001.