SCIFF User's Manual

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:

howto Getting started
projects
options
Syntax of the history
Syntax of ics
Syntax of sokb
fdet: improving performance
allows: a framework for testing conformance of web services

Getting Started

Load SICStus or SWI, then consult or compile sciff.pl. For maximum performance, in SWI use

set_prolog_flag(optimise,true). and then compile(sciff). In SICStus, use compile(sciff).

Create a project, following the indications in projects.

Using Projects

In order to create a new project:

Create a directory with the name of the project in the path specified in the file defaults.pl (it is the father of the directory where is SCIFF, by default).
E.g., suppose the project is myprj, from SCIFF directory: mkdir ..\myprj (Windows syntax)
Copy the file project.pl in the created directory.
E.g., copy project.pl ..\myprj
Edit the file ..\myprj\project.pl with a text editor
Insert the appropriate names in the facts 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’). You may also add required options adding facts required_option/2 (see options).
Create in directory ..\myprj the history file, the sokb file, and the ics file.

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

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

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.

In a closed derivation, after processing the input history, SCIFF makes a closed world assumption on the set of happened events. Thus, it assumes that no more events will happen. This assumption allows SCIFF to detect violation of E expectations. If another event happens after the closed world assumption, the derivation fails.
In an open derivation, no such assumption is made. Thus, SCIFF does not detect violation of E expectations (unless a deadline has passed). More events can happen without causing a failure.

To run SCIFF with an open derivation, use run_open

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.

In a closed derivation, after processing the input history, SCIFF makes a closed world assumption on the set of happened events. Thus, it assumes that no more events will happen. This assumption allows SCIFF to detect violation of E expectations. If another event happens after the closed world assumption, the derivation fails.
In an open derivation, no such assumption is made. Thus, SCIFF does not detect violation of E expectations (unless a deadline has passed). More events can happen without causing a failure.

To run SCIFF with a closed derivation, use run_closed

min_viol_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

min_viol_open(Num,CHRList),

Known bug: the number of violations is not precise: often the reported number of violations should be increased by 1.

project/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

default_dir

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('../').

Options

The following options are recognised by the SCIFF proof-procedure:

fulfiller
seq_act
factoring
sciff_debug
violation_causes_failure
graphviz
allow_events_not_expected
min_viol_closed
min_viol_open
coloring

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.

fulfiller

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

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.

factoring

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.

sciff_debug

Print on screen debug messages.

Usually is off.

violation_causes_failure

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.

graphviz

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.

allow_events_not_expected

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.

Default value is yes.

coloring

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

The output of SCIFF includes the implications that remain at the end of the derivation. Some of these implications are the original Integrity Constraints (IC), others are partially solved integrity constraints (PSIC). The integrity constraints have an internal representation as atoms ic(Body,Head), and they will be shown as such whenever the 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.

By default, portray_ic is on.

set_option(Option,Value)

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.

get_option(Option,State)

You can inspect the state of an option using the predicate: sciff_option(?Option, ?State).

show_options

The predicate show_options shows all the options available and their state

Syntax of the history

The history is a file containing Prolog facts, given with one of the following syntaxes:

either as hap/2 facts (the first argument being a term, the second is the time, i.e., an integer number)
or as Apache Combined Log Format
or as follows.

In the last syntax, events are terms with a Functor and the following arguments:

A list containing a constant
Dialog Identifier (constant)
Sender (constant)
Receiver (constant)
Performative (constant)
Arguments of the performative (List of Terms)
Time (integer)

The term should be terminated with full stop.

It will be converted into an atom

H(Functor(Sender,Receiver,Performative(Arguments),DialogID),Time).

Apache Combined Log Format

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:

H(log(IP,Ident,UserID,ReadableTime,Request,Status,Size,Referer,Browser),T)

where

IP: the IP address of the requesting machine. It is a 32-bit integer number (e.g., 3232235770, not 192.168.0.250)
Ident: the identity of the client (highly unreliable, as stated in Apache documentation)
UserID: User ID. Currently not implemented
ReadableTime: Time in human-readable format: a term time(Day/Month/Year,Hour/Min/Sec,TimeZone)
Request: The request to the server. It is a term get/1 or put/1, containing a list of atomic constants. E.g., "GET /Info1/dummy.gif HTTP/1.1" is provided as get(['Info1',dummy,gif]). The protocol version is currently discarded
Status: the status code that the server sends back to the client (integer)
Size: size of the object returned to the client
Referer: a list of atomic constants. E.g.: http://linuxsrv.lab2007.ing.man/Info1/consegna.php?Action=upload is provided as [http,linuxsrv,lab2007,ing,man,'Info1',consegna,php,'Action',upload].
Browser: the identifying information that the client browser reports about itself. It is provided as a code-list in SICStus syntax (i.e., an unparsed string).
T is the time, in integer format

