• Stars
    star
    7
  • Rank 2,294,772 (Top 46 %)
  • Language
    Ada
  • License
    GNU Lesser Genera...
  • Created about 6 years ago
  • Updated over 3 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

SPARK TOTP library

STOTP

STOTP is an implementation of the time based one time pad (TOTP) written in SPARK. It currently only supports SHA-1 but since it is based on the libsparkcrypto further algorithms can be added.

The library includes a toolset to generate tokens for twe factor authentication from provided base32 keys:

The code proves for the absence of runtime errors and the correctness of its dependencies.

Usage

Requirements

To build the project the GNAT GPL toolchain is required.

Build

  • $ git clone --recursive https://github.com/jklmnn/STOTP.git
  • $ cd STOTP
  • $ gprbuild -P stotp.gpr

Prove

  • $ gnatprove -P stotp.gpr

Example

The project file builds an example application that takes a base32 key and generates the current TOTP token:

  • $ ./build/generate_2fa_token <base32 key>

Tests

The project also builds some simple tests to check the outputs of core packages. These are executables in the build directory prefixed with test_ and all of them should only output TRUE one or multiple times.

Basic usage

To get a basic understanding in how to use the library take a look at the files in examples and tests. Also all specifications in src are annotated. Further documentation might probably follow