(Constraint Logic-based ATtack SEarcher)

An automatic tool for protocol and web-services analysis
developped for the European Projects Avantssar & Avispa.

Description and Functionalities#


CL-AtSe [1][2] is a Constraint Logic based Attack Searcher for security protocols and services. The main idea in CL-AtSe consists in running the protocol or set of services in all possible ways by representing families of traces with positive or negative constraints on the intruder knowledge, on variable values, on sets, etc. Thus, each run of a service step consists in adding new constraints on the current intruder and environment state, reducing these constraints down to a normalized form for which satisfiability is easily decidable, and decide whether some security property has been violated up to this point. CL-AtSe does not limit the service in any way except for bounding the maximal number of times a service can be iterated, in the case such an iteration is allowed in the specification. Otherwise, the analysis might be non-terminating on secure services and only heuristics, approximations, or restrictions on the input language could lift this limitation.

If a security property of the input specification is violated then CL-AtSe outputs a warning (UNSAFE), some details about the analysis (e.g. whether the considered model is a typed or an untyped one), the property that was violated (secrecy, for instance), statistics on the number of explored states, and, finally, an ATTACK TRACE that gives a detailed account of the attack scenario. If no attack was found then similar information is provided (but the ATTACK TRACE).

Simplifications and optimizations#

CL-AtSe implements modules to simplify and optimize the input specification statically before analysis. The simplification module aims at reducing the search space without truly changing the structure of the problem to be analyzed. This option is activated by default because the computations involved are quite small compared to the expected gain on the analysis time. The optimization module, on the other hand, tries to change the structure of the input specification to pre-process a significant part of the branching that should be done during analysis, so that many dead-ends can be found and removed statically. This option is not activated by default since, theoretically, in the worst case it might be equivalent to a complete analysis, especially for specifications with weak message structure (e.g. a large number of encryptions with no headers, etc.). However, when the specification is adapted the gain during analysis can be huge. It can be activated with the --opt option.

Support for ASLan#

CL-AtSe reads any specification written in ASLan by default. The only current limitation is limited support for LTL. Horn clauses are supported except for explicit horn clauses with intruder knowledge as consequence instead of facts. We are continuously working on the tool, and we expect to lift the remaining restrictions in a near future. Currently, security goals are rewritten into attack states, for which support in the tool is complete. Significant LTL support for properties based on future time will be added soon. Unlike other backends in the project, the support for horn clauses has been implemented using a backward strategy. This means that the termination conditions are different for CL-AtSe than for other backends: a specification can be analyzed when it's horn clauses do not loop infinitely when recursively applied from consequences to conditions on facts required to run the protocol/service. For other backends, the same conditions must hold but from conditions to consequences when applied on facts produced by the protocol run. This difference of strategy is an advantage: one specification can loop with one tool but go through softly with an other. Moreover, whatever the strategy the tools must not disagree.

Support for the Output Formats#

Cl-AtSe can optionally output the analysis result in the new Output Format defined by the project. This include showing which rule and horn clauses have been used to construct an attack trace. Only low-lever horn clauses coding internal intruder's actions (w.r.t. its knowledge, etc..) are not shown and cannot be because they are hard-coded inside the analysis methods. Moreover, various other output formats are supported: the old output format from the AVISPA project is still supported; two additional levels of verbosity are supported over the standard output format, providing detailed informations about the protocol and the analysis; and two additional levels of conciseness are supported, to have a quick view of the analysis's result. A benchmarking mode is also supported, which can run many instances of (e.g. different versions of) the tool on a set of specifications to compare results.

Support for stop and restart#

Cl-AtSe is capable to stop and restart later an analysis, by writing and reading a so-called state file containing the current state of the analysis. This can be produced either anytime during a very long analysis to resume e.g. in case of power loss, and this can be used each time an attack is found to store the state of the system without the attack, and thus, resume the analysis to find other attacks (either on the same branch with other constraints, or on other branches). The latter is used by the AVANTSSAR Orchestrator to enumerate orchestrations. Cl-Atse take care not to produce new attacks which would admit an attack already found as a prefix. Finally, the stop-and-restart functionality is used for massive parallel computing: with the appropriate option, Cl-AtSe can advance a bit in a protocol's analysis before stopping and writing one state file per branch that still need to be analyzed. This can produce as many sub-state files as needed, and each can be analyzed independently from others by Cl-AtSe, e.g. on different CPUs or PCs.