Syntax of ICs

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 where Body is a conjunction of

literals H (happened events) and their negation !H
expectations E (expected to happen), EN (expected not to happen) and their default negation !E and !EN
abducibles ABD
clp constraints
atoms defined in the SOKB.

Head is a disjunction of conjunctions. Disjunctions are represented wih the symbol \/ , and conjunctions with /\ .

Each conjunct can be

an expectation E (expected to happen), EN (expected not to happen) or their default negation !E and !EN
an abducible ABD
a clp constraint
a literal defined in the SOKB.

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.

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 ics_file/1 predicate. The user should load the ruleml_parser library before loading the project, i.e.:

?- use_module(library(ruleml_parser)).
?-project(...).


 
SCIFF will try to parse
the file first as a RuleML file. In case of failure, it will use the normal
ICs parser.


Syntax of SOKB
The SOKB is a set of clauses, a la logic programming. Each clause is
an implication
head :- body.
where head is an atom and body is a conjunction
of literals, that can contain abducibles and clp constraints.

The abducibles can be expectations or general abducibles.
The syntax of abducibles is different from that of ics, and
is the following:


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


The funcor symbols 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.

The SOKB can be defined in one or more files.
Each sokb file should be declared in the project.pl in a fact
sokb_file(Name_Of_SOKB_File).

Exactly one of the SOKB files should define the predicate 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
Currently, the set of CLP constraints that are interpreted in the
ics is the following:
 
 == (equality)
 <> (disequality)
 >= (greater than or equal to)
 > (greater than)
 =< (less than or equal to)
 < (less than)
 <> (different from)
:: (membership; the second argument should be a ground list)

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. 


fdet declarations
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 
E(message(S,R,type),T) can be fulfilled at most by one event. 
For instance, if in a protocol we have that
E(message(S1,R1,type),T1) ∧ E(message(S2,R2,type),T2) → S1=S2 ∧ R1=R2 ∧ T1=T2 
then we know that only one event can fulfill an E expectation matching with
E(message(S,R,type),T).
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 fdet/1.
In the example, add to the SOKB the definition:

fdet(e(message(S,R,type),T)). 
Of course, if one E expectation can be matched by
more than one H event, declaring it as fdet undermines completeness,
i.e., some solutions may be lost. 

AlLoWS

A^lLoWS (Abductive Logic Web-service Specification)
is a framework for testing conformance of web services to choreographies
(see publication PPDP 2006).
In order to use A^lLoWS, you have to

Define the interface behaviour of the web service under test. This is done by
defining SOKB and ics. 
The name of the web service under test must be declared in the SOKB in a
fact testing/1. E.g., add to the SOKB testing(ws).
Define the choreography, again by defining a SOKB and ics

In A^lLoWS, expectations are only positive (E)
and have the following syntax:
E(do(Expecter,Sender,Receiver,Message,DialogID),Time)
where Expecter can be either chor (i.e., this is an expectation of the
choreography), or the name of the web service under test (in the example, ws)
The 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).
Build the project, with the predicate project
Finally, you can execute the goal allows(Succeed), or redefine, in the
file project.pl (see projects) the
predicate run as follows:
run(Succeed) :- allows(Succeed).
If the web service is not conformant, A^lLoWS 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/1.

If Succeed=false, predicate allows/1 will fail in case
the web service is not conformant
if Succeed=true, predicate allows/1 will succeed
in all cases, useful to inspect the constraint store and have more information
about the history that proves non compliance
if Succeed = verbose, allows/1 prints all the possible histories.
  
A^lLoWS 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 

allow_events_not_expected = yes
(default) → Feeble conformance
allow_events_not_expected = no
→ Strong conformance.



pretty_print
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

[pretty_print].

and the output of SCIFF will be more readable.


svg
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

run_predicate, svg(OutFile,Anim,Options)

where run_predicate is one of run, run_open 
or run_close.

OutFile is the name of the output file, e.g., 'result.svg'
Anim can be either 'no' or 'anim(Sec)'. Two different types of graphs are
visualised. In the second, there is an animation lasting Sec seconds. Note that
currently Firefox does not support SVG animations, Opera does.
Options is a list that can contain zero or more of the following constants:

grid: visualise a grid
history: visualise the history
exp: visualise expectations (only E expectations currently shown)





help
To get help, type help(topic) at the SICStus prompt.
The available topics (links) are represented between stars,
as in the following example:
options
Note that topics names are case-sensitive.

To access the developer's manual, type either devman. or devman(topics). at the SCIFF prompt,
or read devman.html from the documentation.