Specification of Security Properties The objective of this task is to determine the most appropiate way of expressing the dynamic properties of interest for security and safety. We have some experience of using a linear-time temporal logic over program traces for expressing a variety of security properties. This task is an investigation of the scalability and extension of these techniques to realistic case studies.

Documents

	Renaud Marlet and Daniel Le Metayer. First note on industrial needs in terms of language, API and security properties of Java Card. SECSAFE-TL-002. Renaud Marlet. Typical code Patterns Found in Java Card Applets to be used as Targets for Program Analysis. SECSAFE-TL-003. Renaud Marlet. Proposition of a Hierarchy of Languages to be studied in Secsafe. SECSAFE-TL-004. Renaud Marlet. Syntax of the JCVM Language to be studied in the SecSafe Project. May 16, 2001. SECSAFE-TL-005. ( .pdf) Renaud Marlet and Daniel Le Metayer. Security Properties and Java Card Specificities to be Studied in the SecSafe Project. August 23, 2001. SECSAFE-TL-006. ( .pdf) Rene Rydhof Hansen. Computer Security Bibliography. July 5, 2001. SECSAFE-DAIMI-003. ( .ps) Rene Rydhof Hansen. Java Bibliography. January 22, 2001. SECSAFE-DAIMI-004. ( .pdf) Renaud Marlet and Cedric Mesnil. Demoney: A Demonstrative Electronic Purse - Card specification . November 22, 2002. SECSAFE-TL-007. ( .pdf)