Subject: Re: looking for tools for formal dev. of Protocols
From: [email-masked] (Steve Brackin)
To: [email-masked]
Cc: [email-masked]
Date: 10 Apr 1996 19:11:41 GMT

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: [email-masked] (Steve Brackin)
To: [email-masked]
Cc: [email-masked]
Subject: Re: looking for tools for formal dev. of Protocols
Date: 10 Apr 1996 19:21:56 GMT
Organization: Arca Systems, Inc 
Sender: [email-masked]
Precedence: bulk
Reply-To: [email-masked] (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: [email-masked]
Path: capa.inria.fr!thery
From: [email-masked] (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 [email-masked]
Projet Croap INRIA - Sophia Antipolis,
2004, rte des Lucioles, 06565 Valbonne Cedex, FRANCE