Context of execution#

Properties and Limitations#

The Cl-AtSe model checker analyzes Avantssar's ASLan v1 files w.r.t. a bounded number of "sessions". The tool supports associative (--assoc) or non-associative (--free) pairing symbol, as well as the algebraic properties of xor and exponential. There is no need to include such properties in the specification, these are hard-coded in the tool. Also, both the typed (--typed) and untyped (--untyped) models are supported. The tool is backward-compatible with the Avispa project. It has currently two main limitations w.r.t ASLan: horn clauses with an intruder knowledge in the LHS[2] are not supported, except those coding composition or decomposition of functions; and LTL goals are limited to those that the tool can automatically translate to attack states. Besides that, the support is complete.

Horn Clauses.#

For horn clauses, it is important to know what strategy the tool employ: in Cl-AtSe, this is a backward strategy. This means that horn clauses are used when and only when some fact is required to be build (by e.g. the LHS of a transition). Other tools may employ a forward strategy, where the set of known facts is saturated by horn clauses between each transition. Whatever the strategy used, there are always systems of horn clauses that won't terminate, and thus, the modeler should make sure that the horn clauses in his specification terminate w.r.t the strategy used by the tool used for the analysis.

Bounding Execution.#

A second very important point to be aware of is the option --nb which controls the bound on the number of sessions used during the analysis. Except for e.g. OFMC in non-classical mode, this bound is a need to ensure termination anyway. The definition of sessions is controlled by the --lvl option, but, whatever the definition of session used, the --nb option defines the maximum number of times each transition can be run in a trace. The default value is 1, and thus, it is up to the modeler to correctly adjust this value depending on his specification. For example, if the specification does not use loops, then the default 1 value should be fine; if the specification uses loops but the maximum number of iteration is known in advance (e.g. loops used to avoid writing the same transitions many times), then a value sufficiently large must be provided to ensure that the specification can be run completely; and if the specification uses loops in an unpredictable or infinite way, then the problem is fundamentally undecidable and thus, the modeler should interactively increase the bound until an attack is found or the problem gets too big.

Level of Rebuilding.#

As pointed out above, Cl-AtSe tries by default to extract coherent sessions from the ASLan v1 specification. A session for Cl-AtSe is a (longest) sequence or tree of transitions that is played by one (and only one) agent and where each transition appears only once. The kind of session used by Cl-AtSe is controlled by the option --lvl ('level' of rebuilding). A 0 value is the safe mode where one transition is equal to one session. The values 1 and 2 (default) are two rebuilding methods and should be equivalent. Identifying sessions within an ASLan v1 file may fail due to the structure of the specification: the syntax does not guarantee that simple sessions can be rebuilt, and moreover, sometimes building sessions is equivalent to enumerating all execution traces. In such situation, the tool will fallback to the default --lvl 0 option and write a message like "Forced use of the --lvl 0 option". A successful session rebuilding often means better analysis performances.

Output Formats.#

Many levels of verbosity, or even output syntaxes, are available with Cl-AtSe. Those kind of outputs are controlled by the --of option, which accepts many values: "ASLan" for the standard ASLan output format, as defined in the Avantssar's deliverables; if, if+ and if++ are tree levels of verbosity of an Avispa-like output format, which gives more and more information on the way the specification was understood by the tool; if- gives a condensed view of an attack found, if any; and brief gives an even more elementary view of the result.

Advanced Horn Clause Use.#

For more advanced users, Cl-AtSe allows you some control on the strategy used for horn clauses. Even if the strategy remains backward only, you can control the kind of recursive algorithm used to help the tool to analyze your specification more efficiently. That is, three variants of the horn clauses strategies are available:
  • Backward with Depth-first search : h.c. are used to produce the facts required by a transition, an attack state, or the RHS of an other h.c., in a Depth-first mode. That is, first finish the deductions of the first fact in the list before doing deductions for the next one. Facts are taken in the order they were written in the ASLAN file. Activated by option --hc btd (for BackwardTopDown)
  • Backward with Depth-first search, but with modified ordering (default). This is the same as above, but the tool choose himself the ordering of facts to use, i.e. the tool choose which fact must be deduced first. This will reorder the lists of facts so that the more "interesting" facts are tried first. This is an heuristic, but in the worst case still everything is tested. If you want to control the ordering yourself, please use the other option above. This one can be activated with --hc btd+, and it is the default.
  • Backward with Breadth-first search. Assume you have a set of facts to test. In this mode the tool with make one elementary deduction for each fact, storing the subsequent new facts to produce, and iterate only after all facts have been processed. The advantage is that the ordering is not important anymore in this mode, since you move "layer by layer". The bad consequence however, is that if you are unlucky today, one of your facts may explodes into a huge set of facts before the deductions on an other fact could add the right constraints. However, such conditions are quite particular, and in that case the modeler should choose his fact ordering carefully with --hc btd or thrust the tool with the default --hc btd+. This option is activated with the option --hc blr (for BackwardLeftRight).

