SAML SSO Tutorial

This tutorial presents an application of the SPaCIoS Tool to the SAML SSO case study.

Involved Components

  • IBT For AAT instrumentation and execution.
  • SATMC For AAT generation.
  • Fred For LTL goal separation.


Expected results

  • Execute a test and observe the SUCCESS verdict in the console.

Resources required

Tutorial steps


    1. Download and unzip the project. Download and unzip the file The archive contains:
      • (P1) the SAML2-SSO SPaCIoS project: ASLan++, ASLan, OF, IUT files and others
      • (P2) the SpaciosHTTPHTMLAdapters Java project: common testing adapter for HTTP and HTML.

      Notice that project (P1) depends on project (P2).


    1. Run Eclipse with the SPaCIoS Tool and import the projects.
      • Run your Eclipse with the SPaCIoS Tool.
      • Import the projects (P1) and (P2) following the these steps:



    1. (Optional step) Inspecting the ASLan++ Model. By double-clicking one of the ASLan++ files available in the SAML2-SSO project, the SPaCIoS Tool loads it into the editor area allowing the inspection of the model.


    1. (Available component) Applying LTL separation. The Fred tool allows for obtaining several LTL separated models from a given ASLan model. Then, the new models can be exploited in the ongoing analysis and testing process. LTL separation can be applied in this point of the tutorial by invoking Fred on one of the existing ASLan models. As a result, new models will appear in the current workspace.


    1. (Optional step) Model Checking the ASLan Model. The SAML-SSO project already contains the model checker output needed for the tutorial. To generate it we execute the following steps. Locate the ASLan file SAML_SSO-SP_init-ACM_2SSLuserlogin-functional.aslan in the project. Right-click on it and select SPaCIoS -> Run SATMC. This will open the SATMC option dialog. (To avoid overwriting the existing file set the output file field, e.g., we can input tutorial_aat.of). Then, we confirm and we press Ok in the following invocation summary screen. This starts the model checking procedure which may take a few minutes. Eventually, the SATMC output will be added in the project folder.


    1. (Optional step) Inspecting the Generated AAT. You can inspect the AAT by following these steps.
      • Open the abstract trace saml_sso-sp_init-acm_2ssluserlogin-functional.of
      • Click on the “Events Sequence Chart” tab to see the graphical view of the abstract trace
      • Click on the “#” button of the Outline to see the list of steps of the abstract trace

      You should obtain an output similar to the following figure:
      ibtThis abstract trace captures the functional execution of the protocol. It has been obtained by model-checking the file SAML_SSO-SP_init-ACM_2SSLuserlogin-functional.aslan automatically generated from the ASLan++ model.


    1. (Optional step) Open the IUT file. To visualize the content of the IUT filefoodlXfeide.iut double-click on it. See figure below:
      You can see which agents are included in the SUT and how the various abstract symbols are mapped to real world values and Java Adapter classes.


  1. Preparing the SUT for testcase execution. Before running testcases, some preparation and configuration for the SUT may be necessary. This is specific for the SUT and testcases considered. For this tutorial we have to:
    • Create an account: Register an account on Feide OpenIdP, if you do not have one yet:
      • Access this page and follow the registration process.
      • Please take note of your username and password. In the sequel, we will refer to them as (USR) and (PWD) respectively.
    • Set the testing user and password:
      • Open the class saml_sso.setup.FoodlXfeideSetup within theSAML2-SSO project. (See figure below).
      • Set the strings to (USR) and (PWD) (see previous tutorial step).


  2. Create the “Execute Abstract Trace” run configuration.
    • Open the run configuration, see \autoref{fig:ibt-tutorial-rc}
    • Go to the “Execute Abstract Trace”
    • Create a new launch configuration,
    • Fill-in as in \autoref{fig:ibt-tutorial-rc}. Set the proxy if and only if you are behind a proxy.


  3. Running the AAT (see IBT Tutorial).
      • Click on the run button of the run configuration you just created.
      • You may get an pop-up as in the following figure.


      In case just click on yes.

    • You should see the console printing out many logging information.
    • The “Test Execution Result” view should open.
    • Double-click on the last line and then click on the “Browser rendering” tab. You should get something similar to:
    • You should get a SUCCESS verdict in the console, as in: