andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
0b524e6ef8
scyther/src/specialterm.h

79 lines
2.0 KiB
C
Raw Normal View History

Added GPL 2 License to the C sources. A first step towards releasing Scyther completely to the public.
2007-06-11 13:01:04 +01:00
/*
* Scyther : An automatic verifier for security protocols.
Updating time stamps for next release.
2013-10-05 23:56:12 +01:00
* Copyright (C) 2007-2013 Cas Cremers
Added GPL 2 License to the C sources. A first step towards releasing Scyther completely to the public.
2007-06-11 13:01:04 +01:00
*
* This program is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
* as published by the Free Software Foundation; either version 2
* of the License, or (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program; if not, write to the Free Software
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
*/
- Moved special terms into their own (very) special file.
2005-06-16 15:10:07 +01:00
#ifndef SPECIALTERM
#define SPECIALTERM
- Improved some type of warnings for e.g. empty prec sets andsoforth.
2005-12-28 14:25:06 +00:00
#include "term.h"
#include "termlist.h"
- Many cleanups to make -Wall happy. Next up is pedantic...
2007-01-06 14:45:29 +00:00
#include "system.h"
- Improved some type of warnings for e.g. empty prec sets andsoforth.
2005-12-28 14:25:06 +00:00
- Moved special terms into their own (very) special file.
2005-06-16 15:10:07 +01:00
/*
* Some declarations in spercialterm.c
*/
extern Term TERM_Agent;
extern Term TERM_Function;
extern Term TERM_Hidden;
Introduced markers in proof output for consistency with book description.
2012-10-02 12:43:30 +01:00
extern Term TERM_CoOld;
extern Term TERM_CoNew;
extern Term TERM_DeEx;
extern Term TERM_DeNew;
- Moved special terms into their own (very) special file.
2005-06-16 15:10:07 +01:00
extern Term TERM_Type;
extern Term TERM_Nonce;
extern Term TERM_Ticket;
- Added '--concrete' switch to fill in to pick readable names for variables.
2005-11-12 21:13:00 +00:00
extern Term TERM_Data;
- Moved special terms into their own (very) special file.
2005-06-16 15:10:07 +01:00
extern Term TERM_Claim;
extern Term CLAIM_Secret;
NEW: Added Aliveness and Weak Agreement claims.
2011-01-04 14:18:22 +00:00
extern Term CLAIM_Alive;
extern Term CLAIM_Weakagree;
- Moved special terms into their own (very) special file.
2005-06-16 15:10:07 +01:00
extern Term CLAIM_Nisynch;
extern Term CLAIM_Niagree;
extern Term CLAIM_Empty;
- New claim: CLAIM_Reachable - Added new switches: -G,--generate-statespace -C,--generate-claims - Claims are now allowed to have no label (they will be generated automatically) - Output summary shows parameter of claims - Internally, new symbols can now be generated by symbolNextFree(prefixsymbol)
2005-12-28 11:50:17 +00:00
extern Term CLAIM_Reachable;
NEW: Added SID & SKR dummy claims. This allows for input file reuse among branches (i.e. compromise).
2011-01-04 14:17:52 +00:00
extern Term CLAIM_SID;
extern Term CLAIM_SKR;
NEW: Added claims: Commit and Running. There are two new claims: claim(X,Commit,t) : check for agreement on data claim(X,Running,t) : signaling claim The property checked is that each claim Commit needs to be preceded by a Running with an identical term t. Cherry-picked from commit 99a6be00e9d3d219ec73665607e8a3a7d65d04d1
2011-01-04 14:10:14 +00:00
extern Term CLAIM_Commit;
extern Term CLAIM_Running;
Added support for inequality tests. There is a new event: not match(t1,t2) where t1,t2 are terms. They are implemented by using a special claim that simply stores the intended inequality. The pruning theorems (prune_theorems.c) ensure that these terms never become equal. If there are equal, the constraint is violated. As long as they are not equal, there exists a solution using groung terms such that their instantiation is not equal. Currently not very efficient implemented and the graph out output is also ugly for now. Conflicts: gui/Scyther/Trace.py src/compiler.c src/scanner.l
2012-11-21 12:40:15 +00:00
extern Term CLAIM_Notequal;
- Moved special terms into their own (very) special file.
2005-06-16 15:10:07 +01:00
- Big catchup commit to make sure we are up to beta7. This includes a number of single patches, ranging from the vista fix with the buffers, to the start of many new minor features.
2007-05-18 13:06:29 +01:00
extern Term AGENT_Alice;
extern Term AGENT_Bob;
extern Term AGENT_Charlie;
extern Term AGENT_Dave;
extern Term AGENT_Eve;
Attack output improvement: better choice of agent names. When an attack pattern is displayed, Scyther instantiates open variables with concrete names. This is often more intuitive for humans. In the case of instantiating role names, we often ended up assigning Alice to the B role and Bob to the A role. This patch provides a more clever heuristic to find agent names that start with the same letter as the role (variable) name. In case this fails, we still try to map Alice to roles starting with 'I' and Bob to 'R', and otherwise we just pick something. Also added "Simon" and "Pete" to cover some common role names. Conflicts: src/arachne.c
2014-06-30 17:03:24 +01:00
extern Term AGENT_Simon;
extern Term AGENT_Pete;
SPDL: Introduced preconstructed PKI with pk/sk/k. Introduced K(A1...AN) constant function for symmetric pre-shared keys. Added inverses (pk,sk) as default constructs.
2010-11-10 10:15:00 +00:00
extern Term TERM_PK;
extern Term TERM_SK;
extern Term TERM_K;
- Big catchup commit to make sure we are up to beta7. This includes a number of single patches, ranging from the vista fix with the buffers, to the start of many new minor features.
2007-05-18 13:06:29 +01:00
Implemented equality/pattern matching support. Introduced a new event: match(pattern,groundterm) This event can only be executed if pattern can be matched to groundterm. Variable substitutions are persistent with respect to later events in the same role. Currently implemented as syntactic sugar, essentially unfolded in role R to: fresh x; send ( R,R, { groundterm }x ); recv ( R,R, { pattern }x ); This work is not complete yet in the send that the output still contains the unfolding. Ideally, the graph rendered detects this syntactic sugar and renders a simplified event. This should be possible on the basis of the label name prefix. Conflicts: src/compiler.c src/parser.y src/scanner.l src/tac.h
2012-11-21 10:28:40 +00:00
extern Term LABEL_Match;
- Improved some type of warnings for e.g. empty prec sets andsoforth.
2005-12-28 14:25:06 +00:00
extern Termlist CLAIMS_dep_prec;
- Many cleanups to make -Wall happy. Next up is pedantic...
2007-01-06 14:45:29 +00:00
void specialTermInit (const System sys);
- Big catchup commit to make sure we are up to beta7. This includes a number of single patches, ranging from the vista fix with the buffers, to the start of many new minor features.
2007-05-18 13:06:29 +01:00
void specialTermInitAfter (const System sys);
- Removed some too interesting pruning methods that really need theorems first. Revealed by the certified e-mail protocol by Abadi and Blanchet.
2006-01-17 16:18:26 +00:00
int isTicketTerm (Term t);
int hasTicketSubterm (Term t);
- Moved special terms into their own (very) special file.
2005-06-16 15:10:07 +01:00
#endif
Reference in New Issue Copy Permalink