To conclude about horn clauses, please note also the existence of an option called --not_hc. Due to structural constraints inside the horn clauses functions in Cl-AtSe, sometimes false attacks might appear where negative tests inside horn clauses was validated while they should not. This is due to the fact that testing such negative tests might require to perform an inversion of a formal state, which is a very complex and costly operation. Thus, until now, this operation is done only when the option --not_hc is provided, instead of just refusing horn clauses using such tests. Note that no false feeling of security can appear here. This option might be activated by default in a near future.

Future developments of Cl-Atse#

While Cl-Atse matured enough to support analysis of Avantssar's industrial case-studies, it's development is is far from being closed and we have important pending additions to the tool that we could not yet investigate. First, the support for Horn Clauses with intruder knowledges in their LHS is not complete and need to be fully supported to ease the use of communication channels and allow more flexibility with the intruder's capabilities. Second, full support of temporal logic-based security properties is structurally complex to add in the tool, but possible, and would greatly extend the expressibility. Third, extensions of the term algebra like e.g. support of explicit destructor would we very useful to integrate the tool with other systems than those of Avantssar. Fourth, one-click use of parallelism is a need to greatly increase performances, both for off-line analysis on multi-cores PCs and for on-line analysis: since the problem is NP-Complete, the gain of speed offered by multi-core parallelism is huge.

