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:


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:

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.

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.

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),

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.

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:

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.

See also get_option

get_option(Option,State)

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

See also set_option

show_options

The predicate show_options shows all the options available and their state

See also get_option, set_option


Syntax of the history

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

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

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


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

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.

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:

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

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

  • 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 AlLoWS, 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, 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/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.

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


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.