Compare commits
15 Commits
22da81b807
...
8d16f2b40f
| Author | SHA1 | Date |
|---|---|---|
 Achim D. Brucker
|
8d16f2b40f | |
|
Achim D. Brucker
|
65583684a1 | |
|
Achim D. Brucker
|
10a9b2514e | |
|
Achim D. Brucker
|
35fd91aad5 | |
|
Achim D. Brucker
|
c028fc027e | |
|
Achim D. Brucker
|
805e67fefb | |
|
Achim D. Brucker
|
781d13855a | |
|
Achim D. Brucker
|
2c804039b5 | |
|
Achim D. Brucker
|
bb1c93b00e | |
|
Achim D. Brucker
|
9ef8e90bd7 | |
|
Achim D. Brucker
|
9f66f82aa8 | |
|
Achim D. Brucker
|
ec42f2f2de | |
|
Achim D. Brucker
|
53cea57fb5 | |
|
Achim D. Brucker
|
0d6d685268 | |
|
Achim D. Brucker
|
aad1e984f9 |
|
|
@ -0,0 +1 @@
|
|||
bin/anb2thy
|
||||
4
LICENSE
4
LICENSE
|
|
@ -1,5 +1,5 @@
|
|||
Copyright (c) 2013-2015, Achim D. Brucker
|
||||
2013-2015, Helmut Petritsch
|
||||
Copyright (c) 2013-2016 Achim D. Brucker
|
||||
|
||||
All rights reserved.
|
||||
|
||||
Redistribution and use in source and binary forms, with or without
|
||||
|
|
|
|||
|
|
@ -1,10 +1,11 @@
|
|||
# Isabelle/OFMC - Linking OFMC and Isabelle/HOL
|
||||
This is a developer release for Isabelle/OFMC, i.e., while it may be
|
||||
of interested to experts, it is not yet useable by the general
|
||||
public. This development version comprises a small set of Isabelle
|
||||
theories and a prototypical tool, called anb2thy. Using OFMC's
|
||||
fixed-point module, anb2thy generates Isabelle theory files for
|
||||
protocols that haven been successfully validated by OFMC.
|
||||
public. This development version comprise a small Isabelle
|
||||
theory and a prototypical tool, called anb2thy. Using OFMC's
|
||||
fixed-point module, anb2thy generate a Isabelle theory (for
|
||||
[Isabelle 2016](http://isabelle.in.tum.de/website-Isabelle2016/index.html))
|
||||
file for protocols that haven been successfully validated by OFMC.
|
||||
|
||||
## Team
|
||||
* [Achim D. Brucker](http://www.brucker.ch/)
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
header {* Analysing BilateralKeyExchange *}
|
||||
chapter {* Analysing BilateralKeyExchange *}
|
||||
(* ***********************************
|
||||
This file is automatically generated from the AnB file "AnB/Bilateral-Key_Exchange.AnB".
|
||||
Backend: Open Source Fixedpoint Model Checker version 2009c
|
||||
|
|
@ -7,7 +7,7 @@ header {* Analysing BilateralKeyExchange *}
|
|||
theory
|
||||
"Bilateral-Key_Exchange"
|
||||
imports
|
||||
ofmc
|
||||
"../src/ofmc"
|
||||
begin
|
||||
|
||||
|
||||
|
|
@ -242,7 +242,8 @@ where
|
|||
|
||||
|
||||
section {* Fixed-point Definition (BilateralKeyExchange) *}
|
||||
constdefs BilateralKeyExchange_fp::"Fact set""BilateralKeyExchange_fp == {m. ( ? a32 a33 Abs_NB5 Abs_NB6 Abs_NB7 Abs_NB4 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 i14 i15 Abs_NA3 i3 Abs_NA4 Abs_NA5 Abs_NA6 Abs_NB1 Abs_NB2 Abs_NB3 a24 a25 a26 a27 a28 a29 a30 a31 a5 Abs_NI1 a6 a7 a8 Abs_NI2 a9 a10 a11 a12 a13 a14 Abs_NI3 a15 a16 a17 a18 a19 Abs_K1 a20 a21 Abs_K2 a22 a23 Abs_NA2 sid0 a4 Abs_NI0 Abs_NB0 a0 i0 Abs_NA0 a1 i1 Abs_NA1 a2 a3 i2 Abs_K0 .
|
||||
definition
|
||||
"BilateralKeyExchange_fp = {m. ( ? a32 a33 Abs_NB5 Abs_NB6 Abs_NB7 Abs_NB4 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 i14 i15 Abs_NA3 i3 Abs_NA4 Abs_NA5 Abs_NA6 Abs_NB1 Abs_NB2 Abs_NB3 a24 a25 a26 a27 a28 a29 a30 a31 a5 Abs_NI1 a6 a7 a8 Abs_NI2 a9 a10 a11 a12 a13 a14 Abs_NI3 a15 a16 a17 a18 a19 Abs_K1 a20 a21 Abs_K2 a22 a23 Abs_NA2 sid0 a4 Abs_NI0 Abs_NB0 a0 i0 Abs_NA0 a1 i1 Abs_NA1 a2 a3 i2 Abs_K0 .
|
||||
(m = Iknows(Nonce((ni Abs_NI0))))
|
||||
| (m = Iknows(Agent(dishonest(i0))))
|
||||
| (m = State(rA, [Agent(honest(a0)), Step(0), inv(pk(Agent(honest(a1)))), pk(Agent(dishonest(i0))), pk(Agent(honest(a2))), Agent(dishonest(i1)), SID(sid0)] ))
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
header {* Analysing DenningSacco *}
|
||||
chapter {* Analysing DenningSacco *}
|
||||
(* ***********************************
|
||||
This file is automatically generated from the AnB file "AnB/Denning-Sacco.AnB".
|
||||
Backend: Open Source Fixedpoint Model Checker version 2009c
|
||||
|
|
@ -7,7 +7,7 @@ header {* Analysing DenningSacco *}
|
|||
theory
|
||||
"Denning-Sacco"
|
||||
imports
|
||||
ofmc
|
||||
"../src/ofmc"
|
||||
begin
|
||||
|
||||
|
||||
|
|
@ -189,7 +189,8 @@ where
|
|||
|
||||
|
||||
section {* Fixed-point Definition (DenningSacco) *}
|
||||
constdefs DenningSacco_fp::"Fact set""DenningSacco_fp == {m. ( ? Abs_NI0 i8 i9 i10 i11 i12 i13 i14 i15 a10 a11 a12 a13 a14 a15 a16 a17 Abs_KAB5 a18 a19 a20 Abs_KAB6 i7 a5 a6 Abs_KAB3 Abs_T2 a7 a8 Abs_KAB4 a9 Abs_Payload1 sid0 Abs_Payload0 i3 i4 i5 i6 a0 a1 a2 a3 Abs_KAB1 a4 Abs_KAB2 Abs_T1 i0 i1 i2 Abs_KAB0 Abs_T0 .
|
||||
definition
|
||||
"DenningSacco_fp = {m. ( ? Abs_NI0 i8 i9 i10 i11 i12 i13 i14 i15 a10 a11 a12 a13 a14 a15 a16 a17 Abs_KAB5 a18 a19 a20 Abs_KAB6 i7 a5 a6 Abs_KAB3 Abs_T2 a7 a8 Abs_KAB4 a9 Abs_Payload1 sid0 Abs_Payload0 i3 i4 i5 i6 a0 a1 a2 a3 Abs_KAB1 a4 Abs_KAB2 Abs_T1 i0 i1 i2 Abs_KAB0 Abs_T0 .
|
||||
(m = Iknows(Nonce((ni Abs_NI0))))
|
||||
| (m = Iknows(Agent(dishonest(i0))))
|
||||
| (m = State(rA, [Agent(honest(a0)), Step(0), Nonce((timestamp Abs_T0)), SymKey((sk(pair(Agent(honest(a1)), Agent(honest(a2)))) Abs_KAB0)), Agent(dishonest(i0)), SID(sid0)] ))
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
header {* Analysing ISO_onepass_pk *}
|
||||
chapter {* Analysing ISO_onepass_pk *}
|
||||
(* ***********************************
|
||||
This file is automatically generated from the AnB file "AnB/ISOpubKeyOnePassUnilateralAuthProt.AnB".
|
||||
Backend: Open Source Fixedpoint Model Checker version 2009c
|
||||
|
|
@ -7,7 +7,7 @@ header {* Analysing ISO_onepass_pk *}
|
|||
theory
|
||||
"ISOpubKeyOnePassUnilateralAuthProt"
|
||||
imports
|
||||
ofmc
|
||||
"../src/ofmc"
|
||||
begin
|
||||
|
||||
|
||||
|
|
@ -188,7 +188,8 @@ where
|
|||
|
||||
|
||||
section {* Fixed-point Definition (ISO_onepass_pk) *}
|
||||
constdefs ISO_onepass_pk_fp::"Fact set""ISO_onepass_pk_fp == {m. ( ? Abs_NI3 Abs_NI4 Abs_NI5 a18 a19 a20 a21 a22 a23 a24 a25 i11 i12 i13 Abs_Text13 Abs_Text14 Abs_Text15 Abs_NA3 a12 a13 a14 Abs_NA4 a15 a16 a17 Abs_NA5 i8 i9 i10 Abs_Text11 Abs_Text12 Abs_NI0 Abs_NI1 Abs_NA1 i3 i4 i5 i6 i7 Abs_NI2 a9 a10 a11 Abs_NA2 sid0 a6 a7 a8 a5 i0 i1 i2 a0 a1 Abs_NA0 a2 a3 a4 Abs_Text10 .
|
||||
definition
|
||||
"ISO_onepass_pk_fp = {m. ( ? Abs_NI3 Abs_NI4 Abs_NI5 a18 a19 a20 a21 a22 a23 a24 a25 i11 i12 i13 Abs_Text13 Abs_Text14 Abs_Text15 Abs_NA3 a12 a13 a14 Abs_NA4 a15 a16 a17 Abs_NA5 i8 i9 i10 Abs_Text11 Abs_Text12 Abs_NI0 Abs_NI1 Abs_NA1 i3 i4 i5 i6 i7 Abs_NI2 a9 a10 a11 Abs_NA2 sid0 a6 a7 a8 a5 i0 i1 i2 a0 a1 Abs_NA0 a2 a3 a4 Abs_Text10 .
|
||||
(m = Iknows(Nonce((ni Abs_NI0))))
|
||||
| (m = Iknows(Agent(dishonest(i0))))
|
||||
| (m = State(rA, [Agent(honest(a0)), Step(0), inv(pk(Agent(honest(a1)))), pk(Agent(honest(a2))), crypt(inv(pk(Agent(honest(a3)))), pair(Agent(honest(a4)), pk(Agent(honest(a5))))), Agent(dishonest(i0)), SID(sid0)] ))
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
header {* Analysing ISO_twopass_symm *}
|
||||
chapter {* Analysing ISO_twopass_symm *}
|
||||
(* ***********************************
|
||||
This file is automatically generated from the AnB file "AnB/ISOsymKeyTwoPassUnilateralAuthProt.AnB".
|
||||
Backend: Open Source Fixedpoint Model Checker version 2009c
|
||||
|
|
@ -7,7 +7,7 @@ header {* Analysing ISO_twopass_symm *}
|
|||
theory
|
||||
"ISOsymKeyTwoPassUnilateralAuthProt"
|
||||
imports
|
||||
ofmc
|
||||
"../src/ofmc"
|
||||
begin
|
||||
|
||||
|
||||
|
|
@ -151,7 +151,8 @@ where
|
|||
|
||||
|
||||
section {* Fixed-point Definition (ISO_twopass_symm) *}
|
||||
constdefs ISO_twopass_symm_fp::"Fact set""ISO_twopass_symm_fp == {m. ( ? Abs_NB2 Abs_NB3 Abs_NI1 i7 Abs_Text22 Abs_Text23 a8 a9 a10 a11 a12 a13 a14 i4 i5 Abs_NB1 a6 a7 i6 sid0 a3 a4 a5 i3 Abs_NI0 Abs_NB0 a2 a0 i0 Abs_Text20 i1 a1 i2 Abs_Text21 .
|
||||
definition
|
||||
"ISO_twopass_symm_fp = {m. ( ? Abs_NB2 Abs_NB3 Abs_NI1 i7 Abs_Text22 Abs_Text23 a8 a9 a10 a11 a12 a13 a14 i4 i5 Abs_NB1 a6 a7 i6 sid0 a3 a4 a5 i3 Abs_NI0 Abs_NB0 a2 a0 i0 Abs_Text20 i1 a1 i2 Abs_Text21 .
|
||||
(m = Iknows(Nonce((ni Abs_NI0))))
|
||||
| (m = Iknows(Agent(dishonest(i0))))
|
||||
| (m = State(rA, [Agent(honest(a0)), Step(0), SymKey(sk(pair(Agent(honest(a1)), Agent(dishonest(i0))))), Agent(dishonest(i1)), SID(sid0)] ))
|
||||
|
|
|
|||
|
|
@ -1,83 +0,0 @@
|
|||
#############################################################################
|
||||
# Isabelle-OFMC --- Connecting OFMC and Isabelle/HOL
|
||||
#
|
||||
# IsaMakefile ---
|
||||
# This file is part of Isabelle-OFMC.
|
||||
#
|
||||
# Copyright (c) 2009 Achim D. Brucker, Germany
|
||||
#
|
||||
# All rights reserved.
|
||||
#
|
||||
# Redistribution and use in source and binary forms, with or without
|
||||
# modification, are permitted provided that the following conditions are
|
||||
# met:
|
||||
#
|
||||
# * Redistributions of source code must retain the above copyright
|
||||
# notice, this list of conditions and the following disclaimer.
|
||||
#
|
||||
# * Redistributions in binary form must reproduce the above
|
||||
# copyright notice, this list of conditions and the following
|
||||
# disclaimer in the documentation and/or other materials provided
|
||||
# with the distribution.
|
||||
#
|
||||
# * Neither the name of the copyright holders nor the names of its
|
||||
# contributors may be used to endorse or promote products derived
|
||||
# from this software without specific prior written permission.
|
||||
#
|
||||
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
# OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
# LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
# DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
# THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
# (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
##############################################################################
|
||||
# $Id: IsaMakefile 927 2009-11-01 22:36:10Z brucker $
|
||||
|
||||
default: ofmc-anb
|
||||
images:
|
||||
test: ofmc-anb
|
||||
|
||||
all: images test
|
||||
|
||||
## global settings
|
||||
|
||||
SRC = $(ISABELLE_HOME)/src
|
||||
OUT = $(ISABELLE_OUTPUT)
|
||||
LOG = $(OUT)/log
|
||||
HEAP = ofmc-anb
|
||||
|
||||
MV = mv
|
||||
CP = cp
|
||||
|
||||
USEDIR = $(ISATOOL) usedir -b -g true -v true -i true -d pdf ## -D generated
|
||||
USEDIR = $(ISATOOL) usedir -b
|
||||
|
||||
HOSTNAME = $(shell,$(ISATOOL) getenv HOSTNAME)
|
||||
export HOSTNAME
|
||||
|
||||
## ofmc-isabelle
|
||||
|
||||
$(HEAP): $(LOG)/HOL-$(HEAP).gz
|
||||
|
||||
$(LOG)/HOL-$(HEAP).gz: ROOT.ML document/root.tex *.thy
|
||||
@$(RM) -rf $(ISABELLE_BROWSER_INFO)/HOL/$(HEAP)/document
|
||||
@$(USEDIR) ofmc $(HEAP)
|
||||
@$(CP) $(ISABELLE_BROWSER_INFO)/HOL/ofmc/$(HEAP)/document.pdf $(HEAP).pdf
|
||||
|
||||
thygen:
|
||||
for i in AnB/*.AnB; do echo -e $$i; anb2thy $$i > `basename $$i .AnB`.thy; done
|
||||
thygen-noproof:
|
||||
for i in AnB/*.AnB; do echo -e $$i; anb2thy --noproof $$i > `basename $$i .AnB`.thy; done
|
||||
|
||||
fpgen:
|
||||
for i in AnB/*.AnB; do echo -e $$i; ofmc $$i -ot Isa > AnB/`basename $$i .AnB`.fp; done
|
||||
|
||||
## clean
|
||||
|
||||
clean:
|
||||
@$(RM) -f $(LOG)/HOL-$(HEAP).gz
|
||||
|
|
@ -0,0 +1,38 @@
|
|||
#############################################################################
|
||||
# Isabelle-OFMC --- Connecting OFMC and Isabelle/HOL
|
||||
#
|
||||
# IsaMakefile ---
|
||||
# This file is part of Isabelle-OFMC.
|
||||
#
|
||||
# Copyright (c) 2009 Achim D. Brucker, Germany
|
||||
#
|
||||
# All rights reserved.
|
||||
#
|
||||
# Redistribution and use in source and binary forms, with or without
|
||||
# modification, are permitted provided that the following conditions are met:
|
||||
#
|
||||
# * Redistributions of source code must retain the above copyright notice, this
|
||||
# list of conditions and the following disclaimer.
|
||||
#
|
||||
# * Redistributions in binary form must reproduce the above copyright notice,
|
||||
# this list of conditions and the following disclaimer in the documentation
|
||||
# and/or other materials provided with the distribution.
|
||||
#
|
||||
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
# DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
# FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
# DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
# SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
|
||||
thygen:
|
||||
for i in AnB/*.AnB; do echo -e $$i; ../bin/anb2thy $$i > `basename $$i .AnB`.thy; done
|
||||
thygen-noproof:
|
||||
for i in AnB/*.AnB; do echo -e $$i; ../bin/anb2thy --noproof $$i > `basename $$i .AnB`.thy; done
|
||||
|
||||
fpgen:
|
||||
for i in AnB/*.AnB; do echo -e $$i; ofmc $$i -ot Isa > AnB/`basename $$i .AnB`.fp; done
|
||||
|
|
@ -1,76 +0,0 @@
|
|||
(*****************************************************************************
|
||||
* HOL-OCL --- connecting OFMC and Isabelle/HOL
|
||||
*
|
||||
* ROOT.ML ---
|
||||
* This file is part of Isabelle-OFMC.
|
||||
*
|
||||
* Copyright (c) 2009 Achim D. Brucker, Germany
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: ROOT.ML 931 2009-11-01 22:44:01Z brucker $ *)
|
||||
|
||||
|
||||
val today = (Date.toString(Date.fromTimeUniv (Time.now())))^" (UTC)"
|
||||
val hostname = getOpt (OS.Process.getEnv "HOSTNAME", "hostname not set")
|
||||
val timer = Timer.startRealTimer ()
|
||||
val log_file = "document/report.tex"
|
||||
|
||||
val _ = File.write (Path.explode (log_file))
|
||||
( "% This file was generated automatically \n"
|
||||
^"\\section{Runtime Report}\n"
|
||||
^"All reported runtime are measured on host ``"^hostname^"'' on "^today^".\n\n"
|
||||
^"\\begin{tabular}{lr}\n"
|
||||
)
|
||||
|
||||
fun log_thy thy =
|
||||
let
|
||||
val start = Timer.checkRealTimer timer
|
||||
val _ = use_thy thy
|
||||
val stop = Timer.checkRealTimer timer
|
||||
val duration = Time.-(stop,start)
|
||||
val _ = File.append (Path.explode(log_file)) (" "^thy^" & "^(Time.toString duration)^"\\\\\n")
|
||||
in () end
|
||||
|
||||
|
||||
|
||||
val _ = map log_thy [
|
||||
"ISOsymKeyTwoPassUnilateralAuthProt",
|
||||
"Denning-Sacco",
|
||||
"nsl",
|
||||
"ISOpubKeyOnePassUnilateralAuthProt",
|
||||
"WideMouthFrog",
|
||||
"Bilateral-Key_Exchange",
|
||||
"nsl-ks"
|
||||
]
|
||||
|
||||
val _ = File.append (Path.explode (log_file)) ("\\end{tabular}")
|
||||
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
header {* Analysing WideMouthFrog *}
|
||||
chapter {* Analysing WideMouthFrog *}
|
||||
(* ***********************************
|
||||
This file is automatically generated from the AnB file "AnB/WideMouthFrog.AnB".
|
||||
Backend: Open Source Fixedpoint Model Checker version 2009c
|
||||
|
|
@ -7,7 +7,7 @@ header {* Analysing WideMouthFrog *}
|
|||
theory
|
||||
"WideMouthFrog"
|
||||
imports
|
||||
ofmc
|
||||
"../src/ofmc"
|
||||
begin
|
||||
|
||||
|
||||
|
|
@ -174,7 +174,8 @@ where
|
|||
|
||||
|
||||
section {* Fixed-point Definition (WideMouthFrog) *}
|
||||
constdefs WideMouthFrog_fp::"Fact set""WideMouthFrog_fp == {m. ( ? Abs_TA2 Abs_TA1 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 a32 a33 a34 a17 a18 a19 a20 i19 i20 i21 i22 i23 i24 i18 i12 Abs_TS2 i13 i14 Abs_TS3 i15 Abs_TS4 i16 i17 Abs_NI0 Abs_NI1 i6 a9 Abs_NI2 a10 a11 i7 Abs_KAB2 a12 i8 a13 a14 a15 i9 i10 a16 i11 Abs_KAB3 Abs_TS1 a8 i5 Abs_KAB1 sid0 i4 a5 a6 a7 a3 Abs_TA0 a4 a1 a2 i0 i1 Abs_TS0 i2 a0 i3 Abs_KAB0 .
|
||||
definition
|
||||
"WideMouthFrog_fp = {m. ( ? Abs_TA2 Abs_TA1 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 a32 a33 a34 a17 a18 a19 a20 i19 i20 i21 i22 i23 i24 i18 i12 Abs_TS2 i13 i14 Abs_TS3 i15 Abs_TS4 i16 i17 Abs_NI0 Abs_NI1 i6 a9 Abs_NI2 a10 a11 i7 Abs_KAB2 a12 i8 a13 a14 a15 i9 i10 a16 i11 Abs_KAB3 Abs_TS1 a8 i5 Abs_KAB1 sid0 i4 a5 a6 a7 a3 Abs_TA0 a4 a1 a2 i0 i1 Abs_TS0 i2 a0 i3 Abs_KAB0 .
|
||||
(m = Iknows(Nonce((ni Abs_NI0))))
|
||||
| (m = Iknows(Agent(dishonest(i0))))
|
||||
| (m = State(rA, [Agent(honest(a0)), Step(0), SymKey(sk(pair(Agent(honest(a1)), Agent(honest(a2))))), Agent(dishonest(i0)), SID(sid0)] ))
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
header {* Analysing NSL *}
|
||||
chapter {* Analysing NSL *}
|
||||
(* ***********************************
|
||||
This file is automatically generated from the AnB file "AnB/nsl-ks.AnB".
|
||||
Backend: Open Source Fixedpoint Model Checker version 2009c
|
||||
|
|
@ -7,7 +7,7 @@ header {* Analysing NSL *}
|
|||
theory
|
||||
"nsl-ks"
|
||||
imports
|
||||
ofmc
|
||||
"../src/ofmc"
|
||||
begin
|
||||
|
||||
|
||||
|
|
@ -315,7 +315,8 @@ where
|
|||
|
||||
|
||||
section {* Fixed-point Definition (NSL) *}
|
||||
constdefs NSL_fp::"Fact set""NSL_fp == {m. ( ? Abs_NA3 Abs_NA4 Abs_NA5 i13 Abs_NI1 Abs_NI2 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 Abs_NA1 Abs_NA2 a3 a4 a5 a6 a7 i2 i3 a8 i4 i5 a9 i6 i7 a10 i8 Abs_NB2 i9 a11 i10 Abs_NB3 a12 i11 Abs_NB4 a13 a14 a15 i12 Abs_NB5 sid0 Abs_NI0 Abs_NA0 a0 i0 Abs_NB0 a1 i1 Abs_NB1 a2 .
|
||||
definition
|
||||
"NSL_fp = {m. ( ? Abs_NA3 Abs_NA4 Abs_NA5 i13 Abs_NI1 Abs_NI2 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 Abs_NA1 Abs_NA2 a3 a4 a5 a6 a7 i2 i3 a8 i4 i5 a9 i6 i7 a10 i8 Abs_NB2 i9 a11 i10 Abs_NB3 a12 i11 Abs_NB4 a13 a14 a15 i12 Abs_NB5 sid0 Abs_NI0 Abs_NA0 a0 i0 Abs_NB0 a1 i1 Abs_NB1 a2 .
|
||||
(m = Iknows(Nonce((ni Abs_NI0))))
|
||||
| (m = Iknows(Agent(dishonest(i0))))
|
||||
| (m = State(rA, [Agent(honest(a0)), Step(0), Agent(dishonest(i0)), pk(Agent(honest(a1))), Agent(honest(a2)), inv(pk(Agent(honest(a3)))), pk(Agent(honest(a4))), SID(sid0)] ))
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
header {* Analysing NSL *}
|
||||
chapter {* Analysing NSL *}
|
||||
(* ***********************************
|
||||
This file is automatically generated from the AnB file "AnB/nsl.AnB".
|
||||
Backend: Open Source Fixedpoint Model Checker version 2009c
|
||||
|
|
@ -7,7 +7,7 @@ header {* Analysing NSL *}
|
|||
theory
|
||||
"nsl"
|
||||
imports
|
||||
ofmc
|
||||
"../src/ofmc"
|
||||
begin
|
||||
|
||||
|
||||
|
|
@ -15,7 +15,7 @@ begin
|
|||
section {* Protocol Model (NSL) *}
|
||||
datatype Role = rA | rB
|
||||
|
||||
datatype Purpose = purposeNA | purposeNB
|
||||
datatype Purpose = purposeNI | purposeNA | purposeNB
|
||||
datatype Agent = honest nat
|
||||
| dishonest nat
|
||||
|
||||
|
|
@ -244,7 +244,8 @@ where
|
|||
|
||||
|
||||
section {* Fixed-point Definition (NSL) *}
|
||||
constdefs NSL_fp::"Fact set""NSL_fp == {m. ( ? Abs_NA3 Abs_NA4 Abs_NA5 i9 Abs_NI1 Abs_NI2 a11 a12 a13 a14 a15 a16 a17 a18 a19 Abs_NA1 Abs_NA2 a3 a4 i2 i3 a5 i4 Abs_NB2 i5 a6 i6 Abs_NB3 a7 i7 Abs_NB4 a8 a9 a10 i8 Abs_NB5 sid0 Abs_NI0 Abs_NA0 a0 i0 Abs_NB0 a1 i1 Abs_NB1 a2 .
|
||||
definition
|
||||
"NSL_fp = {m. ( ? Abs_NA3 Abs_NA4 Abs_NA5 i9 Abs_NI1 Abs_NI2 a11 a12 a13 a14 a15 a16 a17 a18 a19 Abs_NA1 Abs_NA2 a3 a4 i2 i3 a5 i4 Abs_NB2 i5 a6 i6 Abs_NB3 a7 i7 Abs_NB4 a8 a9 a10 i8 Abs_NB5 sid0 Abs_NI0 Abs_NA0 a0 i0 Abs_NB0 a1 i1 Abs_NB1 a2 .
|
||||
(m = Iknows(Nonce((ni Abs_NI0))))
|
||||
| (m = Iknows(Agent(dishonest(i0))))
|
||||
| (m = State(rA, [Agent(honest(a0)), Step(0), Agent(dishonest(i0)), inv(pk(Agent(honest(a1)))), SID(sid0)] ))
|
||||
|
|
|
|||
|
|
@ -1,95 +0,0 @@
|
|||
#############################################################################
|
||||
# Isabelle-OFMC --- Connecting OFMC and Isabelle/HOL
|
||||
#
|
||||
# IsaMakefile --- main build setup for Isabelle-OFMC
|
||||
# This file is part of Isabelle-OFMC.
|
||||
#
|
||||
# Copyright (c) 2009 Achim D. Brucker, Germany
|
||||
#
|
||||
# All rights reserved.
|
||||
#
|
||||
# Redistribution and use in source and binary forms, with or without
|
||||
# modification, are permitted provided that the following conditions are
|
||||
# met:
|
||||
#
|
||||
# * Redistributions of source code must retain the above copyright
|
||||
# notice, this list of conditions and the following disclaimer.
|
||||
#
|
||||
# * Redistributions in binary form must reproduce the above
|
||||
# copyright notice, this list of conditions and the following
|
||||
# disclaimer in the documentation and/or other materials provided
|
||||
# with the distribution.
|
||||
#
|
||||
# * Neither the name of the copyright holders nor the names of its
|
||||
# contributors may be used to endorse or promote products derived
|
||||
# from this software without specific prior written permission.
|
||||
#
|
||||
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
# OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
# LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
# DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
# THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
# (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
##############################################################################
|
||||
# $Id: IsaMakefile 935 2009-11-02 00:02:50Z brucker $
|
||||
|
||||
# determine current source version:
|
||||
nullstring:=
|
||||
space := $(nullstring) #
|
||||
#
|
||||
REVISION := $(shell svnversion .)
|
||||
VER_MAIJOR=0
|
||||
VER_MINOR=0
|
||||
VER_MICRO=0
|
||||
VER_TAG=$(space)(dev build: $(REVISION))
|
||||
|
||||
CONFIG_SED_SCRIPT='s/<COLLECTIONTYPE>/$(COLLECTIONTYPE)/;\
|
||||
s/<UNIVERSE>/$(UNIVERSE)/;\
|
||||
s/<VER_MAIJOR>/$(VER_MAIJOR)/;s/<VER_MINOR>/$(VER_MINOR)/;\
|
||||
s/<VER_MICRO>/$(VER_MICRO)/;s/<VER_TAG>/${VER_TAG}/;\
|
||||
s/<XMI_SUPPORT>/$(XMI_SUPPORT)/;\
|
||||
s/<REVISION>/$(REVISION)/'
|
||||
|
||||
## global settings
|
||||
# make internal configuration
|
||||
.PHONY: config.sml
|
||||
|
||||
ECHO=echo
|
||||
RM=rm
|
||||
MV=mv
|
||||
SED=sed
|
||||
MLTON=mlton
|
||||
|
||||
## targets
|
||||
HEAP=ofmc
|
||||
SRC = $(ISABELLE_HOME)/src
|
||||
OUT = $(ISABELLE_OUTPUT)
|
||||
LOG = $(OUT)/log
|
||||
|
||||
USEDIR = $(ISATOOL) usedir -b -g true -v true -i true -d pdf -D generated
|
||||
USEDIR = $(ISATOOL) usedir -b
|
||||
|
||||
$(LOG)/$(HEAP).gz: config.sml ROOT.ML *.thy *.ML ../bin/anb2thy
|
||||
@(test -e generated && find generated -name .svn -type d -print0 | xargs -0 /bin/rm -fr || true)
|
||||
@$(RM) -rf $(ISABELLE_BROWSER_INFO)/HOL/HOL/$(HEAP)/document
|
||||
@($(USEDIR) HOL $(HEAP) \
|
||||
|| \
|
||||
($(ECHO) -e "\033[1;31;40m";\
|
||||
$(ECHO) -e "\a *************************************************" ;\
|
||||
$(ECHO) -e "\a ****************** BUILD FAILED ***************" ;\
|
||||
$(ECHO) -e "\a *************************************************" ;\
|
||||
$(ECHO) -e "\033[1;37;40m\033[0;37;0m")\
|
||||
|| true)
|
||||
|
||||
config.sml:
|
||||
@$(RM) -rf config.sml
|
||||
@$(SED) -e $(CONFIG_SED_SCRIPT) config.sml.in > config.sml
|
||||
|
||||
../bin/anb2thy: encoder/*.sml
|
||||
$(MLTON) encoder/anb2thy.cm
|
||||
$(MV) encoder/anb2thy ../bin
|
||||
|
|
@ -0,0 +1,42 @@
|
|||
#############################################################################
|
||||
# Isabelle-OFMC --- Connecting OFMC and Isabelle/HOL
|
||||
#
|
||||
# IsaMakefile --- main build setup for Isabelle-OFMC
|
||||
# This file is part of Isabelle-OFMC.
|
||||
#
|
||||
# Copyright (c) 2009 Achim D. Brucker, Germany
|
||||
#
|
||||
# All rights reserved.
|
||||
#
|
||||
# Redistribution and use in source and binary forms, with or without
|
||||
# modification, are permitted provided that the following conditions are met:
|
||||
#
|
||||
# * Redistributions of source code must retain the above copyright notice, this
|
||||
# list of conditions and the following disclaimer.
|
||||
#
|
||||
# * Redistributions in binary form must reproduce the above copyright notice,
|
||||
# this list of conditions and the following disclaimer in the documentation
|
||||
# and/or other materials provided with the distribution.
|
||||
#
|
||||
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
# DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
# FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
# DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
# SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
##############################################################################
|
||||
|
||||
MLTON=mlton
|
||||
MV=mv
|
||||
|
||||
../bin/anb2thy: encoder/*.sml
|
||||
$(MLTON) encoder/anb2thy.cm
|
||||
$(MV) encoder/anb2thy ../bin
|
||||
|
||||
generate-parser: encoder/*.lex encoder/*.grm
|
||||
mllex encoder/*.lex
|
||||
mlyacc encoder/*.grm
|
||||
75
src/ROOT.ML
75
src/ROOT.ML
|
|
@ -1,75 +0,0 @@
|
|||
(*****************************************************************************
|
||||
* Isabelle/OFMC --- connecting OFMC and Isabelle/HOL
|
||||
*
|
||||
* ROOT.ML --- main file for Isabelle-OFMC.
|
||||
* This file is part of Isabelle-OFMC.
|
||||
*
|
||||
* Copyright (c) 2009 Achim D. Brucker, Germany
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: ROOT.ML 935 2009-11-02 00:02:50Z brucker $ *)
|
||||
|
||||
use "config.sml";
|
||||
|
||||
OS.FileSys.chDir "encoder";
|
||||
use "root.sml";
|
||||
OS.FileSys.chDir "..";
|
||||
|
||||
use "config.sml";
|
||||
|
||||
val isabelle_version = Distribution.version
|
||||
val ofmc_version = Int.toString(ofmc_ver_major)^"."^Int.toString(ofmc_ver_minor)^"."
|
||||
^Int.toString(ofmc_ver_micro)^ofmc_ver_tag
|
||||
val version = "Isabelle/ofmc "^ofmc_version^", based on "^isabelle_version;
|
||||
|
||||
fun infostr _ = (
|
||||
("\n")^
|
||||
(" Isabelle/ofmc "^ofmc_version^" \n")^
|
||||
(" connecting OFMC and Isabelle/HOL \n")^
|
||||
(" Copyright (c) 2009 Achim D. Brucker \n")^
|
||||
(" \n")^
|
||||
(" Configuration: \n")^
|
||||
(" - ofmc binary: "^(ofmc_connector.ofmc_home()^ofmc_connector.ofmc)^"\n" )^
|
||||
(" - Isabelle: "^(isabelle_version)^"\n" )^
|
||||
(" - ML-system: "^(ml_system)^"\n" ));
|
||||
|
||||
fun info () = writeln (infostr());
|
||||
|
||||
use_thy "ofmc";
|
||||
|
||||
|
||||
|
||||
|
||||
val welcome = Toplevel.imperative (info);
|
||||
val welcomeP =
|
||||
OuterSyntax.improper_command "welcome" "print welcome message" OuterKeyword.diag
|
||||
(Scan.succeed (Toplevel.no_timing o welcome));
|
||||
|
|
@ -1,82 +0,0 @@
|
|||
(*****************************************************************************
|
||||
* Isabelle-OFMC --- Connecting OFMC and Isabelle/HOL
|
||||
*
|
||||
* config.sml.in --- main configuration file for Isabelle-OFMC
|
||||
* This file is part of Isabelle-OFMC.
|
||||
*
|
||||
* Copyright (c) 2009 Achim D. Brucker, Germany
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: config.sml.in 349 2009-01-16 19:17:39Z brucker $ *)
|
||||
|
||||
|
||||
|
||||
structure config =
|
||||
struct
|
||||
val ofmc_id = "$Id: config.sml.in 349 2009-01-16 19:17:39Z brucker $"
|
||||
end;
|
||||
|
||||
|
||||
|
||||
(** Major version number.
|
||||
*
|
||||
* Modify when incompatible changes are made to published interfaces.
|
||||
*)
|
||||
val ofmc_ver_major = 0
|
||||
|
||||
(* Minor version number.
|
||||
*
|
||||
* Modify when new functionality is added or new interfaces are
|
||||
* defined, but all changes are backward compatible.
|
||||
*)
|
||||
val ofmc_ver_minor = 0
|
||||
|
||||
(** Patch number.
|
||||
*
|
||||
* Modify for every released patch.
|
||||
*)
|
||||
val ofmc_ver_micro= 0
|
||||
|
||||
|
||||
(** Version tag: a string describing the version.
|
||||
*
|
||||
* This tag remains " (dev build)" in the repository so that we can
|
||||
* always see from "version()" that the software has been built
|
||||
* from the repository rather than a "blessed" distribution.
|
||||
*
|
||||
* When rolling a tarball, we automatically replace this text with ""
|
||||
* for final releases; in prereleases, it becomes " (Alpha)",
|
||||
* " (Beta 1)", etc., as appropriate.
|
||||
*
|
||||
*)
|
||||
val ofmc_ver_tag = " (dev build: 929:933M)"
|
||||
|
||||
|
|
@ -1,82 +0,0 @@
|
|||
(*****************************************************************************
|
||||
* Isabelle-OFMC --- Connecting OFMC and Isabelle/HOL
|
||||
*
|
||||
* config.sml.in --- main configuration file for Isabelle-OFMC
|
||||
* This file is part of Isabelle-OFMC.
|
||||
*
|
||||
* Copyright (c) 2009 Achim D. Brucker, Germany
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: config.sml.in 349 2009-01-16 19:17:39Z brucker $ *)
|
||||
|
||||
|
||||
|
||||
structure config =
|
||||
struct
|
||||
val ofmc_id = "$Id: config.sml.in 349 2009-01-16 19:17:39Z brucker $"
|
||||
end;
|
||||
|
||||
|
||||
|
||||
(** Major version number.
|
||||
*
|
||||
* Modify when incompatible changes are made to published interfaces.
|
||||
*)
|
||||
val ofmc_ver_major = <VER_MAIJOR>
|
||||
|
||||
(* Minor version number.
|
||||
*
|
||||
* Modify when new functionality is added or new interfaces are
|
||||
* defined, but all changes are backward compatible.
|
||||
*)
|
||||
val ofmc_ver_minor = <VER_MINOR>
|
||||
|
||||
(** Patch number.
|
||||
*
|
||||
* Modify for every released patch.
|
||||
*)
|
||||
val ofmc_ver_micro= <VER_MICRO>
|
||||
|
||||
|
||||
(** Version tag: a string describing the version.
|
||||
*
|
||||
* This tag remains " (dev build)" in the repository so that we can
|
||||
* always see from "version()" that the software has been built
|
||||
* from the repository rather than a "blessed" distribution.
|
||||
*
|
||||
* When rolling a tarball, we automatically replace this text with ""
|
||||
* for final releases; in prereleases, it becomes " (Alpha)",
|
||||
* " (Beta 1)", etc., as appropriate.
|
||||
*
|
||||
*)
|
||||
val ofmc_ver_tag = "<VER_TAG>"
|
||||
|
||||
|
|
@ -9,34 +9,26 @@
|
|||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
* modification, are permitted provided that the following conditions are met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright notice, this
|
||||
* list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* * Redistributions in binary form must reproduce the above copyright notice,
|
||||
* this list of conditions and the following disclaimer in the documentation
|
||||
* and/or other materials provided with the distribution.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: anb2thy.cm 870 2009-10-30 11:05:03Z brucker $ *)
|
||||
|
||||
Group is
|
||||
|
||||
|
|
|
|||
|
|
@ -9,34 +9,26 @@
|
|||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
* modification, are permitted provided that the following conditions are met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright notice, this
|
||||
* list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* * Redistributions in binary form must reproduce the above copyright notice,
|
||||
* this list of conditions and the following disclaimer in the documentation
|
||||
* and/or other materials provided with the distribution.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: ofmc-fp.grm 901 2009-11-01 17:12:18Z brucker $ *)
|
||||
|
||||
|
||||
open OfmcFp
|
||||
|
|
@ -67,6 +59,8 @@ fun rmOuterOp (Operator(_,[msg])) = msg
|
|||
| TBAR of string
|
||||
| TCOMMA of string
|
||||
| TCPAREN of string
|
||||
| TOBRACE of string
|
||||
| TCBRACE of string
|
||||
| TCRYPT of string
|
||||
| TQUOTE of string
|
||||
| TEXP of string
|
||||
|
|
@ -94,9 +88,13 @@ fun rmOuterOp (Operator(_,[msg])) = msg
|
|||
| TTYPES of string
|
||||
| TWITNESS of string
|
||||
| TXOR of string
|
||||
| TDERIVATION of string
|
||||
|
||||
%nonterm START of ofmc_fp
|
||||
| trace of ofmc_fp
|
||||
| ofmc_fp of ofmc_fp
|
||||
| attackinfo of ofmc_fp
|
||||
| fp_or_attack of ofmc_fp
|
||||
| simple_name of string
|
||||
| role of string
|
||||
| factname of string
|
||||
|
|
@ -122,13 +120,24 @@ fun rmOuterOp (Operator(_,[msg])) = msg
|
|||
|
||||
%%
|
||||
|
||||
START: ofmc_fp (ofmc_fp)
|
||||
START: TBACKEND TCOLON simple_names (update_backend simple_names empty_ofmc_fp)
|
||||
| TBACKEND TCOLON simple_names fp_or_attack (update_backend simple_names fp_or_attack)
|
||||
|
||||
ofmc_fp: TPROTOCOL TCOLON simple_name (update_protocol simple_name empty_ofmc_fp)
|
||||
fp_or_attack:TPROTOCOL TCOLON simple_name (update_protocol simple_name empty_ofmc_fp)
|
||||
| TPROTOCOL TCOLON simple_name ofmc_fp (update_protocol simple_name ofmc_fp)
|
||||
| TBACKEND TCOLON simple_names (update_backend simple_names empty_ofmc_fp)
|
||||
| TBACKEND TCOLON simple_names ofmc_fp (update_backend simple_names ofmc_fp)
|
||||
| TTYPES TCOLON types (update_types ((types_of empty_ofmc_fp)@types) empty_ofmc_fp)
|
||||
|
||||
| TATTACK TOPAREN msglist TCPAREN (update_attack msglist empty_ofmc_fp)
|
||||
| TATTACK TOPAREN msglist TCPAREN attackinfo (update_attack msglist attackinfo)
|
||||
|
||||
|
||||
attackinfo: TATTACK TOPAREN msglist TCPAREN (update_attack msglist empty_ofmc_fp)
|
||||
| TATTACK TOPAREN msglist TCPAREN attackinfo (update_attack msglist attackinfo)
|
||||
| TDERIVATION SIMPLE_NAME SIMPLE_NAME TATTACK TCOLON TATTACK TOPAREN msglist TCPAREN trace ((fn (_,_) => empty_ofmc_fp) (trace,msglist))
|
||||
|
||||
|
||||
|
||||
|
||||
ofmc_fp: TTYPES TCOLON types (update_types ((types_of empty_ofmc_fp)@types) empty_ofmc_fp)
|
||||
| TTYPES TCOLON types ofmc_fp (update_types ((types_of ofmc_fp)@types) ofmc_fp)
|
||||
| TSECTION TINITIAL TSECSTATE TCOLON knowledge (update_knowledge knowledge empty_ofmc_fp)
|
||||
| TSECTION TINITIAL TSECSTATE TCOLON knowledge ofmc_fp (update_knowledge knowledge ofmc_fp)
|
||||
|
|
@ -139,6 +148,20 @@ ofmc_fp: TPROTOCOL TCOLON simple_name (update_pr
|
|||
| TSECTION TABSTRACTION TCOLON abstractions (update_abstractions ((abstractions_of empty_ofmc_fp )@abstractions) empty_ofmc_fp)
|
||||
| TSECTION TABSTRACTION TCOLON (update_abstractions ((abstractions_of empty_ofmc_fp )@[]) empty_ofmc_fp)
|
||||
| TSECTION TABSTRACTION TCOLON abstractions ofmc_fp (update_abstractions ((abstractions_of ofmc_fp)@abstractions) ofmc_fp)
|
||||
|
||||
trace: TMINUS trace (empty_ofmc_fp)
|
||||
| TIKNOWS trace (empty_ofmc_fp)
|
||||
| TSECRET trace (empty_ofmc_fp)
|
||||
| TOBRACE trace (empty_ofmc_fp)
|
||||
| TCBRACE trace (empty_ofmc_fp)
|
||||
| TCBRACE (empty_ofmc_fp)
|
||||
| TOPAREN trace (empty_ofmc_fp)
|
||||
| TCPAREN trace (empty_ofmc_fp)
|
||||
| TCOMMA trace (empty_ofmc_fp)
|
||||
| TCPAREN (empty_ofmc_fp)
|
||||
| TCOMMA (empty_ofmc_fp)
|
||||
| SIMPLE_NAME trace (empty_ofmc_fp)
|
||||
| SIMPLE_NAME (empty_ofmc_fp)
|
||||
|
||||
rules: TSTEP TCOLON facts TMETAIMPLIES facts ([(NONE, facts1, facts2)])
|
||||
| TSTEP TCOLON facts TMETAIMPLIES facts rules ((NONE, facts1, facts2)::rules)
|
||||
|
|
@ -157,10 +180,10 @@ facts: fact ([fact])
|
|||
|
||||
fact: TSTATE TOPAREN role TCOMMA TOBRACKET msglist TCBRACKET TCPAREN (State(role, msglist))
|
||||
| TIKNOWS TOPAREN msg TCPAREN (Iknows(msg))
|
||||
| TATTACK TOPAREN msg TCPAREN (Attack(msg))
|
||||
| TSECRET TOPAREN msglist TCPAREN (Secret(msglist))
|
||||
| TWITNESS TOPAREN msglist TCPAREN (Witness(msglist))
|
||||
| TREQUEST TOPAREN msglist TCPAREN (Request(msglist))
|
||||
| TATTACK TOPAREN msglist TCPAREN (Attack(msglist))
|
||||
|
||||
nfacts: nfact ([nfact])
|
||||
| nfact TSEMICOLON nfacts (nfact::nfacts)
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@ signature OfmcFpParser_TOKENS =
|
|||
sig
|
||||
type ('a,'b) token
|
||||
type svalue
|
||||
val TDERIVATION: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TXOR: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TWITNESS: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TTYPES: (string) * 'a * 'a -> (svalue,'a) token
|
||||
|
|
@ -29,6 +30,8 @@ val TFACT: (string) * 'a * 'a -> (svalue,'a) token
|
|||
val TEXP: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TQUOTE: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TCRYPT: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TCBRACE: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TOBRACE: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TCPAREN: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TCOMMA: (string) * 'a * 'a -> (svalue,'a) token
|
||||
val TBAR: (string) * 'a * 'a -> (svalue,'a) token
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -9,34 +9,26 @@
|
|||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
* modification, are permitted provided that the following conditions are met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright notice, this
|
||||
* list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* * Redistributions in binary form must reproduce the above copyright notice,
|
||||
* this list of conditions and the following disclaimer in the documentation
|
||||
* and/or other materials provided with the distribution.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: ofmc-fp.lex 869 2009-10-30 10:36:14Z brucker $ *)
|
||||
|
||||
structure Tokens = Tokens
|
||||
|
||||
|
|
@ -80,6 +72,8 @@ ws = [\ \t];
|
|||
|
||||
|
||||
"-" => (Tokens.TMINUS(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"{" => (Tokens.TOBRACE(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"}" => (Tokens.TCBRACE(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"->" => (Tokens.TARROW(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
":" => (Tokens.TCOLON(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"=" => (Tokens.TEQ(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
|
|
@ -121,6 +115,7 @@ ws = [\ \t];
|
|||
"Inv" => (Tokens.TINV(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"Exp" => (Tokens.TEXP(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"Xor" => (Tokens.TXOR(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
"Derivation" => (Tokens.TDERIVATION(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
|
||||
(_|{alpha}|{digit})+ => (Tokens.SIMPLE_NAME(yytext,inputPos_half yypos,inputPos_half yypos));
|
||||
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -9,34 +9,26 @@
|
|||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
* modification, are permitted provided that the following conditions are met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright notice, this
|
||||
* list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* * Redistributions in binary form must reproduce the above copyright notice,
|
||||
* this list of conditions and the following disclaimer in the documentation
|
||||
* and/or other materials provided with the distribution.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: ofmc_abstraction.sml 929 2009-11-01 22:37:06Z brucker $ *)
|
||||
|
||||
structure ofmc_abstraction =
|
||||
struct
|
||||
|
|
@ -50,7 +42,7 @@ datatype CMsg = CVariable of string * string
|
|||
|
||||
datatype CFact = CState of string * CMsg list
|
||||
| CIknows of CMsg
|
||||
| CAttack of CMsg
|
||||
| CAttack of CMsg list
|
||||
| CWitness of CMsg list
|
||||
| CRequest of CMsg list
|
||||
| CSecret of CMsg list
|
||||
|
|
@ -122,9 +114,9 @@ fun deabstractMsg abstractions (Atom s) = (case check_abstraction abstra
|
|||
|
||||
fun deabstractFact abstractions (State (n,ms)) = (CState (n, map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Iknows m) = (CIknows (deabstractMsg abstractions m))
|
||||
| deabstractFact abstractions (Attack m) = (CAttack (deabstractMsg abstractions m))
|
||||
| deabstractFact abstractions (Witness ms) = (CWitness (map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Attack ms) = (CAttack (map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Request ms) = (CRequest (map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Witness ms) = (CWitness (map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Secret ms) = (CSecret (map (deabstractMsg abstractions) ms))
|
||||
| deabstractFact abstractions (Fact (n,m)) = (CFact (n, deabstractMsg abstractions m))
|
||||
| deabstractFact abstractions (NotEqual (n,m)) = (CNotEqual (deabstractMsg abstractions n, deabstractMsg abstractions m))
|
||||
|
|
|
|||
|
|
@ -9,34 +9,26 @@
|
|||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
* modification, are permitted provided that the following conditions are met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright notice, this
|
||||
* list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* * Redistributions in binary form must reproduce the above copyright notice,
|
||||
* this list of conditions and the following disclaimer in the documentation
|
||||
* and/or other materials provided with the distribution.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: ofmc_connector.sml 903 2009-11-01 19:05:11Z brucker $ *)
|
||||
|
||||
signature OFMC_CONNECTOR =
|
||||
sig
|
||||
|
|
|
|||
|
|
@ -9,31 +9,24 @@
|
|||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
* modification, are permitted provided that the following conditions are met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright notice, this
|
||||
* list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* * Redistributions in binary form must reproduce the above copyright notice,
|
||||
* this list of conditions and the following disclaimer in the documentation
|
||||
* and/or other materials provided with the distribution.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: ofmc_encoder.sml 450 2009-02-02 08:59:41Z brucker $ *)
|
||||
|
|
|
|||
|
|
@ -9,43 +9,45 @@
|
|||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
* modification, are permitted provided that the following conditions are met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright notice, this
|
||||
* list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* * Redistributions in binary form must reproduce the above copyright notice,
|
||||
* this list of conditions and the following disclaimer in the documentation
|
||||
* and/or other materials provided with the distribution.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: ofmc_thygen.sml 937 2009-11-02 05:21:07Z brucker $ *)
|
||||
|
||||
signature OFMC_ENCODER =
|
||||
sig
|
||||
val ofmc_thygen: OfmcFp.ofmc_fp -> unit
|
||||
val ofmc_thygenAnB: string -> unit
|
||||
val main: string * string list -> unit
|
||||
type result
|
||||
val ofmc_thygen: OfmcFp.ofmc_fp -> result * OfmcFp.ofmc_fp
|
||||
val ofmc_thygenAnB: string -> result * OfmcFp.ofmc_fp
|
||||
val main: string * string list -> unit * OfmcFp.ofmc_fp
|
||||
end
|
||||
|
||||
structure ofmc_thygen =
|
||||
struct
|
||||
datatype result = unknownError | success | parseError | attackOfmc | attackIsabelle
|
||||
|
||||
fun string_of_result unknownError = "unkown error"
|
||||
| string_of_result success = "success"
|
||||
| string_of_result parseError = "parse error"
|
||||
| string_of_result attackOfmc = "attack found by ofmc"
|
||||
| string_of_result attackIsabelle = "attack found by isabelle"
|
||||
|
||||
|
||||
val varcnt = ref ~1
|
||||
val noproof = ref false
|
||||
|
|
@ -69,7 +71,7 @@ fun gen_header ofmcfp =
|
|||
else filename
|
||||
end
|
||||
in
|
||||
"header {* Analysing "^(protocol)^" *}\n"
|
||||
"chapter {* Analysing "^(protocol)^" *}\n"
|
||||
^"(* *********************************** \n"
|
||||
^" This file is automatically generated from the AnB file \""
|
||||
^(source_of ofmcfp)^"\".\n"
|
||||
|
|
@ -82,7 +84,7 @@ fun gen_header ofmcfp =
|
|||
else filename (source_of ofmcfp) )
|
||||
^"\"\n"
|
||||
^" imports"^"\n"
|
||||
^" ofmc"^"\n"
|
||||
^" \"../src/ofmc\""^"\n"
|
||||
^"begin"^"\n\n"
|
||||
end
|
||||
|
||||
|
|
@ -167,7 +169,7 @@ fun gen_datatype ofmcfp =
|
|||
|
||||
fun collect_vars ofmcfp (CState (s,ms)) = List.concat (map (collect_msgvars ofmcfp) ms)
|
||||
| collect_vars ofmcfp (CIknows m) = collect_msgvars ofmcfp m
|
||||
| collect_vars ofmcfp (CAttack m) = collect_msgvars ofmcfp m
|
||||
| collect_vars ofmcfp (CAttack ms) = List.concat (map (collect_msgvars ofmcfp) ms)
|
||||
| collect_vars ofmcfp (CWitness ms) = List.concat (map (collect_msgvars ofmcfp) ms)
|
||||
| collect_vars ofmcfp (CRequest ms) = List.concat (map (collect_msgvars ofmcfp) ms)
|
||||
| collect_vars ofmcfp (CSecret ms) = List.concat (map (collect_msgvars ofmcfp) ms)
|
||||
|
|
@ -190,7 +192,7 @@ and string_of_cmsg_list [] = ""
|
|||
|
||||
fun string_of_cfact ofmcfp (CState (s,ms)) = "State("^s^", ["^(string_of_cmsg_list ms)^"] )"
|
||||
| string_of_cfact ofmcfp (CIknows m) = "Iknows("^(string_of_cmsg m)^")"
|
||||
| string_of_cfact ofmcfp (CAttack m) = "Attack("^(string_of_cmsg m)^")"
|
||||
| string_of_cfact ofmcfp (CAttack ms) = "Attack("^(string_of_cmsg_list ms)^")"
|
||||
| string_of_cfact ofmcfp (CWitness ms) = "Witness("^(string_of_cmsg_list ms)^")"
|
||||
| string_of_cfact ofmcfp (CRequest ms) = "Request("^(string_of_cmsg_list ms)^")"
|
||||
| string_of_cfact ofmdfp (CSecret ms) = "Secret("^(string_of_cmsg_list ms)^")"
|
||||
|
|
@ -272,7 +274,7 @@ fun gen_fp ofmcfp =
|
|||
|
||||
fun mk_vars_unique (CState (s,ms)) = (CState (s, map mk_msgvars_unique ms))
|
||||
| mk_vars_unique (CIknows m) = (CIknows (mk_msgvars_unique m) )
|
||||
| mk_vars_unique (CAttack m) = (CAttack (mk_msgvars_unique m))
|
||||
| mk_vars_unique (CAttack ms) = (CAttack (map mk_msgvars_unique ms))
|
||||
| mk_vars_unique (CWitness ms) = (CWitness (map mk_msgvars_unique ms))
|
||||
| mk_vars_unique (CRequest ms) = (CRequest (map mk_msgvars_unique ms))
|
||||
| mk_vars_unique (CSecret ms) = (CSecret (map mk_msgvars_unique ms))
|
||||
|
|
@ -280,7 +282,7 @@ fun gen_fp ofmcfp =
|
|||
|
||||
fun mk_vars_unique' v (CState (s,ms)) = (CState (s, map (mk_msgvars_unique' v) ms))
|
||||
| mk_vars_unique' v (CIknows m) = (CIknows (mk_msgvars_unique' v m) )
|
||||
| mk_vars_unique' v (CAttack m) = (CAttack (mk_msgvars_unique' v m))
|
||||
| mk_vars_unique' v (CAttack ms) = (CAttack (map (mk_msgvars_unique' v) ms))
|
||||
| mk_vars_unique' v (CWitness ms) = (CWitness (map (mk_msgvars_unique' v) ms))
|
||||
| mk_vars_unique' v (CRequest ms) = (CRequest (map (mk_msgvars_unique' v) ms))
|
||||
| mk_vars_unique' v (CSecret ms) = (CSecret (map (mk_msgvars_unique' v) ms))
|
||||
|
|
@ -329,16 +331,14 @@ fun gen_fp ofmcfp =
|
|||
in
|
||||
if inner_quantification
|
||||
then
|
||||
( "constdefs"
|
||||
^" "^protocolFp^"::\"Fact set\""
|
||||
^"\""^protocolFp^" == {m. (\n"
|
||||
( "definition\n"
|
||||
^"\""^protocolFp^" = {m. (\n"
|
||||
^" ("^(string_of_fp_fact ofmcfp (hd facts)^")\n")
|
||||
^(String.concat (map (fn f => " | ("^(string_of_fp_fact ofmcfp f)^")\n") (tl facts) ))
|
||||
^")}\"\n")
|
||||
else
|
||||
( "constdefs"
|
||||
^" "^protocolFp^"::\"Fact set\""
|
||||
^"\""^protocolFp^" == {m. ( ? "^(String.concat (map (fn f => string_of_cmsg f^" ") (#1 outer_ex )))^".\n"
|
||||
( "definition\n"
|
||||
^"\""^protocolFp^" = {m. ( ? "^(String.concat (map (fn f => string_of_cmsg f^" ") (#1 outer_ex )))^".\n"
|
||||
^" ("^(string_of_fp_fact' ofmcfp (hd (#2 outer_ex ))^")\n")
|
||||
^(String.concat (map (fn f => " | ("^(string_of_fp_fact' ofmcfp f)^")\n") (tl (#2 outer_ex )) ))
|
||||
^")}\"\n")
|
||||
|
|
@ -430,6 +430,8 @@ fun checkfp ofmcfp =
|
|||
|
||||
|
||||
fun ofmc_thygen ofmcfp =
|
||||
if is_safe ofmcfp
|
||||
then
|
||||
let
|
||||
val protocol = protocol_of ofmcfp
|
||||
val _ = print (gen_header ofmcfp)
|
||||
|
|
@ -451,9 +453,11 @@ fun ofmc_thygen ofmcfp =
|
|||
val _ = print ("*)\n")
|
||||
*)
|
||||
val _ = print ("\n\nend (* theory *)\n")
|
||||
in () end
|
||||
in (success,ofmcfp) end
|
||||
else (attackOfmc,ofmcfp)
|
||||
|
||||
val ofmc_thygenAnB = ofmc_thygen o ofmc_connector.parseAnBFile
|
||||
fun ofmc_thygenAnB f = (ofmc_thygen o ofmc_connector.parseAnBFile) f
|
||||
handle _ => (parseError, OfmcFp.empty_ofmc_fp)
|
||||
|
||||
fun print_usage name = let
|
||||
val _ = print("\n")
|
||||
|
|
@ -467,6 +471,8 @@ in
|
|||
()
|
||||
end
|
||||
|
||||
fun warning s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr)
|
||||
|
||||
fun main (name:string,args:(string list)) =
|
||||
let
|
||||
val prgName = (hd o rev) (String.fields (fn s => s = #"/" orelse s = #"\\") name)
|
||||
|
|
@ -478,7 +484,26 @@ fun main (name:string,args:(string list)) =
|
|||
| (n, "--wauth"::ar) => (ofmc_connector.wauth := true ; main(name, ar))
|
||||
| (n, [file]) => if String.isPrefix "-" file
|
||||
then print_usage name
|
||||
else ofmc_thygenAnB file
|
||||
else let
|
||||
val timer = Timer.startRealTimer ()
|
||||
val start = Timer.checkRealTimer timer
|
||||
val (result,fp) = ofmc_thygenAnB file
|
||||
val stop = Timer.checkRealTimer timer
|
||||
val duration = Time.-(stop,start)
|
||||
fun print_result duration result fp =
|
||||
let
|
||||
val _ = warning ("\nprotocol: "^(protocol_of fp)^"\n")
|
||||
val _ = warning ("result: "^(string_of_result result)^"\n")
|
||||
val _ = warning ("duration: "^(Time.toString duration)^"\n")
|
||||
val _ = warning ("fixed-point: "
|
||||
^(Int.toString(List.length (fixedpoint_of fp )))^"\n")
|
||||
val _ = warning ("knowledge: "
|
||||
^(Int.toString(List.length (knowledge_of fp )))^"\n")
|
||||
in () end
|
||||
in
|
||||
print_result duration result fp
|
||||
end
|
||||
|
||||
| (_,_) => print_usage name
|
||||
)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -9,34 +9,26 @@
|
|||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
* modification, are permitted provided that the following conditions are met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright notice, this
|
||||
* list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* * Redistributions in binary form must reproduce the above copyright notice,
|
||||
* this list of conditions and the following disclaimer in the documentation
|
||||
* and/or other materials provided with the distribution.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: ofmcfp.sml 890 2009-10-31 21:34:17Z brucker $ *)
|
||||
|
||||
|
||||
structure OfmcFp = struct
|
||||
|
|
@ -54,7 +46,7 @@ type ProtocolState = MsgPat list
|
|||
datatype Fact = State of string * Msg list
|
||||
| FPState of string * Msg
|
||||
| Iknows of Msg
|
||||
| Attack of Msg
|
||||
| Attack of Msg list
|
||||
| Witness of Msg list
|
||||
| Request of Msg list
|
||||
| Secret of Msg list
|
||||
|
|
@ -72,30 +64,35 @@ type ofmc_fp = {
|
|||
Knowledge: (string * Fact) list,
|
||||
FixedPoint: (string * Fact) list,
|
||||
Abstractions : (Msg * Msg) list,
|
||||
Attack : Msg list,
|
||||
Source : string
|
||||
}
|
||||
|
||||
|
||||
val empty_ofmc_fp = {Backend="", Protocol="", Types = [("Number",["NI"])], Rules = [], Knowledge=[], FixedPoint=[],
|
||||
Abstractions=[(Atom "ni",Atom "NI")], Source=""}:ofmc_fp
|
||||
Abstractions=[(Atom "ni",Atom "NI")], Source="", Attack=[]}:ofmc_fp
|
||||
(* Abstractions=[(Atom "purpose",Atom "PURPOSE"),(Atom "ni",Atom "NI")], Source=""}:ofmc_fp *)
|
||||
|
||||
fun update_protocol protocol ({Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_backend backend ({Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_types types ({Backend=backend, Protocol=protocol, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_rules rules ({Backend=backend, Protocol=protocol, Types=types, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_knowledge knowledge ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_fixedpoint fixedpoint ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, Abstractions=abstractions,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_abstractions abstractions ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint,Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
fun update_source source ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint,Abstractions=abstractions, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source}:ofmc_fp)
|
||||
|
||||
fun update_protocol protocol ({Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack,...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_backend backend ({Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack,...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_types types ({Backend=backend, Protocol=protocol, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack,...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_rules rules ({Backend=backend, Protocol=protocol, Types=types, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack,...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_knowledge knowledge ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_fixedpoint fixedpoint ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, Abstractions=abstractions,Source=source, Attack=attack, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_abstractions abstractions ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint,Source=source, Attack=attack, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
fun update_source source ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint,Abstractions=abstractions, Attack=attack, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Source=source, Attack=attack}:ofmc_fp)
|
||||
|
||||
fun update_attack attack ({Backend=backend, Protocol=protocol, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint,Abstractions=abstractions, Source=source, ...}:ofmc_fp)
|
||||
= ({Protocol=protocol, Source=source, Backend=backend, Types=types, Rules=rules, Knowledge = knowledge, FixedPoint=fixedpoint, Abstractions=abstractions,Attack=attack}:ofmc_fp)
|
||||
|
||||
|
||||
fun mk_unique [] = []
|
||||
|
|
@ -113,5 +110,9 @@ fun fixedpoint_of (ofmcfp:ofmc_fp) = #FixedPoint ofmcfp
|
|||
fun abstractions_of (ofmcfp:ofmc_fp) = #Abstractions ofmcfp
|
||||
fun source_of (ofmcfp:ofmc_fp) = #Source ofmcfp
|
||||
|
||||
fun attack_of (ofmcfp:ofmc_fp) = #Attack ofmcfp
|
||||
|
||||
fun is_safe ofmcfp = (attack_of ofmcfp = [])
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -9,34 +9,26 @@
|
|||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
* modification, are permitted provided that the following conditions are met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright notice, this
|
||||
* list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* * Redistributions in binary form must reproduce the above copyright notice,
|
||||
* this list of conditions and the following disclaimer in the documentation
|
||||
* and/or other materials provided with the distribution.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: root.sml 450 2009-02-02 08:59:41Z brucker $ *)
|
||||
|
||||
|
||||
val ord = Char.ord;
|
||||
|
|
|
|||
125
src/ofmc.thy
125
src/ofmc.thy
|
|
@ -4,49 +4,36 @@
|
|||
* config.sml.in --- main configuration file for Isabelle-OFMC
|
||||
* This file is part of Isabelle-OFMC.
|
||||
*
|
||||
* Copyright (c) 2009 Achim D. Brucker, Germany
|
||||
* Copyright (c) 2009-2016 Achim D. Brucker, Germany
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions are
|
||||
* met:
|
||||
* modification, are permitted provided that the following conditions are met:
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright notice, this
|
||||
* list of conditions and the following disclaimer.
|
||||
*
|
||||
* * Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* * Redistributions in binary form must reproduce the above copyright notice,
|
||||
* this list of conditions and the following disclaimer in the documentation
|
||||
* and/or other materials provided with the distribution.
|
||||
*
|
||||
* * Redistributions in binary form must reproduce the above
|
||||
* copyright notice, this list of conditions and the following
|
||||
* disclaimer in the documentation and/or other materials provided
|
||||
* with the distribution.
|
||||
*
|
||||
* * Neither the name of the copyright holders nor the names of its
|
||||
* contributors may be used to endorse or promote products derived
|
||||
* from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
******************************************************************************)
|
||||
(* $Id: ofmc.thy 935 2009-11-02 00:02:50Z brucker $ *)
|
||||
|
||||
|
||||
theory
|
||||
ofmc
|
||||
imports
|
||||
Main
|
||||
(* uses
|
||||
"kernel_ext/isabelle2009_kernel_patch.ML"
|
||||
(* "kernel_ext/ProofObligationMgr2008.sml" *)
|
||||
*)
|
||||
begin
|
||||
|
||||
|
||||
|
|
@ -60,76 +47,33 @@ section {* Proof Obligation Manager Configuration *}
|
|||
|
||||
section {* Isabelle/ofmc Specific Tactics *}
|
||||
|
||||
(*
|
||||
|
||||
|
||||
setup {*
|
||||
Method.add_method ("propagate_fp_cterm",
|
||||
let
|
||||
fun propagate_fp_tac ctxt facts =
|
||||
let
|
||||
val thy = ProofContext.theory_of ctxt
|
||||
fun m_tac thm =
|
||||
let
|
||||
fun collect_facts (((Const ("op :",_))$(t)$(Const("List.set",_)$_))) = [t]
|
||||
| collect_facts (t1$t2) = ((collect_facts t1)@(collect_facts t2))
|
||||
| collect_facts (Abs (_,_,t)) = collect_facts t
|
||||
| collect_facts _ = []
|
||||
val cand = collect_facts (hd(prems_of(thm)))
|
||||
fun subst v t = let
|
||||
val _ = warning ("substituting "^(Syntax.string_of_term ctxt t))
|
||||
in
|
||||
(Thm.cterm_of thy (Var((v,0),type_of t)),
|
||||
Thm.cterm_of thy t)
|
||||
end
|
||||
val _ = warning ("Candidates found:")
|
||||
val _ = map (fn p => warning (" "^(Syntax.string_of_term ctxt p)
|
||||
)) cand
|
||||
|
||||
fun foo [f] = (forw_terminst_tac [] [subst "c" f] (instantiate' [SOME (ctyp_of thy (type_of f))] [] (PureThy.get_thm thy "subsetD")) 1)
|
||||
THEN (simp_tac HOL_ss 1)
|
||||
| foo (f::facts) = foo [f] THEN (foo facts)
|
||||
| foo [] = all_tac
|
||||
in
|
||||
(foo cand) thm
|
||||
end
|
||||
in
|
||||
m_tac
|
||||
end
|
||||
in
|
||||
Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => propagate_fp_tac ctxt facts))
|
||||
end,
|
||||
"propagate fixed-point")
|
||||
*})
|
||||
|
||||
*)
|
||||
|
||||
|
||||
setup {*
|
||||
Method.add_method("propagate_fp",
|
||||
method_setup propagate_fp = {*
|
||||
let
|
||||
fun propagate_fp_tac_str ctxt facts =
|
||||
fun propagate_fp_tac_str ctxt =
|
||||
let
|
||||
val thy = ProofContext.theory_of ctxt
|
||||
val thy = Proof_Context.theory_of ctxt
|
||||
fun m_tac thm =
|
||||
let
|
||||
fun replace_bounded b (t1$t2) = (replace_bounded b t1)$(replace_bounded b t2)
|
||||
| replace_bounded b (Bound c) = Free(List.nth (b,(List.length b) - c -1))
|
||||
| replace_bounded _ t = t
|
||||
|
||||
fun collect_facts b (((Const ("op :",_))$(t)$(Const("List.set",_)$_))) = [replace_bounded b t]
|
||||
fun collect_facts b (((Const (@{const_name Set.member},_))$(t)$(Const(@{const_name List.set},_)$_))) = [replace_bounded b t]
|
||||
| collect_facts b (t1$t2) = ((collect_facts b t1)@(collect_facts b t2))
|
||||
| collect_facts b (Abs (n,ty,t)) = collect_facts (b@[(n,ty)]) t
|
||||
| collect_facts _ _ = []
|
||||
fun to_string f = (PrintMode.setmp [] Display.string_of_cterm (cterm_of thy f))
|
||||
val cand = case prems_of(thm) of
|
||||
|
||||
val string_of_term = Sledgehammer_Util.hackish_string_of_term ctxt
|
||||
val string_of_cterm = string_of_term o Thm.term_of
|
||||
|
||||
val cand = case Thm.prems_of thm of
|
||||
[] => []
|
||||
| (p::ps) => collect_facts [] p
|
||||
(* val _ = warning "Candiates are"
|
||||
val _ = map (fn s => warning (Syntax.string_of_term ctxt s)) cand *)
|
||||
(* fun foo [f] = (forw_inst_tac ctxt [("c", to_string f )] (PureThy.get_thm thy "subsetD") 1) *)
|
||||
fun foo [f] = (forw_inst_tac ctxt [(("c",0), to_string f )] (PureThy.get_thm thy "subsetD") 1)
|
||||
THEN (simp_tac HOL_ss 1)
|
||||
|
||||
fun my_inst_tac f = (Rule_Insts.forw_inst_tac ctxt [((("c",0),Position.none), string_of_term f )]
|
||||
[] (@{thm subsetD}) 1)
|
||||
|
||||
fun foo [f] = (my_inst_tac f) THEN (simp_tac ctxt 1)
|
||||
| foo (f::facts) = foo [f] THEN (foo facts)
|
||||
| foo [] = all_tac
|
||||
in
|
||||
|
|
@ -139,10 +83,11 @@ let
|
|||
m_tac
|
||||
end
|
||||
in
|
||||
Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => propagate_fp_tac_str ctxt facts))
|
||||
Scan.succeed (fn ctxt: Proof.context =>
|
||||
SIMPLE_METHOD' (fn i: int => propagate_fp_tac_str ctxt))
|
||||
end
|
||||
,"propagate fixed-point")
|
||||
*}
|
||||
*} "propagate fixed-point"
|
||||
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
Reference in New Issue