[#2] Left-Hand side

AVANTSSAR Backends Benchmark, run on Amazon EC2 servers.

Case Study Specification Tr HC CL-AtSe OFMC SATMC
Car Registration CRP.dyn.aslan (C) 25 52 TO TO 19.23s
CRP.stat.rej.aslan (C) 17 21 0.65s 856.37s 2.63s
CRP.stat.acc.aslan (C) 17 21 0.69s TO 3.89s
crp-statpol.ORCHESTRATED.aslan (C) 22 0 0.73s TO TO
crp-hc.ORCHESTRATED.aslan (C) 22 5 0.81s NS TO
CRP.dyn.meta.aslan (C) 25 52 2.24s 126.47s 3.53s
CRP.dyn.rej.aslan (C) 26 52 2.42s TO 4.96s
CRP.dyn.acc.aslan (C) 26 52 2.48s TO 6.6s
CRP.stat.aslan (C) 16 21 2.78s TO 16.27s
crp-nohc.ORCHESTRATED.aslan (C) 21 0 48.86s TO ERR
Anonymous Shopping IDMXScene1_Safe.aslan (C) 11 30 INC 46.0s NS
IDMXScene1_execTrace.aslan (C) 11 30 0.49s 7.73s NS
IDMXScene2_execTrace.aslan (C) 15 30 1.74s TO NS
Digital Contract Signing dcs-v3-exec1.aslan 39 15 TO NS 128.18s
dcs-v3-exec1-1.aslan 39 15 TO NS 1084.62s
dcs-v1-execFirstSig.aslan 18 15 3.25s NS 3.64s
dcs-v1-exec.aslan 18 15 5.16s NS 14.65s
dcs-v1-secrecy-contract.aslan 18 15 7.99s NS 237.19s
dcs-v1-authentication.aslan 18 13 7.99s NS 2581.39s
dcs-v1-proofOfOrigin.aslan 18 15 8.16s NS TO
dcs-v1-NR.aslan 18 15 8.36s NS 1781.86s
dcs-v1-secrecy-archive.aslan 18 15 8.47s NS 278.02s
dcs-v2-exec2.aslan 30 15 162.85s NS 33.25s
dcs-v1-integrity.aslan 18 15 694.32s NS ERR
Electronic Health Records ECR_SATMC.aslan (C) 23 44 NS 3.06s 19.33s
ECR.aslan (C) 25 45 125.37s TO NS
Loan Origination lobp_new_ntk_attack.aslan 27 16 TO NS 17.86s
lobp_sap_bod_attack.aslan 24 16 TO NS 345.45s
lobp_sap_sod_attack.aslan 24 16 TO NS 354.43s
lop-scene2.aslan 24 16 TO NS 14.09s
lobp_old_substitution_dc_attack.aslan 16 13 0.17s NS 1.45s
lopUGDIST_Safe.aslan 14 16 0.26s NS 7.25s
lobp_new_dc_attack_noUQhc.aslan 27 16 0.74s NS 1.65s
lobp_new_dc_attack.aslan 27 16 0.81s NS 1.81s
lobp_new_sod_noattack.aslan 27 34 9.17s NS TO
lopUGDIST.aslan 14 16 93.59s NS 2.89s
lop-scene1.aslan 14 16 94.65s NS 2.13s
lobp_new_at_attack.aslan 27 16 203.72s NS 14.13s
lobp_sap_at_attack.aslan 24 16 1633.35s NS 14.05s
Public Bidding PBv1_authentication_Unsafe.aslan 30 11 2.53s 2.94s 16.61s
PB_alt_exec.aslan 22 2 7.14s 2.96s ERR
PBv1_exec.aslan 27 8 12.33s NS 35.24s
pb-exec.aslan 36 15 13.29s ERR ERR
PB_alt_secrFP.aslan 22 2 19.9s TO TO
PB_alt_secrTP.aslan 22 2 19.9s TO TO
PB_alt_integr.aslan 22 2 20.01s TO 1937.39s
PB_alt_auth.aslan 22 2 20.09s TO 1762.84s
PB_alt_nonrep.aslan 22 2 20.28s TO 1311.83s
pb-elig.aslan 36 15 285.89s ERR ERR
PBv1_nonRepudiation.aslan 26 8 2154.09s ERR 91.79s
PBv1_integrity.aslan 26 8 2154.77s ERR 94.63s
PBv1_authentication_Safe.aslan 26 8 2158.61s ERR 138.15s
PBv1_secrecy.aslan 26 8 2409.87s ERR 250.77s
Visa Application PTD_VisaBank.aslan (C) 19 38 9.86s 3.12s 44.83s
Process Task Delegation PTD.aslan (C) 18 43 323.83s NS TO
PTD_PC.aslan (C) 21 47 768.6 s NS TO

Tr : number of transitions; HC : number of Horn clauses; NS : Not Supported; ERR : Error; TO : Timeout; INC : Inconclusive.

This is ths Cl-Atse Benchmark page

List of binary packages for Cl-Atse#

The supported platforms are Linux and Windows. Sources can certainly be compiled for Mac too, but I don't know any OCaml cross-compiler for Mac on a Linux system. For older binaries, please ask me. All versions are not listed here, but only the major updates.

December 20th, 2014 : Cl-Atse binary package for Linux & Windows 32bits, Dec. 20th 2014(info)#

Release version. Cumulative update for small corrections and improvements. Also, Enhanced a little bit the analysis speed by fusing hypothesis constraints on X (any variable) and inv(X) together. Internally, a constraint like H(inv(X)).E saying that inv(X) must be built from E cannot live without H(X).E' with E' includes E. Moreover, most of the time E=E' so a fused constraint is created when possible, HI(X).E = H(inv(X)).H(X).E, which manages both constraints together in one step. These constraint management functions are critical for the tool, because that's where most of the time is spent, along with unification functions.

Octobre 12th, 2014 : Cl-Atse binary package for Linux & Windows 32bits, Oct. 12th 2014(info)#

Release version. Added support for Horn Clauses with intruder knowledges as consequences. That is, Horn Clauses which extend the intruder capabilities by using the iknows predicate in their left-hand side are now allowed in the tool, and properly used. Horn Clauses in Cl-Atse are evaluated lazily, i.e. by need on the predicate it can provide, while the intruder knowledges are reduced proactively. Still, w.r.t. some restrictions preventing infinite looping, such Horn clauses are now accepted by the tool. For example, this was used to model the properties of stacks of operators, i.e. when the intruder can deduce something from e.g. f(g(x)) but not from f or g alone. Other improvements: Adapted tool options and created scripts for using the tool in a cluster environment softly.

May 23th, 2014 : Cl-Atse binary package for Linux & Windows 32bits, May 23th 2014(info)#

Release version. Cummulative update for the improvements and corrections made to the tool after the Avantssar and Nessos European projects. Also, added internal system constraints for XML tests (TestInXML, TextNotInXML), and corrected behavior for the simplification module.

December 18th, 2012 : Cl-Atse binary package for Linux 32&64 bits, Windows 32bits, and Mac 64bits, Dec. 18th 2012(info)#

Release version. Rewrote support for the option --trace. Before, this option was not much more than a debugging option to be used in conjunction with --states and --vv. Now, the option refers to objects in the Aslan input file instead of internal objects defined by the tool, and must remain independent from the simplification/optimization modules and the alterations they do to the specification. In particular, the option accepts rule names as defined in the Aslan model, e.g. : cl-atse myspec.aslan --trace "step_015_by_Alice_line_21 step_017_by_Bob_line_38"

--trace behavior. Moreover, this option has now two behaviors: 1) If an attack is found before the end of the trace to follow, then the analysis is stopped and the attack is displayed; 2) If no attack is found at the end of the trace and the final state is not empty, then the analysis continues as a normal depth-first analysis would do, until an attack is found by completing the given trace prefix or no more state can be reached. Also, the old syntax based on agent's names internally chosen by the tool is still accepted, for compatibility.

