This version of SCIFF runs on SICStus 4 and following and on SWI 5. Not all the features are available for both systems.
To get help, type help(topic) at the SICStus prompt. To get help on help, type help(help).
Help available on the following topics:
Load SICStus or SWI, then consult or compile sciff.pl. For maximum performance, in SWI use
set_prolog_flag(optimise,true).
compile(sciff).
compile(sciff).
Create a project, following the indications in projects.
In order to create a new project:
mkdir ..\myprj
(Windows syntax)
copy project.pl ..\myprj
ics_file/1,
history_file/1, sokb_file/1
.
The facts ics_file/1,
history_file/1, sokb_file/1
can contain either the path to a file,
or the URL of the file; in the second case, SCIFF will download the file from
the web. The URL should be given as an atomic term, i.e., with single quotes ’,
and should begin with ’http:’. E.g.,
ics_file(’http://lia.deis.unibo.it/Research/sciff/ic.ruleml’).
required_option/2
(see options).
Now you can build the project, calling the goal
project(myprj).
and run it with run(X)
, or run_close(X)
.
See also project, run, run_open, run_close
run/1 is the predicate that runs a project.
The argument is currently not bound by default. By default, this predicate runs SCIFF in a closed derivation (see run_closed). The developer of the project can redefine this predicate in the project file (see projects) and use the parameter for input or output.
run_closed/1 runs a project with a closed derivation.
The argument is currently not bound by default. The developer of the project can redefine this predicate in the project file (see projects) and use the parameter for input or output.
SCIFF can be run either with a closed or with an open derivation.
To run SCIFF with an open derivation, use run_open
run_open/1 runs a project with an open derivation.
The argument is currently not bound by default. The developer of the project can redefine this predicate in the project file (see projects) and use the parameter for input or output.
SCIFF can be run either with a closed or with an open derivation.
To run SCIFF with a closed derivation, use run_closed
min_viol_closed(Num,CHRList),
amongst the various branches selects the one with the minimal
number of violations. Returns the number of violations and the List of CHR
constraints (containing expectations, etc.) in the best node.
Note that this predicate does not print the CHR store, so the only way to get
the output is to use CHRList (if you invoke min_viol_closed(_,_) you get no
output).
Useful when used in conjunction with the option
violation_causes_failure → no.
Known bug: the number of violations is not precise: often the reported number of violations should be increased by 1.
min_viol_open(Num,CHRList),
amongst the various branches selects the one with the minimal
number of violations. Returns the number of violations and the List of CHR
constraints (containing expectations, etc.) in the best node.
Note that this predicate does not print the CHR store, so the only way to get
the output is to use CHRList (if you invoke min_viol_closed(_,_) you get no
output).
Useful when used in conjunction with the option
violation_causes_failure → no.
Known bug: the number of violations is not precise: often the reported number of violations should be increased by 1.
The predicate project(name)
builds a project called 'name'.
There must exist a corresponding directory called 'name', as a subdirectory of the default_dir and it must contain a file called project.pl
Such file should be created as explained in section projects
The default directory where SCIFF looks for projects is declared in the file
defaults.pl
This file contains a fact default_dir
that contains the path
of the directory containing projects. By defult, it is the father of the
directory containing SCIFF; i.e., by default defaults.pl
contains default_dir('../').
The following options are recognised by the SCIFF proof-procedure:
Options can be stated in projects by adding to the file project.pl a
fact required_option/2
. For example, if your project requires
the option seq_act
, add to the corresponding project.pl the fact:
required_option(seq_act,on).
To set an option, use set_option
To read the state of an option, use get_option or show_options.
The fulfiller option enables the generative version of SCIFF (called g-SCIFF,
see [Alberti et al.
Security protocols verification in abductive logic programming: a case study,
ESAW 2005]).
Operationally, after close_history
, for each positive expectation
that is still pending e(X,T)
the corresponding atom h(X,T)
is abduced, fulfilling the expectation.
seq_act option imposes that two events cannot happen at the same time.
If seq_act is on, two events cannot happen at the same time.
If seq_act is off, more events can happen at the same time.
This option is primarily used in the Abductive Event Calculus.
Usually is off.
Note: this option is not necessary (from a declarative viewpoint), because you can easily add an integrity constraint stating that two events should not happen at the same time. The option is provided here because it has a possibly more efficient behaviour with the CLP(FD) solver. However, it does nothing when using the CLP(R) solver.
The factoring option enables or disables the factoring transition. The factoring transition tries and unifies two abduced atoms. On backtracking, the two abducibles are dis-unified. The factoring transition is useful for obtaining minimal answers. It is important for the Abductive Event Calculus.
The factoring option is off by default.
Print on screen debug messages.
Usually is off.
The option violation_causes_failure Decides if a violation of the protocol should induce a failure (and backtracking where possible) of the proof. Allowed values are yes/no. Default value is yes.
Represents the SCIFF derivation tree in form of a graph, using the graphviz software.
The file should be opened with init_graph(FileName,Stream)
,
and, after the execution of the proof, it should be closed with close_graph
.
The produced file can be opened with DOT and converted in PostScript or other formats.
Default value is off.
By default, SCIFF allows events to happen even if they are not expected.
By setting the allow_events_not_expected
option to no
, SCIFF detects as violation if an
happened event does not have a corresponding expectation.
Useful, in particular, to prove Strong Conformance in the allows framework.
When this option is on
, the output of SCIFF uses colors and text styles
(underlined, bold, ...) to improve readability.
In particular, the special SCIFF atoms are colored (E, H, EN, ...).
In SWI, variables are also colored; Universal variables are Magenta, while existential are blue; flagged variables are underlined.
Coloring uses the ANSI codes, so it is available only on those systems that use ANSI codes. It works correctly in Linux and in MacOS, while it does not work in Windows XP. For this reason, by default coloring is enabled in Unix and MacOS, while it is disabled in Windows. However, it can be enabled or disabled with set_option.
portray_ic
option is off
.
When the portray_ic
is on
, the IC are shown with
the same syntax of ics.
In the same way, PSIC are shown with their internal representation when
portray_ic
is off
, and with the syntax of IC when it is on
.
If option coloring is on, IC are represented with a red implication symbol,
while in PSIC the implication symbol is cyan.
Each option can be set using the predicate:
set_option(Option,Value)
where Option is the name of the option you want to modify, and Value is the new value you want to assign to it.
See also get_option
You can inspect the state of an option using the predicate: sciff_option(?Option, ?State).
See also set_option
The predicate show_options shows all the options available and their state
See also get_option, set_option
The history is a file containing Prolog facts, given with one of the following syntaxes:
hap/2
facts (the first argument being a term, the second is the time,
i.e., an integer number)
The term should be terminated with full stop.
It will be converted into an atom
SCIFF is able to parse the access_log file of the Apache web server. The intended use is to verify if the access policies are respected. The recognized format is the Combined Log Format.
In order to read the history from the access log, the file should be loaded in
the project file, with the usual history_file declaration. SCIFF recognizes that the
history is an access log from the name of the file in the file declaration.
If the filename terminates with access_log
, then the parser of
the access log is activated. E.g., the project file could have a fact:
history_file(monday.access_log).
The H events that SCIFF receives have the following format:
where
time(Day/Month/Year,Hour/Min/Sec,TimeZone)
get(['Info1',dummy,gif])
.
The protocol version is currently discarded
The ICs are the Integrity Constraints of the SCIFF proof-procedure.
They are written in one (or more) text files that should be declared
in the file project.pl (see projects) with a fact ics_file(Filename).
ICs are in the form of implications:
Body ---> Head
Head is a disjunction of conjunctions. Disjunctions are represented wih the
symbol \/
, and conjunctions with /\
.
Each conjunct can be
For example, the following is a valid IC:
% happened events
H(tell(A,B,openauction(Item,TEnd,TDeadline),AuctionId),TOpen)
/\ H(tell(B,A,bid(Item,Quote),AuctionId),TBid)
/\ deadline(X) % Literal defined in SOKB
/\ TOpen < TBid % CLP constraints
/\ TOpen <= TEnd
/\ TEnd < TDeadline+X
--->
E(tell(A,B,answer(win,Item,Quote),AuctionId),TWin)
/\ TWin <= TDeadline
/\ TEnd < TWin
\/
E(tell(A,B,answer(lose,Item,Quote),AuctionId),TLose)
/\ TLose <= TDeadline
/\ TEnd < TLose.
Comments are represented with the ampersand symbol (%) and terminate at the end of the line (as in Prolog). The IC terminates with a full stop.
As an alternative, ICs can also be defined in ruleml.
As an alternative to the syntax of ics, it is possible to define the ICs with the syntax in RuleML 0.9.
RuleML files are declared in the project file with the same syntax of normal
ICs files: using the SCIFF will try to parse
the file first as a RuleML file. In case of failure, it will use the normal
ICs parser.
The SOKB is a set of clauses, a la logic programming. Each clause is
an implication
The abducibles can be expectations or general abducibles.
The syntax of abducibles is different from that of ics, and
is the following:
The funcor symbols The SOKB can be defined in one or more files.
Each sokb file should be declared in the Exactly one of the SOKB files should define the predicate Currently, the set of CLP constraints that are interpreted in the
ics is the following:
as well as unification = and dis-unification !=.
<> and != have the same declarative semantics; however <> is
intended as disequal amongst integers, while != is better suited for disunification
between terms.
In order to test if an E expectation is fulfilled by a
H event, SCIFF generates two alternative hypotheses:
in one it tries to prove that the two will unify, while in the second it tries
and prove that they will not unify.
In some cases, the protocol specification might implicitly impose that
all expectations of type In such cases, the performance can be improved by declaring such event as
having deterministic fulfilment.
This can be accomplished by adding to the SOKB a predicate Of course, if one E expectation can be matched by
more than one H event, declaring it as AlLoWS (Abductive Logic Web-service Specification)
is a framework for testing conformance of web services to choreographies
(see publication PPDP 2006).
In order to use AlLoWS, you have to
In AlLoWS, expectations are only positive (E)
and have the following syntax:
where Expecter can be either The Build the project, with the predicate project
Finally, you can execute the goal If the web service is not conformant, AlLoWS provides,
as counterexample, a possible
history that does not satisfy either the web service's or the choreography's
specifications.
The parameter Succeed is useful to drive the behaviour of the predicate
AlLoWS can prove two types of conformance, named Feeble and
Strong conformance (see publication PPDP 2006). The two types of proof
are distinguished by means of the option (see options)
allow_events_not_expected
The module pretty_print is not loaded by default.
If it is, it makes the output of SCIFF more readable.
It is not loaded by default because some external programs capture the output
of SCIFF, so we recommend using it only if you run SCIFF as a stand-alone
procedure (not with SOCS-SI or SCIFF Editor).
To use pretty_print, simply consult it with The output of SCIFF can be saved in SVG format, readable with modern
browsers, such as Opera or Firefox, or with the Adobe plugin for other browsers.
To use SVG output, invoke the goal To get help, type help(topic) at the SICStus prompt.
The available topics (links) are represented between stars,
as in the following example:
Note that topics names are case-sensitive.
To access the developer's manual, type either ics_file/1
predicate.
The user should load the ruleml_parser
library before loading the project
, i.e.:
?- use_module(library(ruleml_parser)).
?-project(...).
Syntax of SOKB
head :- body.
head
is an atom and body
is a conjunction
of literals, that can contain abducibles and clp constraints.
e(Event,Time)
is a positive expectation
note(Event,Time)
is a negated positive expectation (i.e., the default
negation of a positive expectation)
en(Event,Time)
is a negative expectation
noten(Event,Time)
is a negated negative expectation (the default
negation of en)
abd(Term,Time)
is a general abductive atom
e, note, en, noten, abd
and h
are reserved: if you define a predicate e/4
you will not be able to
use it in the ICs.
project.pl
in a fact
society_goal/0
.
The predicate society_goal
contains the goal of the society,
that is the starting point of SCIFF derivation.
society_goal
is invoked by the run, run_open and
run_closed
predicates that start the derivation.
CLP Constraints
fdet declarations
fdet/1
.
In the example, add to the SOKB the definition:
fdet(e(message(S,R,type),T)).
fdet
undermines completeness,
i.e., some solutions may be lost.
AlLoWS
testing/1
. E.g., add to the SOKB testing(ws).
chor
(i.e., this is an expectation of the
choreography), or the name of the web service under test (in the example, ws
)
society_goal
should be defined only once (in either of the
two SOKBs), and should contain the expectation, both from the choreography
and from the web service's viewpoint, of the message that initiates
the interaction. For example:
society_goal:-
e(do(ws, peer,ws,m1,d1),1),
e(do(chor,peer,ws,m1,d1),1).allows(Succeed)
, or redefine, in the
file project.pl
(see projects) the
predicate run as follows:
run(Succeed) :- allows(Succeed).
allows/1
.
allows/1
will fail in case
the web service is not conformant
allows/1
will succeed
in all cases, useful to inspect the constraint store and have more information
about the history that proves non compliance
allows/1
prints all the possible histories.
pretty_print
[pretty_print].
and the output of SCIFF will be more readable.
svg
run_predicate, svg(OutFile,Anim,Options)
where run_predicate is one of run, run_open
or run_close.
help
devman.
or devman(topics).
at the SCIFF prompt,
or read devman.html from the documentation.