Return-Path: Return-Path: Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET with NIFTP to fgate (PP) id <19028-0@swan.cl.cam.ac.uk>; Sat, 23 Feb 1991 18:08:46 +0000 Received: from vax.nsfnet-relay.ac.uk by sun2.nsfnet-relay.ac.uk with SMTP inbound id <24064-246@sun2.nsfnet-relay.ac.uk>; Sat, 23 Feb 1991 02:58:58 +0000 Received: from iris.ucdavis.edu by vax.NSFnet-Relay.AC.UK via NSFnet with SMTP id aa27001; 23 Feb 91 1:43 GMT Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.4.0) id AA00499; Wed, 20 Feb 91 15:14:30 -0800 Received: from munnari.OZ.AU by clover.eecs.ucdavis.edu (5.59/UCD.EECS.1.11) id AA05284; Wed, 20 Feb 91 15:16:00 PST Received: from itd.dsto.oz (via augean) by munnari.oz.au with SunIII (5.64+1.3.1+0.50) id AA00444; Thu, 21 Feb 1991 10:14:14 +1100 (from cant@itd.dsto.oz.au) Received: from itd0.dsto.oz (itd0.ARPA) by fang.dsto.oz (1.2/4.7) id AA19552; Thu, 21 Feb 91 09:41:01 pdt Received: from tcs12.dsto.oz by itd0.dsto.oz (4.1/SMI-3.2) id AA14745; Thu, 21 Feb 91 09:36:02 CST Date: Thu, 21 Feb 91 09:36:02 CST From: cant@au.oz.dsto.itd (Tony Cant) Message-Id: <9102202306.AA14745@itd0.dsto.oz> To: info-hol@edu.ucdavis.clover Subject: Security Sender: cant If there are any HOL users out there who have worked on security policy models using HOL, or have used HOL to study other aspects of computer security, we would very much like to hear from you by email. Our interest is in formalising proofs of security within HOL for general models of security. Thank you Tony Cant (email cant@itd.dsto.oz.au) Katherine Eastaughffe (email kae@itd.dsto.oz.au) Trusted Computer Systems Group Information Technology Division Defence Science and Technology Organisation GPO BOX 1600 SALISBURY 5108 Australia