October 2nd, 2012 : Cl-Atse binary package for Linux 64bits and Windows 32bits, October 2nd, 2012(info)#

Release version. Added support for Aslan's set semantic through option --sets. Default uses a multi-sets semantic. Added support for converting some No-state transitions to Horn clauses, when possible. This may be used for ACM channels type, while it is important to remember that this type of channels is not adapted to Cl-Atse. The CCM channel type should always be preferred at translation time. Also various minor bug corrections. See the Bugzilla's tranck for Cl-Atse, at

April 2nd, 2012 : Cl-Atse binary package for Linux 64bits and Windows i586, May 02th, 2012(info)#

Release version for Avantssar & Spacios tool distribution.

April 23th, 2012 : Cl-Atse binary package for Linux 64bits and Windows i586, 25 April 2012(info)#

Main update : This tool update introduces the support for negative constraints on the intruder's knowledge. This support is correct and complete for any Aslan specification not containing algebraic operators like Xor and Exp, and complying with the assumptions of the paper "Towards the orchestration of secured services under non-disclosure policies" by T. Avanesov, Y. Chevalier, M. Rusinowitch and M. Turuani (currently under submission). In particular, negative constraints on the intruder's knowledges should not contains variables not already defined in earlier positive constraints. Currently, no theoretical result would guaranty the correction and completeness of the process outside these conditions. Technically, while the process in Cl-Atse for negative constraints on the intruder's knowledge relies on the theoretical result to guaranty completeness, it still employs constrain solving techniques instead of guessing to find attacks, as the tool always did. The negative constraints are managed with the other ones, and tested v.s. positive constraints each time a modification of the system state occurs. Therefore, a solution found by Cl-Atse might still contain variables, and thus represents a set of solutions (as it always did, even with positive constraints only). A representative of this set can be obtained e.g. by filling remaining free variables with fresh values as shown in the theoretical paper, thus preserving the negative constraints that might carry them.

Sample for negative constraints on the intruder's knowledge : Here are some files to show the possibilities of this new feature of Cl-Atse. This sample, based on the Loan Origination case study from Avantssar, is an orchestration problem where the mediator could respond to the client directly if you consider positive constraints only, but should not and is forced to rely on external agents for some of the process because the security policy to be satisfied enforces that some data (e.g. an amount of money) must remain undisclosed to the mediator and known only by trusted 'Clerk' agents. According to the European project Avantssar's orchestration method, this orchestration problem is presented to the Cl-Atse analysis backend as a standard web-services insecurity problem in presence of an active intruder, and any attack found by the tool represents a mediator, i.e. a new agent which role is a solution to the orchestration problem. Thus, constraints like 'the mediator should not know xxx' becomes, on an attack point of view, 'the intruder must not know xxx'. This is novel, as intruder constraints for orchestration/insecurity problems until now were only e.g. "mediator must forge (implies knows) some message for the client". Here are some variants of the specification to show the tool behavior:

  1. Original Aslan++ specification(info) : This is the input of the Aslan++ to Aslan translator, without not(iknows(..)) facts.
  2. Aslan specification, without neg. constraints, and without any clerk(info) : In this situation, Cl-Atse finds an orchestration where the mediator assumes himself the role of Clerk. The mediator is build from scratch by Cl-Atse to match the client's needs.
  3. Aslan specification, with neg. constraints, but without any clerk(info) : In this situation, Cl-Atse cannot find any orchestration, because it is impossible for the mediator satisfy the client without assuming the role of Clerk, and thus, without having a way to acquire the data he should not be aware of.
  4. Aslan specification, with neg. constraints, and with some Clerk available(info) : In this situation, Cl-Atse finds an orchestration where the mediator delegates some part of the process to the Clerks. The secret data remain secret and nondeductible by the mediator thanks the the encryption layer added by the Clerks.

