项目作者: BSI-Bund

项目描述 :
CafeOBJ proof of Key Secrecy of PACE with OTS/CafeOBJ.
高级语言: AMPL
项目地址: git://github.com/BSI-Bund/CafeOBJ-PACE.git
创建时间: 2021-03-31T13:15:21Z
项目社区:https://github.com/BSI-Bund/CafeOBJ-PACE

开源协议:MIT License

下载


OTS-Proof

This repository contains a CafeOBJ proof that is described in the paper
Key Secrecy of PACE with OTS/CafeOBJ.

How to run:

  1. Download CafeOBJ from
    https://cafeobj.org/

    You need: CafeOBJ system Version 1.4.8(PigNose0.99,p33)

  2. Extract CafeOBJ, for example to ~/cafeobj-1.4

  3. To run the proof, start CafeOBJ, e.g. by executing
    ~/cafeobj-1.4/bin/cafeobj

    and call the scripts of the proof score in
    increasing order, like this:

  1. input pace.mod
  2. input invariants.mod
  3. input proof100.mod
  4. input proof110.mod
  5. ...
  6. input proof740.mod

The proofs afterwards are split for perfomance reasons:

  1. input proof800.mod
  2. input proof800_fkm21.mod
  3. input proof800_fkm22.mod
  4. input proof800_fkm31.mod
  5. input proof800_fkm32.mod
  6. input proof900_sdm1.mod
  7. input proof900_sdm3.mod
  8. input proof900_fkm11.mod
  9. input proof900_fkm12.mod
  10. input proof900_fkm21.mod
  11. input proof900_fkm22.mod
  12. input proof900_fkm31.mod
  13. input proof900_fkm32_part1.mod
  14. input proof900_fkm32_part2.mod