Applying Practical Formal Methods to the Specifications and Analysis of Security Properties

2001 ◽  
Author(s):  
Constance Heitmeyer
Keyword(s):  
Formal Methods ◽  
Security Properties

Can Formal Methods Really Help

2012 ◽  
pp. 361-380
Author(s):  
Komminist Weldemariam ◽  
Adolfo Villafiorita
Keyword(s):  
Formal Methods ◽  
Learning Process ◽  
Extended Model ◽  
Voting Systems ◽  
Current Development ◽  
Current Trends ◽  
Security Properties ◽  
Specification And Verification ◽  
Formal Techniques ◽  
Voting Machine

In this chapter, first the authors discuss the current trends in the usage of formal techniques in the development of e-voting systems. They then present their experiences on their usage to specify and verify the behaviors of one of the currently deployed e-voting systems, using formal techniques and verification against a subset of critical security properties that the system should meet. The authors also specify attacks that have been shown to successfully compromise the system. The attack information is used to extend the original specification of the system and derive what the authors call the extended model. This work is a step towards fostering open specification and the (partial) verification of a voting machine. The specification and verification was intended as a learning process where formal techniques were used to improve the current development of e-voting systems.

Methods for Dependability and Security Analysis of Large Networks

2009 ◽  
pp. 921-929
Author(s):  
Ioannis Chochliouros ◽  
Anastasia S. Spiliopoulou ◽  
Stergios P. Chochliouros
Keyword(s):  
Experimental Data ◽  
Formal Methods ◽  
Security Analysis ◽  
The Other ◽  
Network Nodes ◽  
Dependability Analysis ◽  
Underlying Network ◽  
Security Properties ◽  
Unauthorized Disclosure ◽  
Specific Evaluation

Dependability and security are rigorously related concepts that, however, differ for the specific proprieties they mainly concentrate on. In particular, in most commonly applied cases found in practical design techniques (Piedad & Hawkins, 2000), the dependability concept usually includes the security one, being a superset of it. In typical cases, security mainly comprises the following fundamental characteristics: confidentiality, integrity, and availability. Indeed, dependability mainly encompasses the following attributes (Avizienis, Laprie, Randell, & Landwehr, 2004): (1) availability: readiness for correct service; (2) reliability: continuity of correct service; (3) safety: absence of catastrophic consequences on the user(s) and the environment; (4) confidentiality: absence of unauthorized disclosure of information; (5) integrity: absence of improper system alterations; and (6) maintainability: ability to undergo modifications and repairs. The present work primarily intends to deal with formal methods, appropriate to perform both security and dependability analysis in modern networks. In general, security analysis of great networks takes the form of determining the exploitable vulnerabilities of a network, and intends to provide results or appropriate informative (or occasionally experimental) data about which network nodes can be compromised by exploiting chains of vulnerabilities, as well as specifying which fundamental security properties are altered (e.g., Confidentiality, Integrity, Availability). Therefore, such type of analysis is also referred as “network vulnerability analysis.” On the other hand, dependability analysis of networks typically intends to determine specific dependencies within the nodes (or the services offered) of the (appropriate) underlying network, so as to provide results about the consequences of (potential) faults (on services or hosts) and to find out which among these faults are able to cause unacceptable consequences, in terms of the basic dependability attributes. At this specific evaluation, it should be noted that it is possible to consider attacks (as well as attack consequences) as faults.

Application of formal methods to the VIPER microprocessor

1987 ◽  
Vol 134 (3) ◽  
pp. 133 ◽  
Author(s):  
W.J. Cullyer ◽  
C.H. Pygott
Keyword(s):  
Formal Methods

A Prototype Formal Methods Environment

2001 ◽  
Author(s):  
Ray Teitelbaum
Keyword(s):  
Formal Methods

Data Integrity

2017 ◽  
Author(s):  
Keith M. Martin
Keyword(s):  
Hash Function ◽  
Hash Functions ◽  
Data Integrity ◽  
Message Authentication ◽  
Authenticated Encryption ◽  
Authentication Codes ◽  
Basic Model ◽  
Function Design ◽  
Security Properties ◽  
Different Levels

This chapter discusses cryptographic mechanisms for providing data integrity. We begin by identifying different levels of data integrity that can be provided. We then look in detail at hash functions, explaining the different security properties that they have, as well as presenting several different applications of a hash function. We then look at hash function design and illustrate this by discussing the hash function SHA-3. Next, we discuss message authentication codes (MACs), presenting a basic model and discussing basic properties. We compare two different MAC constructions, CBC-MAC and HMAC. Finally, we consider different ways of using MACs together with encryption. We focus on authenticated encryption modes, and illustrate these by describing Galois Counter mode.

Sign in / Sign up

Export Citation Format

Share Document