Feb. 23th, 2011 : Cl-Atse binary package for Linux and Windows, 32 and 64bits, 23 Feb 2011(info) A version for Mac OS X, 386(info)#

Dec. 30th, 2010 : Cl-Atse binary package for Linux and Windows, 32 and 64bits, Dec. 30th, 2010(info)#

This is the Cl-Atse Packages page.

A server ( has been set up offering instant on-line analysis with the Avantssar's and Avispa's tools developed by the CASSIS team. This is a 12-cores Ubuntu server strong enough to offer analysis services to users concurrently. We expect to extend the tool and the server's mechanics to offer parallel and/or delegated on-line analysis in the future. The services currently offered by our server are described on the Avantssar page.

Logo of the Avantssar European Project

Orchestration & Validation Platform, Loria-INRIA part

This server is part of the European Project AVANTSSAR server ring. It provides the following services :

Service Name SOAP of the Web-Service Service description On-line query form(s) Documentation Download
The HLPSL to IF Translator (hlpsl2if) Translator Service WSDL Translate Hlpsl2If Doc. Hlpsl2If Packages
High-Lever Protocol Specification Language (HLPSL) to Intermediate Format (IF) translator for the European Project Avispa

Service Name SOAP of the Web-Service Service description On-line query form(s) Documentation Download
The Cl-Atse back-end solver (cl-atse) CL-Atse Service WSDL Analyze and Get options Cl-Atse Doc. Cl-Atse packages
Protocol and Web-services analysis backend for the European Projects Avispa & Avantssar

Service Name SOAP of the Web-Service Service description Online query form(s) Documentation Download
The ASLAN Orchestrator (Asynchronous) (see WSDL) WSDL (async.) Async. Orchestration Orchestrator Doc. Orchestrator packages
The ASLAN Orchestrator (Synchronous) (see WSDL) WSDL (sync.) Sync. Orchestration Orchestrator Doc. Orchestrator packages
Samples Two-Party Digital Contract Signing(info), Two-Party Digital Contract Signing (Goal Input Style)(info), Squared-Sum Computation(info)
ASLAN-based Web-Services Orchestration tool for the European Project Avantssar.

Other known servers in the AVANTSSAR's ring:

Both SOAP requests and query forms are accepted by the services. Currently, each analysis request 'lives' for 2 minutes maximum and is killed after that delay to prevent overcharge of the server. Parallel processing will allow users to get full distributed CPU power during their 2-minutes window. Delegated analysis will allow (registered?) users to start much longer analysis in the server's background and be warned when a result is found.

The Aslan GUI (python)#

An Aslan Graphical User Interface has been programmed by an engineer in Nancy to help users who want to produce Aslan models from scratch. The interface offers the possibility to code an Aslan specification by only filling boxes in a few windows. The interface organises the provided data to create and fill a whole Aslan v2 structure. Analysis is possible directly from the interface (some cl-atse binary is provided), and the result is shown as a message sequence chart. The interface is written in python, and so python is required as well as some libraries provided in the package for the interface. The Aslan GUI can be downloaded here(info).

Add new attachment

Only authorized users are allowed to upload new attachments.

List of attachments

Kind Attachment Name Size Version Date Modified Author Change note
zip 15,520.4 kB 1 25-Apr-2013 15:37 Mathieu Turuani The Aslan Graphical User Interface, version 1.
« This page (revision-71) was last changed on 25-avr.-2013 15:36 by Mathieu Turuani