proverif用户文档_proverif语法

安全

软件

需积分: 50 384 浏览量更新于2023-05-31 评论收藏 196KB PDF 举报

身份认证购VIP最低享 7 折!

领优惠券(最高得80元）

资源详情

资源评论

资源推荐

ProVerif

Automatic Cryptographic Protocol Veriﬁer

User Manual for Untyped Inputs

Bruno Blanchet

∗

INRIA Paris-Rocquencourt, France

May 15, 2018

Warning! This manual documents the untyped inputs of ProVerif (untyped Horn clauses, untyped

pi calculus). These input formats are no longer actively developed. We recommend coding your protocols

in the typed pi calculus format, described in the ﬁle manual.pdf.

1 Introduction

This manual describes the untyped input s yntax and output of ProVerif. It does not describe the internal

algorithms used in the system. These algorithms have been described in various research papers [6, 2, 7,

1, 3, 4, 8, 10, 5, 9], that can be downloaded on

http://www.di.ens.fr/~blanchet/publications/index.html.

The tool can take two formats as input. Th e ﬁrs t one is in the form of Horn clauses (logic programming

rules), and corr e s ponds to the system described in [6]. The secon d one is in the form of a proces s in an

extension of the pi calculus, described in [2]. In both cases, t he output of the system is essentially the

same.

2 Common remarks on the syntax

Comments can be included in input ﬁles. Comments are surrounded by (* and *). Nested comments

are not supported.

Identiﬁers begin with a letter (uppercase or lowercase) and contain any number of letters, digits, the

underscore character (

), the quote character (’), as well as accented letters of the ISO Latin 1 character

set. Case is signiﬁcant. Each input system has a number of keywords that cannot be used as ordinary

identiﬁers.

In case of syntax error , the system indicates the character position of the error (line and column

numbers). Please use your text editor to ﬁnd the position of the error. (The error messages can be

interpreted by emacs.)

3 Command-line options

The syntax of t he command-line is

./proverif hoptionsi hﬁlenamei

where the hoptionsi can be

∗

This work was partly done while the author was at

Ecole Normale Sup´erieure, Paris and at Max-Planck-Institut f¨ur

Informatik, Saarbr¨ucken.

• -in hformati

Choose the input format (horn, horntype, pi, pitype). When the -in option i s absent, th e input

format is chosen according to the ﬁle exte ns ion, as detailed below. The recommended input format

is the typed pi calculus, which corresponds to the option -in pitype, and is the default when

the ﬁle extension is .pv. It is described in manual.pdf. The other formats are no longer actively

developed. Input may also be provided using the untyped pi c alcu lu s (option -in pi, the default

when the ﬁle extension is .pi), typed Horn clauses (option -in horntype, the default when the

ﬁle extension is .horntype), and untyped Horn clauses (option -in horn, the default for all other

ﬁle extensions). This manual documents the untyped Horn clauses and the untyped pi calculus

input formats.

• -out hformati

Choose th e output format, e it he r solve (analyze the protocol) or spass (stop the analysis before

resolution, and outpu t the clauses in the format required for us e in the Spass ﬁrst-or de r theorem

prover, see http://www.spass-prover.org/). The default is solve. When you select -out spass,

you must add the option -o hﬁlenamei t o specify the ﬁle in which the clauses will be outp ut .

• -TulaFale hversioni

For compatibility with the web service analysis tool TulaFale (see the tool download at http:

//research.microsoft.com/projects/samoa/). The version number is the version of TulaFale

with which you would like compatibility. Currently, only version 1 is supported.

• -color

Display a colored output on terminals that support ANSI color codes. (Will result in a garbage

output on ter mi nals that do not support these codes.) Unix terminals typically support ANSI color

codes. For emacs users, you can run ProVerif in a shell buﬀer with ANSI color codes as follows:

– start a shell with M-x shell

– load the ansi-color library with M-x load-library RET ansi-color RET

– activate ANSI colors with M-x ansi-color-for-comint-mode-on

– now run ProVerif in the shell buﬀer.

You can also activate ANSI colors in shell buﬀers by default by adding t he following to your .emacs:

(autoload ’ansi-color-for-comint-mode-on "ansi-color" nil t)

(add-hook ’shell-mode-hook ’ansi-color-for-comint-mode-on)

• -help or --help

Display a short summary of command-line options.

4 Input as Horn clauses

By default, the executable program proverif takes Horn clauses as input. You can run it as follows:

./proverif hﬁlenamei

where hﬁlenamei references a ﬁle containing the Horn clauses, in the format explained below. The system

then b asi cally deter min es whether a fact can be derived from the clauses. If true, a proof is given. As

shown in [6], this can be used to determine secr e cy properties of protocols: if a c er tain fact cannot be

derived from the clauses, then the secrecy of a certain value is preserved. A diﬀerence with ﬁrst-order

theorem provers that perform a similar task, is that correctness and completeness are r eversed. Here,

correctness means that if a value is not secret, the system says so, that is, if a fact is derivable, the system

says so. Completeness means that if a fact is not derivable, then the system says so. We sometimes dr op

completeness (that is, we lose precision; see options below), but never correctness.

– param verboseTerm = true.

param verboseTerm = false.

Display information on termination when true (changes in the selection function to improve

termination; termin ation warnings).

– param maxDepth = none.

param maxDepth = n.

Do not limit the depth of terms (none) or limit the depth of terms to n, where n is an integer.

A negative value means no limit. When the depth is limited to n, all terms of depth greater

than n are replaced with new variables. Limiting the depth can be used to enforce termination

of the solving process at the cost of precision.

– param maxHyp = none.

param maxHyp = n.

Do not limit the number of hypotheses of clauses (none) or limit it to n, where n is an

integer. A negative value means no limit. When th e number of hypoth es e s is limited to n,

arbitrary hypotheses are removed from clauses, so that only n hypotheses remain. Limiting

the number of hypotheses can be used to enforce termination of the solving process at the

cost of precision (although in general limiting the depth by the above declaration is e n ough

to obtain termination).

– param selFun = TermMaxsize.

param selFun = Term.

param selFun = NounifsetMaxsize.

param selFun = Nounifset.

Chooses the selection function that governs the resolution process. All selection functions

avoid unifying on facts indicated by a nounif declarati on. Nounifset does exactly that.

Term automatically avoids some other uniﬁcations, to help termination, as determined by

some heuristics. NounifsetMaxsize and TermMaxsize choose the fact of maximum size when

there are several possibilities. This choice sometimes gives impressive spe ed up s .

– param stopTerm = true.

param stopTerm = false.

Display a warning and wait for user answer when the system th in k s the solving process will

not termin ate (true), or go on as if nothing had happen ed (false). This setting applies only

to the selection functions NounifsetMaxsize and Nounifset. (See parameter selFun.)

– param redundancyElim = simple.

param redundancyElim = no.

param redundancyElim = best.

An elimination of redundant clauses has been implemented: when a clause without sele cte d

hypotheses is derivable from other clauses without selected hypothesis, it is removed. With

redundancyElim = simple, this is applied for newly generated clauses. With redundancyElim

= no, this is never applied. With redundancyElim = best, this is also applied when an old

clause can be derived fr om other old clauses plus the new clause.

– param redundantHypElim = beginOnly.

param redundantHypElim = false.

param redundantHypElim = true.

When a clause is of the form H ∧ H

′

→ C, and there exists σ such t hat σH ⊆ H

′

and σ does

not change the variables of H

′

and C, then the clause can be replaced with H

′

→ C (since

there are implications in both directions between these clauses).

This replacement is done when redundantHypElim = true., or when redundantHypElim =

beginOnly. and H contains a begin event. Indeed, testing this property takes time, and

slows down small examples. On the other hand, on big examples, in particular when they

contain several begin events (or blocking facts), this technique can yield huge spe ed up s .

– param reconstructDerivation = true.

param reconstructDerivation = false.

剩余19页未读，继续阅读

qq_35737030

粉丝: 0
资源: 1

会员权益专享

proverif用户文档

评论0

会员权益专享

最新资源

proverif用户文档

评论0

ProVerif manual

会员权益专享

最新资源