From: Steve_Brackin@va.arca.com (Steve Brackin) To: schumann@informatik.tu-muenchen.de Cc: softverf@leopard.cs.byu.edu Subject: Re: looking for tools for formal dev. of Protocols Date: 10 Apr 1996 19:11:41 GMT Organization: Arca Systems, Inc Sender: owner-softverf@leopard.cs.byu.edu Precedence: bulk Reply-To: Steve_Brackin@va.arca.com (Steve Brackin) Content-Type: text Content-Length: 2374 Wow, do I have tools for you! I've developed a HOL theory formalizing a significantly extended version of the Gong, Needham, Yahalom belief logic describing authentication properties of cryptographic protocols, developed a collection of HOL tools for automatically proving that protocols have desired properties, developed a simple Interface Specification Language (ISL) for specifying protocols and their desired properties, and developed a Yacc-based translator for converting ISL into HOL and invoking the automatic proof process. These tools also produce output files giving the results of proof attempts in ISL, so the user does not have to know anything about HOL. I'm in the process of trying to publish several papers on these results. So far, all I've heard are acceptances, for two papers and a tutorial proposal. Here are the papers I've submitted: S. Brackin. A HOL Extension of GNY for Automatically Analyzing Cryptographic Protocols. To appear in the 9th IEEE Computer Security Foundations Workshop, County Kerry, Ireland, June 10-12, 1996. S. Brackin. Deciding Cryptographic Protocol Adequacy with HOL: The Implementation. Submitted to the the 1996 International Conference on Theorem Proving in Higher Order LogicS, Turku, Finland, August 27-30, 1996. S. Brackin. An Interfae Specification Language for Cryptographic Protocols and Its Translation into HOL. Submitted to the New Security Paradigms Workshop, Lake Arrowhead, CA, September 16-19, 1996 S. Brackin. Automatic Formal Analyses of Cryptographic Protocols. Submitted to the 19th National Information Systems Security Conference, Baltimore Convention Center, Baltimore, MD, October 22-25, 1996 S. Brackin and R. Lichota. CASE for High Assurance: Utilizing Commercial Technology for Automatic Cryptographic Protocol Analysis. To appear in the Dual-Use Technologies and Applications Conference, Information Management Collections Processing and Distribution, Utica, NY, June 4-6, 1996. I can provide gzipped, uuencoded PostScript for any of these papers to anyone who wnts them. I'll need to check with my company, but so far we've also been treating the tools themsel ---------------------------------------------------------------------- Arca Systems, Inc. Secure Enterprise Solutions ---------------------------------------------------------------------- From: Steve_Brackin@va.arca.com (Steve Brackin) To: schumann@informatik.tu-muenchen.de Cc: softverf@leopard.cs.byu.edu Subject: Re: looking for tools for formal dev. of Protocols Date: 10 Apr 1996 19:21:56 GMT Organization: Arca Systems, Inc Sender: owner-softverf@leopard.cs.byu.edu Precedence: bulk Reply-To: Steve_Brackin@va.arca.com (Steve Brackin) Content-Type: text Content-Length: 592 Because of a mailer error, the last couple of paragraphs in the reply I just sent were deleted. They said that my PRISM collegues Randy Lichota and Grace Hammonds have also submitted a paper on these results that I don't have but can obtain, and that I'll have to check but believe I can give free copies of the tools to anyone who wants them. Steve Brackin Arca Systems, Inc. ---------------------------------------------------------------------- Arca Systems, Inc. Secure Enterprise Solutions ---------------------------------------------------------------------- X-Return-Path: news To: sophia-centaur@sophia.inria.fr Path: capa.inria.fr!thery From: thery@capa.inria.fr (Laurent Thery) Newsgroups: sophia.centaur Subject: Re: VHDL, HOL Date: 17 May 1995 09:22:15 GMT Organization: INRIA, Sophia-Antipolis (Fr) Lines: 48 Distribution: world NNTP-Posting-Host: capa.inria.fr Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit >> We are currently working on "Formal Specifications" for Hardware design. >> We have already been working on VHDL, developping a parser with Centaur and >> we are >> looking for more informations on HOL, CHOL, HOL & VHDL .... >> >> Could someone indicate to me, some pointers to these topics. o HOL is a theorem prover initially developed at Cambridge by Mike Gordon. HOL has been largely applied to hardware verification (VHDL, ELLA etc..) A html pointer for HOL is: http://lal.cs.byu.edu/lal/hol-documentation.html If you are interested in papers, you can have a look at the proceedingss of their conference: HOL: Higher Order Logic and its applications (the last two proceedings have been published as LNCS). o CHOL is an interface for HOL that I've been developped using some components of the Centaur system. It only supports proof management. A html pointer for CHOL is: http://www.inria.fr/croap/chol/chol.html o HOL & VHDL: an embedding of a subset of VHDL in HOL has been done by John Van Tassel for his thesis. It is available as a Cambridge technical report or by ftp: ftp://ftp.cl.cam.ac.uk/hvg/papers/JVTthesis/ a shorter version has been published in the HOL conf in Lewen in 1992. -- Laurent Thery Phone (33) 93 65 78 16 e-mail thery@inria.fr Projet Croap INRIA - Sophia Antipolis, 2004, rte des Lucioles, 06565 Valbonne Cedex, FRANCE